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