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