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