cprover
goto2graph.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Turns a goto-program into an abstract event graph
4 
5 Author: Vincent Nimal
6 
7 Date: 2012
8 
9 \*******************************************************************/
10 
13 
14 #include "goto2graph.h"
15 
16 #include <vector>
17 #include <string>
18 #include <fstream>
19 
20 #include <util/options.h>
21 
23 
24 #include <goto-instrument/rw_set.h>
25 
26 #include "fence.h"
27 
28 // #define PRINT_UNSAFES
29 
30 
32 bool inline instrumentert::local(const irep_idt &id)
33 {
34  std::string identifier=id2string(id);
35 
36  if(has_prefix(identifier, "symex_invalid") ||
37  has_prefix(identifier, "symex::invalid"))
38  {
39  /* symex_invalid and symex::invalid_object generated when pointer analysis
40  fails */
41  return true;
42  }
43 
44  if(identifier==CPROVER_PREFIX "alloc" ||
45  identifier==CPROVER_PREFIX "alloc_size" ||
46  identifier=="stdin" ||
47  identifier=="stdout" ||
48  identifier=="stderr" ||
49  identifier=="sys_nerr" ||
50  has_prefix(identifier, "__unbuffered_"))
51  return true;
52 
53  const size_t pos=identifier.find("[]");
54 
55  if(pos!=std::string::npos)
56  {
57  /* we don't distinguish the members of an array for the moment */
58  identifier.erase(pos);
59  }
60 
61  try
62  {
63  const symbolt &symbol=ns.lookup(identifier);
64 
65  if(!symbol.is_static_lifetime)
66  return true; /* these are local */
67 
68  if(symbol.is_thread_local)
69  return true; /* these are local */
70 
71  return false;
72  }
73  catch(const std::string &exception)
74  {
75  message.debug()<<"Exception: "<<exception << messaget::eom;
76  return false;
77  }
78 }
79 
81 {
82  return instrumenter.local(i);
83 }
84 
88  value_setst &value_sets,
89  memory_modelt model,
90  bool no_dependencies,
91  loop_strategyt duplicate_body)
92 {
93  if(!no_dependencies)
94  message.status() << "Dependencies analysis enabled" << messaget::eom;
95 
96  /* builds the graph following the CFG */
97  cfg_visitort visitor(ns, *this);
98  visitor.visit_cfg(value_sets, model, no_dependencies, duplicate_body,
100 
101  std::vector<std::size_t> subgraph_index;
102  num_sccs=egraph_alt.SCCs(subgraph_index);
103  assert(egraph_SCCs.empty());
104  egraph_SCCs.resize(num_sccs, std::set<event_idt>());
105  for(std::map<event_idt, event_idt>::const_iterator
106  it=map_vertex_gnode.begin();
107  it!=map_vertex_gnode.end();
108  it++)
109  {
110  const std::size_t sg=subgraph_index[it->second];
111  egraph_SCCs[sg].insert(it->first);
112  }
113 
114  message.status() << "Number of threads detected: "
115  << visitor.max_thread << messaget::eom;
116 
117  /* SCCs which could host critical cycles */
118  unsigned interesting_sccs=0;
119  for(unsigned i=0; i<num_sccs; i++)
120  if(egraph_SCCs[i].size()>3)
121  interesting_sccs++;
122 
123  message.statistics() << "Graph with " << egraph_alt.size() << " nodes has "
124  << interesting_sccs << " interesting SCCs"
125  << messaget::eom;
126 
127  message.statistics() << "Number of reads: " << visitor.read_counter
128  << messaget::eom;
129  message.statistics() << "Number of writes: " << visitor.write_counter
130  << messaget::eom;
131  message.statistics() << "Number of wse: " << visitor.ws_counter
132  << messaget::eom;
133  message.statistics() << "Number of rfe/fre: " << visitor.fr_rf_counter
134  << messaget::eom;
135  std::size_t instr_counter=0;
136  for(goto_functionst::function_mapt::const_iterator
137  it=goto_functions.function_map.begin();
138  it!=goto_functions.function_map.end();
139  ++it)
140  instr_counter+=it->second.body.instructions.size();
141  message.statistics() << "Number of goto-instructions: "
142  << instr_counter<<messaget::eom;
143 
144  return visitor.max_thread;
145 }
146 
148  /* value_sets and options */
149  value_setst &value_sets,
150  memory_modelt model,
151  bool no_dependencies,
152  loop_strategyt replicate_body,
153  /* function to analyse */
154  const irep_idt &function,
155  /* incoming edges */
156  const std::set<instrumentert::cfg_visitort::nodet> &initial_vertex,
157  /* outcoming edges */
158  std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)
159 {
160  /* flow: egraph */
161 
162  instrumenter.message.debug() << "visit function "
163  << function << messaget::eom;
164 
165  if(function == INITIALIZE_FUNCTION)
166  {
167  return;
168  }
169 
170 #ifdef LOCAL_MAY
171  local_may_aliast local_may(
172  instrumenter.goto_functions.function_map[function]);
173 #endif
174 
175  /* goes through the function */
177  instrumenter.goto_functions.function_map[function].body)
178  {
179  goto_programt::instructiont &instruction=*i_it;
180 
181  /* thread marking */
182  if(instruction.is_start_thread())
183  {
184  max_thread=max_thread+1;
185  coming_from=current_thread;
186  current_thread=max_thread;
187  }
188  else if(instruction.is_end_thread())
189  current_thread=coming_from;
190  thread=current_thread;
191 
192  instrumenter.message.debug() << "visit instruction "<<instruction.type
193  << messaget::eom;
194 
195  if(instruction.is_start_thread() || instruction.is_end_thread())
196  {
197  /* break the flow */
198  visit_cfg_thread();
199  }
200  else if(instruction.is_atomic_begin() || instruction.is_atomic_end())
201  {
202  /* break the flow (def 1) or add full barrier (def 2) */
203  #ifdef ATOMIC_BREAK
204  visit_cfg_thread();
205  #elif defined ATOMIC_FENCE
206  visit_cfg_fence(i_it);
207  #else
208  /* propagates */
209  visit_cfg_propagate(i_it);
210  #endif
211  }
212  /* a:=b -o-> Rb -po-> Wa */
213  else if(instruction.is_assign())
214  {
215  visit_cfg_assign(value_sets, ns, i_it, no_dependencies
216 #ifdef LOCAL_MAY
217  , local_may
218 #endif
219  ); // NOLINT(whitespace/parens)
220  }
221  else if(is_fence(instruction, instrumenter.ns))
222  {
223  instrumenter.message.debug() << "Constructing a fence" << messaget::eom;
224  visit_cfg_fence(i_it);
225  }
226  else if(model!=TSO && is_lwfence(instruction, instrumenter.ns))
227  {
228  visit_cfg_lwfence(i_it);
229  }
230  else if(model==TSO && is_lwfence(instruction, instrumenter.ns))
231  {
232  /* propagation */
233  visit_cfg_skip(i_it);
234  }
235  else if(instruction.is_other()
236  && instruction.code.get_statement()==ID_fence)
237  {
238  visit_cfg_asm_fence(i_it);
239  }
240  else if(instruction.is_function_call())
241  {
242  visit_cfg_function_call(value_sets, i_it, model,
243  no_dependencies, replicate_body);
244  }
245  else if(instruction.is_goto())
246  {
247  visit_cfg_goto(i_it, replicate_body, value_sets
248 #ifdef LOCAL_MAY
249  , local_may
250 #endif
251  ); // NOLINT(whitespace/parens)
252  }
253 #ifdef CONTEXT_INSENSITIVE
254  else if(instruction.is_return())
255  {
256  visit_cfg_propagate(i_it);
257  add_all_pos(it, out_nodes[function], in_pos[i_it]);
258  }
259 #endif
260  else
261  {
262  /* propagates */
263  visit_cfg_propagate(i_it);
264  }
265  }
266 
267  std::pair<unsigned, data_dpt> new_dp(thread, data_dp);
268  egraph.map_data_dp.insert(new_dp);
269  data_dp.print(instrumenter.message);
270 
271  if(instrumenter.goto_functions.function_map[function]
272  .body.instructions.empty())
273  {
274  /* empty set of ending edges */
275  }
276  else
277  {
278  goto_programt::instructionst::iterator it=instrumenter
279  .goto_functions.function_map[function].body.instructions.end();
280  --it;
281  ending_vertex=in_pos[it];
282  }
283 }
284 
286  goto_programt::instructionst::iterator i_it)
287 {
288  const goto_programt::instructiont &instruction=*i_it;
289  /* propagation */
290  in_pos[i_it].clear();
291  for(const auto &in : instruction.incoming_edges)
292  if(in_pos.find(in)!=in_pos.end())
293  for(const auto &node : in_pos[in])
294  in_pos[i_it].insert(node);
295 }
296 
298 {
299 }
300 
302 /* OBSOLETE */
303 /* Note: can be merged with visit_cfg_body */
304 /* Warning: we iterate here over the successive instructions of the
305  regardless of the gotos. This function has to be called *AFTER*
306  an exploration of the function constructing the graph. */
309 {
310  if(instrumenter.map_function_graph.find(id_function)!=
311  instrumenter.map_function_graph.end())
312  return;
313 
314  /* gets the body of the function */
315  goto_programt::instructionst &body=instrumenter.goto_functions
316  .function_map[id_function].body.instructions;
317 
318  if(body.empty())
319  return;
320 
321  /* end of function */
322  /* TODO: ensure that all the returns point to the last statement if the
323  function, or alternatively make i_it point to each return location in
324  the function */
325  goto_programt::instructionst::iterator i_it=body.end();
326  --i_it;
327 
328  /* beginning of the function */
329  goto_programt::instructionst::iterator targ=body.begin();
330 
331  std::set<event_idt> in_nodes;
332  std::set<event_idt> out_nodes;
333 
334  /* if the target has already been covered by fwd analysis */
335  if(in_pos.find(targ)!=in_pos.end())
336  {
337  /* if in_pos was updated at this program point */
338  if(updated.find(targ)!=updated.end())
339  {
340  /* connects the previous nodes to those ones */
341  for(std::set<nodet>::const_iterator to=in_pos[targ].begin();
342  to!=in_pos[targ].end(); ++to)
343  in_nodes.insert(to->first);
344  for(std::set<nodet>::const_iterator from=in_pos[i_it].begin();
345  from!=in_pos[i_it].end(); ++from)
346  out_nodes.insert(from->first);
347  }
348  else
349  {
350  instrumenter.message.debug() << "else case" << messaget::eom;
351  /* connects NEXT nodes following the targets -- bwd analysis */
352  for(goto_programt::instructionst::iterator cur=i_it;
353  cur!=targ; --cur)
354  {
355  instrumenter.message.debug() << "i" << messaget::eom;
356  for(const auto &in : cur->incoming_edges)
357  {
358  instrumenter.message.debug() << "t" << messaget::eom;
359  if(in_pos.find(in)!=in_pos.end() &&
360  updated.find(in)!=updated.end())
361  {
362  /* out_pos[in].insert(in_pos[in])*/
363  add_all_pos(it1, out_pos[in], in_pos[in]);
364  }
365  else if(in_pos.find(in)!=in_pos.end())
366  {
367  /* out_pos[in].insert(out_pos[cur])*/
368  add_all_pos(it2, out_pos[in], out_pos[cur]);
369  }
370  }
371  }
372 
373  /* connects the previous nodes to those ones */
374  if(out_pos.find(targ)!=out_pos.end())
375  {
376  for(std::set<nodet>::const_iterator to=out_pos[targ].begin();
377  to!=out_pos[targ].end(); ++to)
378  in_nodes.insert(to->first);
379  for(std::set<nodet>::const_iterator from=in_pos[i_it].begin();
380  from!=in_pos[i_it].end(); ++from)
381  out_nodes.insert(from->first);
382  }
383  }
384  }
385 
386  instrumenter.map_function_graph[id_function]=
387  std::make_pair(in_nodes, out_nodes);
388 }
389 
391  event_idt begin, event_idt end)
392 {
393  /* no need to duplicate the loop nodes for the SCC-detection graph -- a
394  single back-edge will ensure the same connectivity */
395  alt_egraph.add_edge(end, begin);
396  return end;
397 }
398 
402  value_setst &value_sets
403  #ifdef LOCAL_MAY
404  , local_may_aliast local_may
405  #endif
406 ) const
407 {
408  instrumenter.message.debug() << "contains_shared_array called for "
409  << targ->source_location.get_line() << " and "
410  << i_it->source_location.get_line() << messaget::eom;
411  for(goto_programt::const_targett cur=targ; cur!=i_it; ++cur)
412  {
413  instrumenter.message.debug() << "Do we have an array at line "
414  <<cur->source_location.get_line()<<"?" << messaget::eom;
415  rw_set_loct rw_set(ns, value_sets, cur
416  #ifdef LOCAL_MAY
417  , local_may
418  #endif
419  ); // NOLINT(whitespace/parens)
420  instrumenter.message.debug() << "Writes: "<<rw_set.w_entries.size()
421  <<"; Reads:"<<rw_set.r_entries.size() << messaget::eom;
422 
423  forall_rw_set_r_entries(r_it, rw_set)
424  {
425  const irep_idt var=r_it->second.object;
426  instrumenter.message.debug() << "Is "<<var<<" an array?"
427  << messaget::eom;
428  if(id2string(var).find("[]")!=std::string::npos
429  && !instrumenter.local(var))
430  return true;
431  }
432 
433  forall_rw_set_w_entries(w_it, rw_set)
434  {
435  const irep_idt var=w_it->second.object;
436  instrumenter.message.debug()<<"Is "<<var<<" an array?"<<messaget::eom;
437  if(id2string(var).find("[]")!=std::string::npos
438  && !instrumenter.local(var))
439  return true;
440  }
441  }
442 
443  return false;
444 }
445 
446 
450  loop_strategyt replicate_body,
451  value_setst &value_sets
452 #ifdef LOCAL_MAY
453  , local_may_aliast &local_may
454 #endif
455 )
456 {
457  /* for each target of the goto */
458  for(const auto &target : i_it->targets)
459  {
460  /* if the target has already been covered by fwd analysis */
461  if(in_pos.find(target)!=in_pos.end())
462  {
463  if(in_pos[i_it].empty())
464  continue;
465 
466  bool duplicate_this=false;
467 
468  switch(replicate_body)
469  {
470  case arrays_only:
471  duplicate_this=contains_shared_array(target, i_it, value_sets
472  #ifdef LOCAL_MAY
473  , local_may
474  #endif
475  ); // NOLINT(whitespace/parens)
476  break;
477  case all_loops:
478  duplicate_this=true;
479  break;
480  case no_loop:
481  duplicate_this=false;
482  break;
483  }
484 
485  if(duplicate_this)
486  visit_cfg_duplicate(target, i_it);
487  else
488  visit_cfg_backedge(target, i_it);
489  }
490  }
491 }
492 
496 {
497  instrumenter.message.status() << "Duplication..." << messaget::eom;
499  instrumenter.goto_functions.function_map[i_it->function];
500 
501  bool found_pos=false;
502  goto_programt::const_targett new_targ=targ;
503 
504  if(in_pos[targ].empty())
505  {
506  /* tries to find the next node after the back edge */
507  for(; new_targ!=fun.body.instructions.end();
508  ++new_targ)
509  {
510  if(in_pos.find(new_targ)!=in_pos.end() && !in_pos[new_targ].empty())
511  {
512  found_pos=true;
513  break;
514  }
515  }
516 
517  if(!found_pos
518  || new_targ->source_location.get_function()
519  !=targ->source_location.get_function()
520  || new_targ->source_location.get_file()
521  !=targ->source_location.get_file())
522  return;
523  }
524 
525  /* appends the body once more */
526  const std::set<nodet> &up_set=in_pos[(found_pos ? new_targ : targ)];
527  const std::set<nodet> &down_set=in_pos[i_it];
528 
529  for(std::set<nodet>::const_iterator begin_it=up_set.begin();
530  begin_it!=up_set.end(); ++begin_it)
531  instrumenter.message.debug() << "Up " << begin_it->first << messaget::eom;
532 
533  for(std::set<nodet>::const_iterator begin_it=down_set.begin();
534  begin_it!=down_set.end(); ++begin_it)
535  instrumenter.message.debug() << "Down " << begin_it->first <<messaget::eom;
536 
537  for(std::set<nodet>::const_iterator begin_it=up_set.begin();
538  begin_it!=up_set.end(); ++begin_it)
539  {
540  for(std::set<nodet>::const_iterator end_it=down_set.begin();
541  end_it!=down_set.end(); ++end_it)
542  {
543  egraph.copy_segment(begin_it->first, end_it->first);
544  alt_copy_segment(egraph_alt, begin_it->second, end_it->second);
545 #if 0
546  const event_idt end=egraph.copy_segment(begin_it->first, end_it->first);
547  const event_idt alt_end=
548  alt_copy_segment(egraph_alt, begin_it->second, end_it->second);
549  // copied; no need for back-edge!
550  // in_pos[i_it].insert(nodet(end, alt_end));
551 #endif
552  }
553  }
554 }
555 
560 {
561  /* if in_pos was updated at this program point */
562  if(updated.find(targ)!=updated.end())
563  {
564  /* connects the previous nodes to those ones */
565  for(std::set<nodet>::const_iterator to=in_pos[targ].begin();
566  to!=in_pos[targ].end(); ++to)
567  for(std::set<nodet>::const_iterator from=in_pos[i_it].begin();
568  from!=in_pos[i_it].end(); ++from)
569  if(from->first!=to->first)
570  {
571  if(egraph[from->first].thread!=egraph[to->first].thread)
572  continue;
573  instrumenter.message.debug() << from->first << "-po->"
574  << to->first << messaget::eom;
575  egraph.add_po_back_edge(from->first, to->first);
576  egraph_alt.add_edge(from->second, to->second);
577  }
578  }
579  else
580  {
581  instrumenter.message.debug() << "else case" << messaget::eom;
582 
583  /* connects NEXT nodes following the targets -- bwd analysis */
584  for(goto_programt::const_targett cur=i_it;
585  cur!=targ; --cur)
586  {
587  for(const auto &in : cur->incoming_edges)
588  {
589  if(in_pos.find(in)!=in_pos.end()
590  && updated.find(in)!=updated.end())
591  {
592  /* out_pos[in].insert(in_pos[in])*/
593  add_all_pos(it1, out_pos[in], in_pos[in]);
594  }
595  else if(in_pos.find(in)!=in_pos.end())
596  {
597  /* out_pos[in].insert(in_pos[cur])*/
598  add_all_pos(it2, out_pos[in], out_pos[cur]);
599  }
600  }
601  }
602 
603  /* connects the previous nodes to those ones */
604  if(out_pos.find(targ)!=out_pos.end())
605  {
606  for(std::set<nodet>::const_iterator to=out_pos[targ].begin();
607  to!=out_pos[targ].end(); ++to)
608  for(std::set<nodet>::const_iterator from=in_pos[i_it].begin();
609  from!=in_pos[i_it].end(); ++from)
610  if(from->first!=to->first)
611  {
612  if(egraph[from->first].thread!=egraph[to->first].thread)
613  continue;
614  instrumenter.message.debug() << from->first<<"-po->"
615  <<to->first << messaget::eom;
616  egraph.add_po_back_edge(from->first, to->first);
617  egraph_alt.add_edge(from->second, to->second);
618  }
619  }
620  }
621 }
622 
624  goto_programt::instructionst::iterator i_it,
625  loop_strategyt replicate_body,
626  value_setst &value_sets
627 #ifdef LOCAL_MAY
628  , local_may_aliast &local_may
629 #endif
630 )
631 {
632  const goto_programt::instructiont &instruction=*i_it;
633 
634  /* propagates */
635  visit_cfg_propagate(i_it);
636 
637  /* if back-edges, constructs them too:
638  if goto to event, connects previously propagated events to it;
639  if not, we need to find which events AFTER the target are to
640  be connected. We do a backward analysis. */
641  if(instruction.is_backwards_goto())
642  {
643  instrumenter.message.debug() << "backward goto" << messaget::eom;
644  visit_cfg_body(i_it, replicate_body, value_sets
645 #ifdef LOCAL_MAY
646  , local_may
647 #endif
648  ); // NOLINT(whitespace/parens)
649  }
650 }
651 
653  value_setst &value_sets,
654  goto_programt::instructionst::iterator i_it,
655  memory_modelt model,
656  bool no_dependencies,
657  loop_strategyt replicate_body)
658 {
659  const goto_programt::instructiont &instruction=*i_it;
660  std::set<nodet> s;
661  for(const auto &in : instruction.incoming_edges)
662  if(in_pos.find(in)!=in_pos.end())
663  for(const auto &node : in_pos[in])
664  s.insert(node);
665 
666  const exprt &fun=to_code_function_call(instruction.code).function();
667  const irep_idt &fun_id=to_symbol_expr(fun).get_identifier();
668  /* ignore recursive calls -- underapproximation */
669  try
670  {
671  enter_function(fun_id);
672  #ifdef CONTEXT_INSENSITIVE
673  stack_fun.push(cur_fun);
674  cur_fun=fun_id;
675  #endif
676 
677  #if 0
678  if(!inline_function_cond(fun_id))
679  {
680  /* do not inline it, connect to an existing subgraph or create a new
681  one */
682  if(instrumenter.map_function_graph.find(fun_id)!=
683  instrumenter.map_function_graph.end())
684  {
685  /* connects to existing */
686  /* TODO */
687  }
688  else
689  {
690  /* just inlines */
691  /* TODO */
692  visit_cfg_function(value_sets, model, no_dependencies, fun_id, s,
693  in_pos[i_it]);
694  updated.insert(i_it);
695  }
696  }
697  else // NOLINT(readability/braces)
698  #endif
699  {
700  /* normal inlining strategy */
701  visit_cfg_function(value_sets, model, no_dependencies, replicate_body,
702  fun_id, s, in_pos[i_it]);
703  updated.insert(i_it);
704  }
705 
706  leave_function(fun_id);
707  #ifdef CONTEXT_INSENSITIVE
708  cur_fun=stack_fun.pop();
709  #endif
710  }
711  catch(const std::string &s)
712  {
713  instrumenter.message.warning() << "sorry, doesn't handle recursion "
714  << "(function " << fun_id << "; .cpp) "
715  << s << messaget::eom;
716  }
717 }
718 
720  goto_programt::instructionst::iterator i_it)
721 {
722  const goto_programt::instructiont &instruction=*i_it;
724  thread, "f", instrumenter.unique_id++, instruction.source_location, false);
725  const event_idt new_fence_node=egraph.add_node();
726  egraph[new_fence_node](new_fence_event);
727  const event_idt new_fence_gnode=egraph_alt.add_node();
728  egraph_alt[new_fence_gnode]=new_fence_event;
729  instrumenter.map_vertex_gnode.insert(
730  std::make_pair(new_fence_node, new_fence_gnode));
731 
732  for(const auto &in : instruction.incoming_edges)
733  if(in_pos.find(in)!=in_pos.end())
734  {
735  for(const auto &node : in_pos[in])
736  {
737  if(egraph[node.first].thread!=thread)
738  continue;
739  instrumenter.message.debug() << node.first<<"-po->"<<new_fence_node
740  << messaget::eom;
741  egraph.add_po_edge(node.first, new_fence_node);
742  egraph_alt.add_edge(node.second, new_fence_gnode);
743  }
744  }
745 
746  in_pos[i_it].clear();
747  in_pos[i_it].insert(nodet(new_fence_node, new_fence_gnode));
748  updated.insert(i_it);
749 }
750 
752  goto_programt::instructionst::iterator i_it)
753 {
754  const goto_programt::instructiont &instruction=*i_it;
755  bool WRfence=instruction.code.get_bool(ID_WRfence);
756  bool WWfence=instruction.code.get_bool(ID_WWfence);
757  bool RRfence=instruction.code.get_bool(ID_RRfence);
758  bool RWfence=instruction.code.get_bool(ID_RWfence);
759  bool WWcumul=instruction.code.get_bool(ID_WWcumul);
760  bool RRcumul=instruction.code.get_bool(ID_RRcumul);
761  bool RWcumul=instruction.code.get_bool(ID_RWcumul);
763  thread, "asm", instrumenter.unique_id++, instruction.source_location,
764  false, WRfence, WWfence, RRfence, RWfence, WWcumul, RWcumul, RRcumul);
765  const event_idt new_fence_node=egraph.add_node();
766  egraph[new_fence_node](new_fence_event);
767  const event_idt new_fence_gnode=egraph_alt.add_node();
768  egraph_alt[new_fence_gnode]=new_fence_event;
769  instrumenter.map_vertex_gnode.insert(
770  std::make_pair(new_fence_node, new_fence_gnode));
771 
772  for(const auto &in : instruction.incoming_edges)
773  if(in_pos.find(in)!=in_pos.end())
774  {
775  for(const auto &node : in_pos[in])
776  {
777  if(egraph[node.first].thread!=thread)
778  continue;
779  instrumenter.message.debug() << node.first<<"-po->"<<new_fence_node
780  << messaget::eom;
781  egraph.add_po_edge(node.first, new_fence_node);
782  egraph_alt.add_edge(node.second, new_fence_gnode);
783  }
784  }
785 
786  in_pos[i_it].clear();
787  in_pos[i_it].insert(nodet(new_fence_node, new_fence_gnode));
788  updated.insert(i_it);
789 }
790 
792  value_setst &value_sets,
793  namespacet &ns,
794  goto_programt::instructionst::iterator &i_it,
795  bool no_dependencies
796 #ifdef LOCAL_MAY
797  , local_may_aliast &local_may
798 #endif
799  )
800 {
801  goto_programt::instructiont &instruction=*i_it;
802 
803  /* Read (Rb) */
804  rw_set_loct rw_set(ns, value_sets, i_it
805 #ifdef LOCAL_MAY
806  , local_may
807 #endif
808  ); // NOLINT(whitespace/parens)
809 
810  event_idt previous=std::numeric_limits<event_idt>::max();
811  event_idt previous_gnode=std::numeric_limits<event_idt>::max();
812 
813 #if 0
814  /* for the moment, use labels ASSERT in front of the assertions
815  to prevent them from being instrumented */
816  if(instruction.is_assert())
817  continue; // return;
818  if(!instruction.labels.empty() && instruction.labels.front()=="ASSERT")
819  continue; // return;
820 #endif
821 
822  forall_rw_set_r_entries(r_it, rw_set)
823  {
824  /* creates Read:
825  read is the irep_id of the read in the code;
826  new_read_event is the corresponding abstract event;
827  new_read_node is the node in the graph */
828  const irep_idt &read=r_it->second.object;
829 
830  /* skip local variables */
831  if(local(read))
832  continue;
833 
834  read_counter++;
835 #if 0
836  assert(read_expr);
837 #endif
838 
840  thread, id2string(read), instrumenter.unique_id++,
841  instruction.source_location, local(read));
842 
843  const event_idt new_read_node=egraph.add_node();
844  egraph[new_read_node]=new_read_event;
845  instrumenter.message.debug() << "new Read"<<read<<" @thread"
846  <<(thread)<<"("<<instruction.source_location<<","
847  <<(local(read)?"local":"shared")<<") #"<<new_read_node
848  << messaget::eom;
849 
850  if(read==ID_unknown)
851  unknown_read_nodes.insert(new_read_node);
852 
853  const event_idt new_read_gnode=egraph_alt.add_node();
854  egraph_alt[new_read_gnode]=new_read_event;
855  instrumenter.map_vertex_gnode.insert(
856  std::make_pair(new_read_node, new_read_gnode));
857 
858  /* creates ... -po-> Read */
859  for(const auto &in : instruction.incoming_edges)
860  {
861  if(in_pos.find(in)!=in_pos.end())
862  {
863  for(const auto &node : in_pos[in])
864  {
865  if(egraph[node.first].thread!=thread)
866  continue;
867  instrumenter.message.debug() << node.first<<"-po->"
868  <<new_read_node << messaget::eom;
869  egraph.add_po_edge(node.first, new_read_node);
870  egraph_alt.add_edge(node.second, new_read_gnode);
871  }
872  }
873  }
874 
875  map_reads.insert(id2node_pairt(read, new_read_node));
876  previous=new_read_node;
877  previous_gnode=new_read_gnode;
878 
879  /* creates Read <-com-> Write ... */
880  const std::pair<id2nodet::iterator, id2nodet::iterator>
881  with_same_var=map_writes.equal_range(read);
882  for(id2nodet::iterator id_it=with_same_var.first;
883  id_it!=with_same_var.second; id_it++)
884  if(egraph[id_it->second].thread!=new_read_event.thread)
885  {
886  instrumenter.message.debug() << id_it->second<<"<-com->"
887  <<new_read_node << messaget::eom;
888  std::map<event_idt, event_idt>::const_iterator entry=
889  instrumenter.map_vertex_gnode.find(id_it->second);
890  assert(entry!=instrumenter.map_vertex_gnode.end());
891  egraph.add_com_edge(new_read_node, id_it->second);
892  egraph_alt.add_edge(new_read_gnode, entry->second);
893  egraph.add_com_edge(id_it->second, new_read_node);
894  egraph_alt.add_edge(entry->second, new_read_gnode);
895  ++fr_rf_counter;
896  }
897 
898  /* for unknown writes */
899  for(std::set<event_idt>::const_iterator id_it=
900  unknown_write_nodes.begin();
901  id_it!=unknown_write_nodes.end();
902  ++id_it)
903  if(egraph[*id_it].thread!=new_read_event.thread)
904  {
905  instrumenter.message.debug() << *id_it<<"<-com->"
906  <<new_read_node << messaget::eom;
907  std::map<event_idt, event_idt>::const_iterator entry=
908  instrumenter.map_vertex_gnode.find(*id_it);
909  assert(entry!=instrumenter.map_vertex_gnode.end());
910  egraph.add_com_edge(new_read_node, *id_it);
911  egraph_alt.add_edge(new_read_gnode, entry->second);
912  egraph.add_com_edge(*id_it, new_read_node);
913  egraph_alt.add_edge(entry->second, new_read_gnode);
914  ++fr_rf_counter;
915  }
916  }
917 
918  /* Write (Wa) */
919  forall_rw_set_w_entries(w_it, rw_set)
920  {
921  /* creates Write:
922  write is the irep_id in the code;
923  new_write_event is the corresponding abstract event;
924  new_write_node is the node in the graph */
925  const irep_idt &write=w_it->second.object;
926 
927  instrumenter.message.debug() << "WRITE: " << write << messaget::eom;
928 
929  /* skip local variables */
930  if(local(write))
931  continue;
932 
933  ++write_counter;
934  // assert(write_expr);
935 
936  /* creates Write */
938  thread, id2string(write), instrumenter.unique_id++,
939  instruction.source_location, local(write));
940 
941  const event_idt new_write_node=egraph.add_node();
942  egraph[new_write_node](new_write_event);
943  instrumenter.message.debug() << "new Write "<<write<<" @thread"<<(thread)
944  <<"("<<instruction.source_location<<","
945  << (local(write)?"local":"shared")<<") #"<<new_write_node
946  << messaget::eom;
947 
948  if(write==ID_unknown)
949  unknown_read_nodes.insert(new_write_node);
950 
951  const event_idt new_write_gnode=egraph_alt.add_node();
952  egraph_alt[new_write_gnode]=new_write_event;
953  instrumenter.map_vertex_gnode.insert(
954  std::pair<event_idt, event_idt>(new_write_node, new_write_gnode));
955 
956  /* creates Read -po-> Write */
957  if(previous!=std::numeric_limits<event_idt>::max())
958  {
959  instrumenter.message.debug() << previous<<"-po->"<<new_write_node
960  << messaget::eom;
961  egraph.add_po_edge(previous, new_write_node);
962  egraph_alt.add_edge(previous_gnode, new_write_gnode);
963  }
964  else
965  {
966  for(const auto &in : instruction.incoming_edges)
967  {
968  if(in_pos.find(in)!=in_pos.end())
969  {
970  for(const auto &node : in_pos[in])
971  {
972  if(egraph[node.first].thread!=thread)
973  continue;
974  instrumenter.message.debug() << node.first<<"-po->"
975  <<new_write_node << messaget::eom;
976  egraph.add_po_edge(node.first, new_write_node);
977  egraph_alt.add_edge(node.second, new_write_gnode);
978  }
979  }
980  }
981  }
982 
983  /* creates Write <-com-> Read */
984  const std::pair<id2nodet::iterator, id2nodet::iterator>
985  r_with_same_var=map_reads.equal_range(write);
986  for(id2nodet::iterator idr_it=r_with_same_var.first;
987  idr_it!=r_with_same_var.second; idr_it++)
988  if(egraph[idr_it->second].thread!=new_write_event.thread)
989  {
990  instrumenter.message.debug() <<idr_it->second<<"<-com->"
991  <<new_write_node << messaget::eom;
992  std::map<event_idt, event_idt>::const_iterator entry=
993  instrumenter.map_vertex_gnode.find(idr_it->second);
994  assert(entry!=instrumenter.map_vertex_gnode.end());
995  egraph.add_com_edge(new_write_node, idr_it->second);
996  egraph_alt.add_edge(new_write_gnode, entry->second);
997  egraph.add_com_edge(idr_it->second, new_write_node);
998  egraph_alt.add_edge(entry->second, new_write_gnode);
999  ++fr_rf_counter;
1000  }
1001 
1002  /* creates Write <-com-> Write */
1003  const std::pair<id2nodet::iterator, id2nodet::iterator>
1004  w_with_same_var=map_writes.equal_range(write);
1005  for(id2nodet::iterator idw_it=w_with_same_var.first;
1006  idw_it!=w_with_same_var.second; idw_it++)
1007  if(egraph[idw_it->second].thread!=new_write_event.thread)
1008  {
1009  instrumenter.message.debug() << idw_it->second<<"<-com->"
1010  <<new_write_node << messaget::eom;
1011  std::map<event_idt, event_idt>::const_iterator entry=
1012  instrumenter.map_vertex_gnode.find(idw_it->second);
1013  assert(entry!=instrumenter.map_vertex_gnode.end());
1014  egraph.add_com_edge(new_write_node, idw_it->second);
1015  egraph_alt.add_edge(new_write_gnode, entry->second);
1016  egraph.add_com_edge(idw_it->second, new_write_node);
1017  egraph_alt.add_edge(entry->second, new_write_gnode);
1018  ++ws_counter;
1019  }
1020 
1021  /* for unknown writes */
1022  for(std::set<event_idt>::const_iterator id_it=
1023  unknown_write_nodes.begin();
1024  id_it!=unknown_write_nodes.end();
1025  ++id_it)
1026  if(egraph[*id_it].thread!=new_write_event.thread)
1027  {
1028  instrumenter.message.debug() << *id_it<<"<-com->"
1029  <<new_write_node << messaget::eom;
1030  std::map<event_idt, event_idt>::const_iterator entry=
1031  instrumenter.map_vertex_gnode.find(*id_it);
1032  assert(entry!=instrumenter.map_vertex_gnode.end());
1033  egraph.add_com_edge(new_write_node, *id_it);
1034  egraph_alt.add_edge(new_write_gnode, entry->second);
1035  egraph.add_com_edge(*id_it, new_write_node);
1036  egraph_alt.add_edge(entry->second, new_write_gnode);
1037  ++fr_rf_counter;
1038  }
1039 
1040  /* for unknown reads */
1041  for(std::set<event_idt>::const_iterator id_it=
1042  unknown_read_nodes.begin();
1043  id_it!=unknown_read_nodes.end();
1044  ++id_it)
1045  if(egraph[*id_it].thread!=new_write_event.thread)
1046  {
1047  instrumenter.message.debug() << *id_it<<"<-com->"
1048  <<new_write_node << messaget::eom;
1049  std::map<event_idt, event_idt>::const_iterator entry=
1050  instrumenter.map_vertex_gnode.find(*id_it);
1051  assert(entry!=instrumenter.map_vertex_gnode.end());
1052  egraph.add_com_edge(new_write_node, *id_it);
1053  egraph_alt.add_edge(new_write_gnode, entry->second);
1054  egraph.add_com_edge(*id_it, new_write_node);
1055  egraph_alt.add_edge(entry->second, new_write_gnode);
1056  ++fr_rf_counter;
1057  }
1058 
1059 
1060  map_writes.insert(id2node_pairt(write, new_write_node));
1061  previous=new_write_node;
1062  previous_gnode=new_write_gnode;
1063  }
1064 
1065  if(previous!=std::numeric_limits<event_idt>::max())
1066  {
1067  in_pos[i_it].clear();
1068  in_pos[i_it].insert(nodet(previous, previous_gnode));
1069  updated.insert(i_it);
1070  }
1071  else
1072  {
1073  /* propagation */
1074  visit_cfg_skip(i_it);
1075  }
1076 
1077  /* data dependency analysis */
1078  if(!no_dependencies)
1079  {
1080  forall_rw_set_w_entries(write_it, rw_set)
1081  forall_rw_set_r_entries(read_it, rw_set)
1082  {
1083  const irep_idt &write=write_it->second.object;
1084  const irep_idt &read=read_it->second.object;
1085  instrumenter.message.debug() << "dp: Write:"<<write<<"; Read:"<<read
1086  << messaget::eom;
1087  const datat read_p(read, instruction.source_location);
1088  const datat write_p(write, instruction.source_location);
1089  data_dp.dp_analysis(read_p, local(read), write_p, local(write));
1090  }
1091  data_dp.dp_merge();
1092 
1093  forall_rw_set_r_entries(read2_it, rw_set)
1094  forall_rw_set_r_entries(read_it, rw_set)
1095  {
1096  const irep_idt &read2=read2_it->second.object;
1097  const irep_idt &read=read_it->second.object;
1098  if(read2==read)
1099  continue;
1100  const datat read_p(read, instruction.source_location);
1101  const datat read2_p(read2, instruction.source_location);
1102  data_dp.dp_analysis(read_p, local(read), read2_p, local(read2));
1103  }
1104  data_dp.dp_merge();
1105  }
1106 }
1107 
1109  goto_programt::instructionst::iterator i_it)
1110 {
1111  const goto_programt::instructiont &instruction=*i_it;
1113  thread, "F", instrumenter.unique_id++, instruction.source_location, false);
1114  const event_idt new_fence_node=egraph.add_node();
1115  egraph[new_fence_node](new_fence_event);
1116  const event_idt new_fence_gnode=egraph_alt.add_node();
1117  egraph_alt[new_fence_gnode]=new_fence_event;
1118  instrumenter.map_vertex_gnode.insert(
1119  std::make_pair(new_fence_node, new_fence_gnode));
1120 
1121  for(const auto &in : instruction.incoming_edges)
1122  if(in_pos.find(in)!=in_pos.end())
1123  {
1124  for(const auto &node : in_pos[in])
1125  {
1126  instrumenter.message.debug() << node.first<<"-po->"<<new_fence_node
1127  << messaget::eom;
1128  egraph.add_po_edge(node.first, new_fence_node);
1129  egraph_alt.add_edge(node.second, new_fence_gnode);
1130  }
1131  }
1132 #if 0
1133  std::set<nodet> s;
1134  s.insert(nodet(new_fence_node, new_fence_gnode));
1135  in_pos[i_it]=s;
1136  updated.insert(i_it);
1137 #endif
1138  in_pos[i_it].clear();
1139  in_pos[i_it].insert(nodet(new_fence_node, new_fence_gnode));
1140  updated.insert(i_it);
1141 }
1142 
1144  goto_programt::instructionst::iterator i_it)
1145 {
1146  visit_cfg_propagate(i_it);
1147 }
1148 
1150  goto_programt::instructionst::iterator it,
1151  goto_programt &interleaving)
1152 {
1153  if(it->is_return() ||
1154  it->is_throw() ||
1155  it->is_catch() ||
1156  it->is_skip() ||
1157  it->is_dead() ||
1158  it->is_start_thread() ||
1159  it->is_end_thread())
1160  return;
1161 
1162  if(it->is_atomic_begin() ||
1163  it->is_atomic_end())
1164  {
1165  /* atomicity not checked here for the moment */
1166  return;
1167  }
1168 
1169  if(it->is_function_call())
1170  {
1171  /* function call not supported for the moment */
1172  return;
1173  }
1174 
1175  /* add this instruction to the interleaving */
1176  goto_programt::targett current_instruction=interleaving.add_instruction();
1177  goto_programt::instructiont new_instruction(*it);
1178  current_instruction->swap(new_instruction);
1179 }
1180 
1182 {
1183  message.debug() << "spurious by CFG? " << messaget::eom;
1184  goto_programt interleaving;
1185 
1187  e_it!=cyc.end() && ++e_it!=cyc.end(); ++e_it)
1188  {
1189  --e_it;
1190 
1191  const abstract_eventt &current_event=egraph[*e_it];
1192  const source_locationt &current_location=current_event.source_location;
1193 
1194  /* select relevant thread (po) -- or function contained in this thread */
1195  goto_programt *current_po=nullptr;
1196  bool thread_found=false;
1197 
1199  {
1200  forall_goto_program_instructions(p_it, f_it->second.body)
1201  if(p_it->source_location==current_location)
1202  {
1203  current_po=&f_it->second.body;
1204  thread_found=true;
1205  break;
1206  }
1207 
1208  if(thread_found)
1209  break;
1210  }
1211  assert(current_po);
1212 
1213  const wmm_grapht::edgest &pos_cur=egraph.po_out(*e_it);
1214  const wmm_grapht::edgest &pos_next=egraph.po_out(*(++e_it));
1215  --e_it;
1216 
1217  bool exists_n=false;
1218 
1219  for(wmm_grapht::edgest::const_iterator edge_it=pos_cur.begin();
1220  edge_it!=pos_cur.end(); edge_it++)
1221  {
1222  if(pos_next.find(edge_it->first)!=pos_next.end())
1223  {
1224  exists_n=true;
1225  break;
1226  }
1227  }
1228 
1229  /* !exists n, has_po_edge(*e_it,n) /\ has_po_edge(*(++it--),n) */
1230  if((++e_it)!=cyc.end() || !exists_n)
1231  {
1232  --e_it;
1233 
1234  /* add this instruction to the interleaving */
1235  Forall_goto_program_instructions(i_it, *current_po)
1236  if(i_it->source_location==current_location)
1237  {
1238  /* add all the instructions of this line */
1239  for(goto_programt::instructionst::iterator same_loc=i_it;
1240  same_loc!=current_po->instructions.end()
1241  && same_loc->source_location==i_it->source_location;
1242  same_loc++)
1243  add_instr_to_interleaving(same_loc, interleaving);
1244  break;
1245  }
1246  }
1247  else
1248  {
1249  --e_it;
1250 
1251  /* find the portion of the thread to add */
1252  const abstract_eventt &next_event=egraph[*(++e_it--)];
1253  const source_locationt &next_location=next_event.source_location;
1254 
1255  bool in_cycle=false;
1256  Forall_goto_program_instructions(it, *current_po)
1257  {
1258  if(it->source_location==current_location)
1259  in_cycle=true;
1260 
1261  /* do not add the last instruction now -- will be done at
1262  the next iteration */
1263  if(it->source_location==next_location)
1264  break;
1265 
1266  if(in_cycle)
1267  add_instr_to_interleaving(it, interleaving);
1268  }
1269  }
1270  }
1271 
1272  /* if a goto points to a label outside from this interleaving, replace it
1273  by an assert 0 */
1274  Forall_goto_program_instructions(int_it, interleaving)
1275  if(int_it->is_goto())
1276  {
1277  for(const auto &t : int_it->targets)
1278  {
1279  bool target_in_cycle=false;
1280 
1281  forall_goto_program_instructions(targ, interleaving)
1282  if(targ==t)
1283  {
1284  target_in_cycle=true;
1285  break;
1286  }
1287 
1288  if(!target_in_cycle)
1289  {
1290  int_it->make_assertion(false_exprt());
1291  break;
1292  }
1293  }
1294  }
1295 
1296  /* now test whether this part of the code can exist */
1298  goto_functiont one_interleaving;
1299  one_interleaving.body.copy_from(interleaving);
1300  map.insert(std::make_pair(
1302  std::move(one_interleaving)));
1303 
1304  goto_functionst this_interleaving;
1305  this_interleaving.function_map=std::move(map);
1306  optionst no_option;
1307  null_message_handlert no_message;
1308 
1309  #if 0
1310  bmct bmc(no_option, symbol_table, no_message);
1311 
1312  bool is_spurious=bmc.run(this_interleaving);
1313 
1314  message.debug() << "CFG:"<<is_spurious << messaget::eom;
1315  return is_spurious;
1316  #else
1317 
1318  return false; // conservative for now
1319  #endif
1320 }
1321 
1323 {
1324  if(!set_of_cycles.empty())
1325  {
1326  for(std::set<event_grapht::critical_cyclet>::iterator
1327  it=set_of_cycles.begin();
1328  it!=set_of_cycles.end();
1329  )
1330  {
1331  bool erased=false;
1332  std::set<event_grapht::critical_cyclet>::iterator next=it;
1333  ++next;
1334  if(is_cfg_spurious(*it))
1335  {
1336  erased=true;
1337  set_of_cycles.erase(it);
1338  }
1339  it=next;
1340  if(!erased)
1341  ++it;
1342  }
1343  }
1344  else if(num_sccs > 0)
1345  {
1346  for(unsigned i=0; i<num_sccs; i++)
1347  for(std::set<event_grapht::critical_cyclet>::iterator it=
1348  set_of_cycles_per_SCC[i].begin();
1349  it!=set_of_cycles_per_SCC[i].end();
1350  )
1351  {
1352  bool erased=false;
1353  std::set<event_grapht::critical_cyclet>::iterator next=it;
1354  ++next;
1355  if(is_cfg_spurious(*it))
1356  {
1357  erased=true;
1358  set_of_cycles_per_SCC[i].erase(it);
1359  }
1360  it=next;
1361  if(!erased)
1362  ++it;
1363  }
1364  }
1365  else
1366  message.status() << "No cycle to filter" << messaget::eom;
1367 }
1368 
1370  const std::set<event_grapht::critical_cyclet> &set,
1371  std::ofstream &dot,
1372  std::ofstream &ref,
1373  std::ofstream &output,
1374  std::ofstream &all,
1375  std::ofstream &table,
1376  memory_modelt model,
1377  bool hide_internals)
1378 {
1379  /* to represent the po aligned in the dot */
1380  std::map<unsigned, std::set<event_idt> > same_po;
1381  unsigned max_thread=0;
1382  unsigned colour=0;
1383 
1384  /* to represent the files as clusters */
1385  std::map<irep_idt, std::set<event_idt> > same_file;
1386 
1387  /* to summarise in a table all the variables */
1388  std::map<std::string, std::string> map_id2var;
1389  std::map<std::string, std::string> map_var2id;
1390 
1391  for(std::set<event_grapht::critical_cyclet>::const_iterator it =
1392  set.begin(); it!=set.end(); it++)
1393  {
1394 #ifdef PRINT_UNSAFES
1395  message.debug() << it->print_unsafes() << messaget::eom;
1396 #endif
1397  it->print_dot(dot, colour++, model);
1398  ref << it->print_name(model, hide_internals) << '\n';
1399  output << it->print_output() << '\n';
1400  all << it->print_all(model, map_id2var, map_var2id, hide_internals)
1401  << '\n';
1402 
1403  /* emphasises instrumented events */
1404  for(std::list<event_idt>::const_iterator it_e=it->begin();
1405  it_e!=it->end(); it_e++)
1406  {
1407  const abstract_eventt &ev=egraph[*it_e];
1408 
1409  if(render_po_aligned)
1410  same_po[ev.thread].insert(*it_e);
1411  if(render_by_function)
1412  same_file[ev.source_location.get_function()].insert(*it_e);
1413  else if(render_by_file)
1414  same_file[ev.source_location.get_file()].insert(*it_e);
1415  if(ev.thread>max_thread)
1416  max_thread=ev.thread;
1417 
1418  if(var_to_instr.find(ev.variable)!=var_to_instr.end()
1419  && id2loc.find(ev.variable)!=id2loc.end())
1420  {
1421  dot << ev.id << "[label=\"\\\\lb {" << ev.id << "}";
1422  dot << ev.get_operation() << "{" << ev.variable << "} {} @thread";
1423  dot << ev.thread << "\",color=red,shape=box];\n";
1424  }
1425  }
1426  }
1427 
1428  /* aligns events by po */
1429  if(render_po_aligned)
1430  {
1431  for(unsigned i=0; i<=max_thread; i++)
1432  if(!same_po[i].empty())
1433  {
1434  dot << "{rank=same; thread_" << i
1435  << "[shape=plaintext, label=\"thread " << i << "\"];";
1436  for(std::set<event_idt>::iterator it=same_po[i].begin();
1437  it!=same_po[i].end(); it++)
1438  dot << egraph[*it].id << ";";
1439  dot << "};\n";
1440  }
1441  }
1442 
1443  /* clusters events by file/function */
1445  {
1446  for(std::map<irep_idt, std::set<event_idt> >::const_iterator it=
1447  same_file.begin();
1448  it!=same_file.end(); it++)
1449  {
1450  dot << "subgraph cluster_" << irep_id_hash()(it->first) << "{\n";
1451  dot << " label=\"" << it->first << "\";\n";
1452  for(std::set<event_idt>::const_iterator ev_it=it->second.begin();
1453  ev_it!=it->second.end(); ev_it++)
1454  {
1455  dot << " " << egraph[*ev_it].id << ";\n";
1456  }
1457  dot << "};\n";
1458  }
1459  }
1460 
1461  /* variable table for "all" */
1462  table << std::string(80, '-');
1463  for(std::map<std::string, std::string>::const_iterator
1464  m_it=map_id2var.begin();
1465  m_it!=map_id2var.end();
1466  ++m_it)
1467  {
1468  table << "\n| " << m_it->first << " : " << m_it->second;
1469  }
1470  table << '\n';
1471  table << std::string(80, '-');
1472  table << '\n';
1473 }
1474 
1475 void instrumentert::print_outputs(memory_modelt model, bool hide_internals)
1476 {
1477  std::ofstream dot;
1478  std::ofstream ref;
1479  std::ofstream output;
1480  std::ofstream all;
1481  std::ofstream table;
1482 
1483  dot.open("cycles.dot");
1484  ref.open("ref.txt");
1485  output.open("output.txt");
1486  all.open("all.txt");
1487  table.open("table.txt");
1488 
1489  dot << "digraph G {\n";
1490  dot << "nodesep=1; ranksep=1;\n";
1491 
1492  /* prints cycles in the different outputs */
1493  if(!set_of_cycles.empty())
1494  print_outputs_local(set_of_cycles, dot, ref, output, all, table,
1495  model, hide_internals);
1496  else if(num_sccs!=0)
1497  {
1498  for(unsigned i=0; i<num_sccs; i++)
1499  {
1500  std::ofstream local_dot;
1501  std::string name="scc_" + std::to_string(i) + ".dot";
1502  local_dot.open(name.c_str());
1503 
1504  local_dot << "digraph G {\n";
1505  local_dot << "nodesep=1; ranksep=1;\n";
1506  print_outputs_local(set_of_cycles_per_SCC[i], local_dot, ref, output, all,
1507  table, model, hide_internals);
1508  local_dot << "}\n";
1509  local_dot.close();
1510 
1511  dot << i << "[label=\"SCC " << i << "\",link=\"" << "scc_" << i;
1512  dot << ".svg\"]\n";
1513  }
1514  }
1515  else
1516  message.debug() << "no cycles to output" << messaget::eom;
1517 
1518  dot << "}\n";
1519 
1520  dot.close();
1521  ref.close();
1522  output.close();
1523  all.close();
1524  table.close();
1525 }
1526 
1528 #if 1
1529 // #ifdef _WIN32
1531 {
1532  unsigned scc=0;
1534  std::set<event_grapht::critical_cyclet>());
1535  for(std::vector<std::set<event_idt> >::const_iterator it=egraph_SCCs.begin();
1536  it!=egraph_SCCs.end(); it++)
1537  if(it->size()>=4)
1538  egraph.collect_cycles(set_of_cycles_per_SCC[scc++], model, *it);
1539 }
1540 #else
1541 class pthread_argumentt
1542 {
1543 public:
1544  instrumentert &instr;
1545  memory_modelt mem;
1546  const std::set<event_idt> &filter;
1547  std::set<event_grapht::critical_cyclet> &cycles;
1548 
1549  pthread_argumentt(instrumentert &_instr,
1550  memory_modelt _mem,
1551  const std::set<event_idt> &_filter,
1552  std::set<event_grapht::critical_cyclet> &_cycles)
1553  :instr(_instr), mem(_mem), filter(_filter), cycles(_cycles)
1554  {
1555  }
1556 };
1557 
1558 /* wraper */
1559 void *collect_cycles_in_thread(void *arg)
1560 {
1561  /* arguments */
1562  pthread_argumentt *p_arg=reinterpret_cast<pthread_argumentt*>(arg);
1563  instrumentert &this_instrumenter=p_arg->instr;
1564  memory_modelt model=p_arg->mem;
1565  const std::set<event_idt> &filter=p_arg->filter;
1566  std::set<event_grapht::critical_cyclet> &cycles=p_arg->cycles;
1567 
1568  this_instrumenter.egraph.collect_cycles(cycles, model, filter);
1569 
1570  return NULL;
1571 }
1572 
1574 {
1575  const unsigned number_of_sccs=num_sccs;
1576  std::set<unsigned> interesting_SCCs;
1577 
1578  unsigned scc=0;
1579  pthread_t *threads=new pthread_t[num_sccs+1];
1580 
1582  std::set<event_grapht::critical_cyclet>());
1583 
1584  for(std::vector<std::set<unsigned> >::const_iterator it=egraph_SCCs.begin();
1585  it!=egraph_SCCs.end(); it++)
1586  if(it->size()>=4)
1587  {
1588  interesting_SCCs.insert(scc);
1589  pthread_argumentt arg(*this, model, *it, set_of_cycles_per_SCC[scc]);
1590 
1591  int rc=pthread_create(&threads[scc++], NULL,
1592  collect_cycles_in_thread, &arg);
1593 
1594  message.status()<<(rc!=0?"Failure ":"Success ")
1595  <<"in creating thread for SCC #"<<scc-1<<messaget::eom;
1596  }
1597 
1598  for(unsigned i=0; i<number_of_sccs; i++)
1599  if(interesting_SCCs.find(i)!=interesting_SCCs.end())
1600  {
1601  int rc=pthread_join(threads[i], NULL);
1602  message.status()<<(rc!=0?"Failure ":"Success ")
1603  <<"in joining thread for SCC #"<<i<<messaget::eom;
1604  }
1605 
1606  delete[] threads;
1607 }
1608 #endif
unsigned goto2graph_cfg(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body)
goes through CFG and build a static abstract event graph overapproximating the read/write relations f...
Definition: goto2graph.cpp:87
const irep_idt & get_statement() const
Definition: std_code.h:39
#define add_all_pos(it, target, source)
Definition: goto2graph.h:183
void visit_cfg_duplicate(goto_programt::const_targett targ, goto_programt::const_targett i_it)
Definition: goto2graph.cpp:493
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
std::map< event_idt, event_idt > map_vertex_gnode
Definition: goto2graph.h:42
bool is_thread_local
Definition: symbol.h:67
std::size_t SCCs(std::vector< node_indext > &subgraph_nr) const
Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes...
Definition: graph.h:649
std::set< targett > incoming_edges
Definition: goto_program.h:226
std::set< irep_idt > var_to_instr
Definition: goto2graph.h:326
bool render_by_file
Definition: goto2graph.h:49
goto_functionst & goto_functions
Definition: goto2graph.h:39
#define CPROVER_PREFIX
messaget & message
Definition: goto2graph.h:279
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
event_idt add_node()
Definition: event_graph.h:407
void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:719
Definition: wmm.h:39
const irep_idt & get_function() const
entriest r_entries
Definition: rw_set.h:57
const irep_idt & get_identifier() const
Definition: std_expr.h:128
goto_programt body
Definition: goto_function.h:23
#define forall_rw_set_w_entries(it, rw_set)
Definition: rw_set.h:108
literalt pos(literalt a)
Definition: literal.h:193
void visit_cfg_skip(goto_programt::instructionst::iterator i_it)
function_mapt function_map
void add_po_edge(event_idt a, event_idt b)
Definition: event_graph.h:455
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void print_outputs(memory_modelt model, bool hide_internals)
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:374
loop_strategyt
Definition: wmm.h:36
bool is_static_lifetime
Definition: symbol.h:67
void visit_cfg_reference_function(irep_idt id_function)
references the first and last edges of the function
Definition: goto2graph.cpp:307
namespacet ns
Definition: goto2graph.h:36
data_typet::const_iterator const_iterator
Definition: event_graph.h:72
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:18
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
std::list< instructiont > instructionst
Definition: goto_program.h:395
void visit_cfg_function_call(value_setst &value_sets, goto_programt::instructionst::iterator i_it, memory_modelt model, bool no_dependenciess, loop_strategyt duplicate_body)
Definition: goto2graph.cpp:652
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:354
bool render_by_function
Definition: goto2graph.h:50
#define forall_rw_set_r_entries(it, rw_set)
Definition: rw_set.h:104
const wmm_grapht::edgest & po_out(event_idt n) const
Definition: event_graph.h:440
void visit_cfg_body(goto_programt::const_targett i_it, loop_strategyt replicate_body, value_setst &value_sets)
strategy: fwd/bwd alternation
Definition: goto2graph.cpp:448
virtual void visit_cfg_function(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function, const std::set< nodet > &initial_vertex, std::set< nodet > &ending_vertex)
TODO: move the visitor outside, and inherit.
Definition: goto2graph.cpp:147
std::pair< event_idt, event_idt > nodet
Definition: goto2graph.h:173
bool local(const irep_idt &id)
is local variable?
Definition: goto2graph.cpp:32
memory_modelt
Definition: wmm.h:17
const irep_idt & get_line() const
instructionst::iterator targett
Definition: goto_program.h:397
bool local(const irep_idt &i)
Definition: goto2graph.cpp:80
unsigned num_sccs
Definition: goto2graph.h:292
Instrumenter.
source_locationt source_location
Definition: message.h:214
messaget & message
Definition: message.h:213
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
#define INITIALIZE_FUNCTION
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
std::multimap< irep_idt, source_locationt > id2loc
Definition: goto2graph.h:327
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
dstring_hash irep_id_hash
Definition: irep.h:34
messaget & message
Definition: event_graph.h:396
event_idt alt_copy_segment(wmm_grapht &alt_egraph, event_idt begin, event_idt end)
Definition: goto2graph.cpp:390
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
event_idt copy_segment(event_idt begin, event_idt end)
Definition: event_graph.cpp:90
void visit_cfg_backedge(goto_programt::const_targett targ, goto_programt::const_targett i_it)
strategy: fwd/bwd alternation
Definition: goto2graph.cpp:557
std::size_t size() const
Definition: graph.h:178
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
std::map< irep_idt, goto_functiont > function_mapt
void add_po_back_edge(event_idt a, event_idt b)
Definition: event_graph.h:464
std::string get_operation() const
void visit_cfg(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function)
Definition: goto2graph.h:236
Definition: data_dp.h:24
void cfg_cycles_filter()
wmm_grapht::node_indext event_idt
Definition: event_graph.h:33
void print_outputs_local(const std::set< event_grapht::critical_cyclet > &set, std::ofstream &dot, std::ofstream &ref, std::ofstream &output, std::ofstream &all, std::ofstream &table, memory_modelt model, bool hide_internals)
The boolean constant false.
Definition: std_expr.h:4499
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
instrumentert & instrumenter
Definition: goto2graph.h:93
entriest w_entries
Definition: rw_set.h:57
bool is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
const irep_idt & get_file() const
bool contains_shared_array(goto_programt::const_targett targ, goto_programt::const_targett i_it, value_setst &value_sets) const
Definition: goto2graph.cpp:399
void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:751
static irep_idt entry_point()
node_indext add_node()
Definition: graph.h:146
mstreamt & status() const
Definition: message.h:317
exprt & function()
Definition: std_code.h:848
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
Fences for instrumentation.
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
void add_com_edge(event_idt a, event_idt b)
Definition: event_graph.h:475
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model, const std::set< event_idt > &filter)
Definition: event_graph.h:553
Base class for all expressions.
Definition: expr.h:42
virtual resultt run(const goto_functionst &goto_functions)
Definition: bmc.h:96
nodet::edgest edgest
Definition: graph.h:137
std::string to_string(const string_constraintt &expr)
Used for debug printing.
void add_edge(node_indext a, node_indext b)
Definition: graph.h:198
#define Forall_goto_functions(it, functions)
Definition: wmm.h:20
std::map< unsigned, data_dpt > map_data_dp
Definition: event_graph.h:399
event_grapht egraph
Definition: goto2graph.h:282
source_locationt source_location
void add_instr_to_interleaving(goto_programt::instructionst::iterator it, goto_programt &interleaving)
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
void clear(goto_program_instruction_typet _type)
Clear the node.
Definition: goto_program.h:233
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition: goto2graph.h:288
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Options.
Definition: wmm.h:40
mstreamt & debug() const
Definition: message.h:332
void visit_cfg_propagate(goto_programt::instructionst::iterator i_it)
Definition: goto2graph.cpp:285
wmm_grapht egraph_alt
Definition: goto2graph.h:43
std::pair< irep_idt, event_idt > id2node_pairt
Definition: goto2graph.h:164
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
mstreamt & statistics() const
Definition: message.h:322
void visit_cfg_fence(goto_programt::instructionst::iterator i_it)
std::vector< std::set< event_idt > > egraph_SCCs
Definition: goto2graph.h:285
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
void visit_cfg_assign(value_setst &value_sets, namespacet &ns, goto_programt::instructionst::iterator &i_it, bool no_dependencies)
Definition: goto2graph.cpp:791
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Definition: goto2graph.h:291
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Definition: fence.cpp:36
bool render_po_aligned
Definition: goto2graph.h:48
Definition: wmm.h:28
Race Detection for Threaded Goto Programs.
void visit_cfg_goto(goto_programt::instructionst::iterator i_it, loop_strategyt replicate_body, value_setst &value_sets)
Definition: goto2graph.cpp:623