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