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