31 #include "../rw_set.h" 52 identifier==
"stdin" ||
53 identifier==
"stdout" ||
54 identifier==
"stderr" ||
55 identifier==
"sys_nerr" ||
59 const size_t pos=identifier.find(
"[]");
61 if(
pos!=std::string::npos)
64 identifier.erase(
pos);
79 catch(std::string exception)
104 visitor.
visit_cfg(value_sets, model, no_dependencies, duplicate_body,
107 std::vector<std::size_t> subgraph_index;
111 for(std::map<event_idt, event_idt>::const_iterator
116 const std::size_t sg=subgraph_index[it->second];
124 unsigned interesting_sccs=0;
130 << interesting_sccs <<
" interesting SCCs" 141 std::size_t instr_counter=0;
142 for(goto_functionst::function_mapt::const_iterator
146 instr_counter+=it->second.body.instructions.size();
157 bool no_dependencies,
162 const std::set<instrumentert::cfg_visitort::nodet> &initial_vertex,
164 std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)
168 instrumenter.message.debug() <<
"visit function " 178 instrumenter.goto_functions.function_map[
function]);
183 instrumenter.goto_functions.function_map[
function].body)
185 goto_programt::instructiont &instruction=*i_it;
188 if(instruction.is_start_thread())
190 max_thread=max_thread+1;
191 coming_from=current_thread;
192 current_thread=max_thread;
194 else if(instruction.is_end_thread())
195 current_thread=coming_from;
196 thread=current_thread;
198 instrumenter.message.debug() <<
"visit instruction "<<instruction.type
201 if(instruction.is_start_thread() || instruction.is_end_thread())
206 else if(instruction.is_atomic_begin() || instruction.is_atomic_end())
211 #elif defined ATOMIC_FENCE 212 visit_cfg_fence(i_it);
215 visit_cfg_propagate(i_it);
219 else if(instruction.is_assign())
221 visit_cfg_assign(value_sets,
ns, i_it, no_dependencies
227 else if(
is_fence(instruction, instrumenter.ns))
229 instrumenter.message.debug() <<
"Constructing a fence" <<
messaget::eom;
230 visit_cfg_fence(i_it);
232 else if(model!=
TSO &&
is_lwfence(instruction, instrumenter.ns))
234 visit_cfg_lwfence(i_it);
236 else if(model==
TSO &&
is_lwfence(instruction, instrumenter.ns))
239 visit_cfg_skip(i_it);
241 else if(instruction.is_other()
242 && instruction.code.get_statement()==ID_fence)
244 visit_cfg_asm_fence(i_it);
246 else if(instruction.is_function_call())
248 visit_cfg_function_call(value_sets, i_it, model,
249 no_dependencies, replicate_body);
251 else if(instruction.is_goto())
253 visit_cfg_goto(i_it, replicate_body, value_sets
259 #ifdef CONTEXT_INSENSITIVE 260 else if(instruction.is_return())
262 visit_cfg_propagate(i_it);
263 add_all_pos(it, out_nodes[
function], in_pos[i_it]);
269 visit_cfg_propagate(i_it);
273 std::pair<unsigned, data_dpt> new_dp(thread, data_dp);
275 data_dp.print(instrumenter.message);
277 if(instrumenter.goto_functions.function_map[
function]
278 .body.instructions.empty())
284 goto_programt::instructionst::iterator it=instrumenter
285 .goto_functions.function_map[
function].body.instructions.end();
287 ending_vertex=in_pos[it];
292 goto_programt::instructionst::iterator i_it)
294 const goto_programt::instructiont &instruction=*i_it;
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);
316 if(instrumenter.map_function_graph.find(
id_function)!=
317 instrumenter.map_function_graph.end())
331 goto_programt::instructionst::iterator i_it=body.end();
335 goto_programt::instructionst::iterator targ=body.begin();
337 std::set<event_idt> in_nodes;
338 std::set<event_idt> out_nodes;
341 if(in_pos.find(targ)!=in_pos.end())
344 if(updated.find(targ)!=updated.end())
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);
356 instrumenter.message.debug() <<
"else case" <<
messaget::eom;
358 for(goto_programt::instructionst::iterator cur=i_it;
362 for(
const auto &in : cur->incoming_edges)
365 if(in_pos.find(in)!=in_pos.end() &&
366 updated.find(in)!=updated.end())
371 else if(in_pos.find(in)!=in_pos.end())
380 if(out_pos.find(targ)!=out_pos.end())
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);
393 std::make_pair(in_nodes, out_nodes);
414 instrumenter.message.debug() <<
"contains_shared_array called for " 415 << targ->source_location.get_line() <<
" and " 419 instrumenter.
message.
debug() <<
"Do we have an array at line " 426 instrumenter.message.debug() <<
"Writes: "<<rw_set.
w_entries.size()
431 const irep_idt var=r_it->second.object;
432 instrumenter.message.debug() <<
"Is "<<var<<
" an array?" 434 if(
id2string(var).find(
"[]")!=std::string::npos
435 && !instrumenter.local(var))
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))
464 for(
const auto &target : i_it->targets)
467 if(in_pos.find(target)!=in_pos.end())
469 if(in_pos[i_it].empty())
472 bool duplicate_this=
false;
474 switch(replicate_body)
477 duplicate_this=contains_shared_array(target, i_it, value_sets
487 duplicate_this=
false;
492 visit_cfg_duplicate(target, i_it);
494 visit_cfg_backedge(target, i_it);
503 instrumenter.message.status() <<
"Duplication..." <<
messaget::eom;
505 instrumenter.goto_functions.function_map[i_it->function];
507 bool found_pos=
false;
510 if(in_pos[targ].empty())
513 for(; new_targ!=fun.
body.instructions.end();
516 if(in_pos.find(new_targ)!=in_pos.end() && !in_pos[new_targ].empty())
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())
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];
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;
539 for(std::set<nodet>::const_iterator begin_it=down_set.begin();
540 begin_it!=down_set.end(); ++begin_it)
543 for(std::set<nodet>::const_iterator begin_it=up_set.begin();
544 begin_it!=up_set.end(); ++begin_it)
546 for(std::set<nodet>::const_iterator end_it=down_set.begin();
547 end_it!=down_set.end(); ++end_it)
568 if(updated.find(targ)!=updated.end())
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)
577 if(
egraph[from->first].thread!=
egraph[to->first].thread)
579 instrumenter.message.debug() << from->first <<
"-po->" 587 instrumenter.message.debug() <<
"else case" <<
messaget::eom;
593 for(
const auto &in : cur->incoming_edges)
595 if(in_pos.find(in)!=in_pos.end()
596 && updated.find(in)!=updated.end())
601 else if(in_pos.find(in)!=in_pos.end())
610 if(out_pos.find(targ)!=out_pos.end())
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)
618 if(
egraph[from->first].thread!=
egraph[to->first].thread)
620 instrumenter.message.debug() << from->first<<
"-po->" 630 goto_programt::instructionst::iterator i_it,
638 const goto_programt::instructiont &instruction=*i_it;
641 visit_cfg_propagate(i_it);
647 if(instruction.is_backwards_goto())
649 instrumenter.message.debug() <<
"backward goto" <<
messaget::eom;
650 visit_cfg_body(i_it, replicate_body, value_sets
660 goto_programt::instructionst::iterator i_it,
662 bool no_dependencies,
665 const goto_programt::instructiont &instruction=*i_it;
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])
677 enter_function(fun_id);
678 #ifdef CONTEXT_INSENSITIVE 679 stack_fun.push(cur_fun);
684 if(!inline_function_cond(fun_id))
688 if(instrumenter.map_function_graph.find(fun_id)!=
689 instrumenter.map_function_graph.end())
698 visit_cfg_function(value_sets, model, no_dependencies, fun_id, s,
700 updated.insert(i_it);
707 visit_cfg_function(value_sets, model, no_dependencies, replicate_body,
708 fun_id, s, in_pos[i_it]);
709 updated.insert(i_it);
712 leave_function(fun_id);
713 #ifdef CONTEXT_INSENSITIVE 714 cur_fun=stack_fun.pop();
719 instrumenter.message.warning() <<
"sorry, doesn't handle recursion " 720 <<
"(function " << fun_id <<
"; .cpp) " 726 goto_programt::instructionst::iterator i_it)
728 const goto_programt::instructiont &instruction=*i_it;
730 thread,
"f", instrumenter.unique_id++, instruction.source_location,
false);
732 egraph[new_fence_node](new_fence_event);
735 instrumenter.map_vertex_gnode.insert(
736 std::make_pair(new_fence_node, new_fence_gnode));
738 for(
const auto &in : instruction.incoming_edges)
739 if(in_pos.find(in)!=in_pos.end())
741 for(
const auto &node : in_pos[in])
743 if(
egraph[node.first].thread!=thread)
745 instrumenter.message.debug() << node.first<<
"-po->"<<new_fence_node
752 in_pos[i_it].clear();
753 in_pos[i_it].insert(
nodet(new_fence_node, new_fence_gnode));
754 updated.insert(i_it);
758 goto_programt::instructionst::iterator i_it)
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);
772 egraph[new_fence_node](new_fence_event);
775 instrumenter.map_vertex_gnode.insert(
776 std::make_pair(new_fence_node, new_fence_gnode));
778 for(
const auto &in : instruction.incoming_edges)
779 if(in_pos.find(in)!=in_pos.end())
781 for(
const auto &node : in_pos[in])
783 if(
egraph[node.first].thread!=thread)
785 instrumenter.message.debug() << node.first<<
"-po->"<<new_fence_node
792 in_pos[i_it].clear();
793 in_pos[i_it].insert(
nodet(new_fence_node, new_fence_gnode));
794 updated.insert(i_it);
800 goto_programt::instructionst::iterator &i_it,
807 goto_programt::instructiont &instruction=*i_it;
816 event_idt previous=std::numeric_limits<event_idt>::max();
817 event_idt previous_gnode=std::numeric_limits<event_idt>::max();
822 if(instruction.is_assert())
824 if(!instruction.labels.empty() && instruction.labels.front()==
"ASSERT")
834 const irep_idt &read=r_it->second.object;
846 thread,
id2string(read), instrumenter.unique_id++,
847 instruction.source_location,
local(read));
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
857 unknown_read_nodes.insert(new_read_node);
861 instrumenter.map_vertex_gnode.insert(
862 std::make_pair(new_read_node, new_read_gnode));
865 for(
const auto &in : instruction.incoming_edges)
867 if(in_pos.find(in)!=in_pos.end())
869 for(
const auto &node : in_pos[in])
871 if(
egraph[node.first].thread!=thread)
873 instrumenter.message.debug() << node.first<<
"-po->" 882 previous=new_read_node;
883 previous_gnode=new_read_gnode;
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++)
892 instrumenter.message.debug() << id_it->second<<
"<-com->" 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());
905 for(std::set<event_idt>::const_iterator id_it=
906 unknown_write_nodes.begin();
907 id_it!=unknown_write_nodes.end();
911 instrumenter.message.debug() << *id_it<<
"<-com->" 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());
931 const irep_idt &write=w_it->second.object;
933 instrumenter.message.debug() <<
"WRITE: " << write <<
messaget::eom;
944 thread,
id2string(write), instrumenter.unique_id++,
945 instruction.source_location,
local(write));
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
954 if(write==ID_unknown)
955 unknown_read_nodes.insert(new_write_node);
959 instrumenter.map_vertex_gnode.insert(
960 std::pair<event_idt, event_idt>(new_write_node, new_write_gnode));
963 if(previous!=std::numeric_limits<event_idt>::max())
965 instrumenter.message.debug() << previous<<
"-po->"<<new_write_node
972 for(
const auto &in : instruction.incoming_edges)
974 if(in_pos.find(in)!=in_pos.end())
976 for(
const auto &node : in_pos[in])
978 if(
egraph[node.first].thread!=thread)
980 instrumenter.message.debug() << node.first<<
"-po->" 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)
996 instrumenter.message.debug() <<idr_it->second<<
"<-com->" 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());
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)
1015 instrumenter.message.debug() << idw_it->second<<
"<-com->" 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());
1028 for(std::set<event_idt>::const_iterator id_it=
1029 unknown_write_nodes.begin();
1030 id_it!=unknown_write_nodes.end();
1034 instrumenter.message.debug() << *id_it<<
"<-com->" 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());
1047 for(std::set<event_idt>::const_iterator id_it=
1048 unknown_read_nodes.begin();
1049 id_it!=unknown_read_nodes.end();
1053 instrumenter.message.debug() << *id_it<<
"<-com->" 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());
1067 previous=new_write_node;
1068 previous_gnode=new_write_gnode;
1071 if(previous!=std::numeric_limits<event_idt>::max())
1073 in_pos[i_it].clear();
1074 in_pos[i_it].insert(
nodet(previous, previous_gnode));
1075 updated.insert(i_it);
1080 visit_cfg_skip(i_it);
1084 if(!no_dependencies)
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
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));
1102 const irep_idt &read2=read2_it->second.object;
1103 const irep_idt &read=read_it->second.object;
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));
1115 goto_programt::instructionst::iterator i_it)
1117 const goto_programt::instructiont &instruction=*i_it;
1119 thread,
"F", instrumenter.unique_id++, instruction.source_location,
false);
1121 egraph[new_fence_node](new_fence_event);
1124 instrumenter.map_vertex_gnode.insert(
1125 std::make_pair(new_fence_node, new_fence_gnode));
1127 for(
const auto &in : instruction.incoming_edges)
1128 if(in_pos.find(in)!=in_pos.end())
1130 for(
const auto &node : in_pos[in])
1132 instrumenter.message.debug() << node.first<<
"-po->"<<new_fence_node
1140 s.insert(
nodet(new_fence_node, new_fence_gnode));
1142 updated.insert(i_it);
1144 in_pos[i_it].clear();
1145 in_pos[i_it].insert(
nodet(new_fence_node, new_fence_gnode));
1146 updated.insert(i_it);
1150 goto_programt::instructionst::iterator i_it)
1152 visit_cfg_propagate(i_it);
1156 goto_programt::instructionst::iterator it,
1159 if(it->is_return() ||
1164 it->is_start_thread() ||
1165 it->is_end_thread())
1168 if(it->is_atomic_begin() ||
1169 it->is_atomic_end())
1175 if(it->is_function_call())
1183 goto_programt::instructiont new_instruction(*it);
1184 current_instruction->swap(new_instruction);
1192 for(event_grapht::critical_cyclet::const_iterator e_it=cyc.begin();
1193 e_it!=cyc.end() && ++e_it!=cyc.end(); ++e_it)
1202 bool thread_found=
false;
1207 if(p_it->source_location==current_location)
1209 current_po=&f_it->second.body;
1223 bool exists_n=
false;
1225 for(wmm_grapht::edgest::const_iterator edge_it=pos_cur.begin();
1226 edge_it!=pos_cur.end(); edge_it++)
1228 if(pos_next.find(edge_it->first)!=pos_next.end())
1236 if((++e_it)!=cyc.end() || !exists_n)
1242 if(i_it->source_location==current_location)
1245 for(goto_programt::instructionst::iterator same_loc=i_it;
1247 && same_loc->source_location==i_it->source_location;
1261 bool in_cycle=
false;
1264 if(it->source_location==current_location)
1269 if(it->source_location==next_location)
1281 if(int_it->is_goto())
1283 for(
const auto &t : int_it->targets)
1285 bool target_in_cycle=
false;
1290 target_in_cycle=
true;
1294 if(!target_in_cycle)
1306 map.insert(std::make_pair(
1308 std::move(one_interleaving)));
1316 bmct bmc(no_option, symbol_table, no_message);
1318 bool is_spurious=bmc.
run(this_interleaving);
1332 for(std::set<event_grapht::critical_cyclet>::iterator
1338 std::set<event_grapht::critical_cyclet>::iterator next=it;
1353 for(std::set<event_grapht::critical_cyclet>::iterator it=
1359 std::set<event_grapht::critical_cyclet>::iterator next=it;
1376 const std::set<event_grapht::critical_cyclet> &
set,
1379 std::ofstream &output,
1381 std::ofstream &table,
1383 bool hide_internals)
1386 std::map<unsigned, std::set<event_idt> > same_po;
1387 unsigned max_thread=0;
1391 std::map<irep_idt, std::set<event_idt> > same_file;
1394 std::map<std::string, std::string> map_id2var;
1395 std::map<std::string, std::string> map_var2id;
1397 for(std::set<event_grapht::critical_cyclet>::const_iterator it =
1398 set.begin(); it!=
set.end(); it++)
1400 #ifdef PRINT_UNSAFES 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)
1410 for(std::list<event_idt>::const_iterator it_e=it->begin();
1411 it_e!=it->end(); it_e++)
1416 same_po[ev.
thread].insert(*it_e);
1427 dot << ev.
id <<
"[label=\"\\\\lb {" << ev.
id <<
"}";
1429 dot << ev.
thread <<
"\",color=red,shape=box];\n";
1437 for(
unsigned i=0; i<=max_thread; i++)
1438 if(!same_po[i].empty())
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++)
1452 for(std::map<
irep_idt, std::set<event_idt> >::const_iterator it=
1454 it!=same_file.end(); it++)
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++)
1461 dot <<
" " <<
egraph[*ev_it].id <<
";\n";
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();
1474 table <<
"\n| " << m_it->first <<
" : " << m_it->second;
1477 table << std::string(80,
'-');
1485 std::ofstream output;
1487 std::ofstream table;
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");
1495 dot <<
"digraph G {\n";
1496 dot <<
"nodesep=1; ranksep=1;\n";
1501 model, hide_internals);
1506 std::ofstream local_dot;
1507 std::string name=
"scc_" + std::to_string(i) +
".dot";
1508 local_dot.open(name.c_str());
1510 local_dot <<
"digraph G {\n";
1511 local_dot <<
"nodesep=1; ranksep=1;\n";
1513 table, model, hide_internals);
1517 dot << i <<
"[label=\"SCC " << i <<
"\",link=\"" <<
"scc_" << i;
1540 std::set<event_grapht::critical_cyclet>());
1541 for(std::vector<std::set<event_idt> >::const_iterator it=
egraph_SCCs.begin();
1547 class pthread_argumentt
1552 const std::set<event_idt> &filter;
1553 std::set<event_grapht::critical_cyclet> &cycles;
1557 const std::set<event_idt> &_filter,
1558 std::set<event_grapht::critical_cyclet> &_cycles)
1559 :instr(_instr), mem(_mem), filter(_filter), cycles(_cycles)
1565 void *collect_cycles_in_thread(
void *arg)
1568 pthread_argumentt *p_arg=
reinterpret_cast<pthread_argumentt*
>(arg);
1571 const std::set<event_idt> &filter=p_arg->filter;
1572 std::set<event_grapht::critical_cyclet> &cycles=p_arg->cycles;
1581 const unsigned number_of_sccs=
num_sccs;
1582 std::set<unsigned> interesting_SCCs;
1585 pthread_t *threads=
new pthread_t[
num_sccs+1];
1588 std::set<event_grapht::critical_cyclet>());
1590 for(std::vector<std::set<unsigned> >::const_iterator it=
egraph_SCCs.begin();
1594 interesting_SCCs.insert(scc);
1597 int rc=pthread_create(&threads[scc++], NULL,
1598 collect_cycles_in_thread, &arg);
1604 for(
unsigned i=0; i<number_of_sccs; i++)
1605 if(interesting_SCCs.find(i)!=interesting_SCCs.end())
1607 int rc=pthread_join(threads[i], NULL);
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...
std::map< irep_idt, goto_functiont > function_mapt
#define add_all_pos(it, target, source)
void visit_cfg_duplicate(goto_programt::const_targett targ, goto_programt::const_targett i_it)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
targett add_instruction()
Adds an instruction at the end.
const std::string & id2string(const irep_idt &d)
std::map< event_idt, event_idt > map_vertex_gnode
std::list< instructiont > instructionst
std::set< irep_idt > var_to_instr
goto_functionst & goto_functions
void visit_cfg_thread() const
std::size_t SCCs(std::vector< node_indext > &subgraph_nr)
instructionst instructions
The list of instructions in the goto program.
void visit_cfg_lwfence(goto_programt::instructionst::iterator i_it)
const irep_idt & get_function() const
const irep_idt & get_identifier() const
#define forall_rw_set_w_entries(it, rw_set)
void visit_cfg_skip(goto_programt::instructionst::iterator i_it)
void add_po_edge(event_idt a, event_idt b)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
void print_outputs(memory_modelt model, bool hide_internals)
void visit_cfg_reference_function(irep_idt id_function)
references the first and last edges of the function
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
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)
#define forall_rw_set_r_entries(it, rw_set)
const wmm_grapht::edgest & po_out(event_idt n) const
void visit_cfg_body(goto_programt::const_targett i_it, loop_strategyt replicate_body, value_setst &value_sets)
strategy: fwd/bwd alternation
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.
std::pair< event_idt, event_idt > nodet
bool local(const irep_idt &id)
is local variable?
const irep_idt & get_line() const
bool local(const irep_idt &i)
source_locationt source_location
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
static irep_idt entry_point()
API to expression classes.
std::multimap< irep_idt, source_locationt > id2loc
dstring_hash irep_id_hash
event_idt alt_copy_segment(wmm_grapht &alt_egraph, event_idt begin, event_idt end)
event_idt copy_segment(event_idt begin, event_idt end)
void visit_cfg_backedge(goto_programt::const_targett targ, goto_programt::const_targett i_it)
strategy: fwd/bwd alternation
virtual resultt run(const goto_functionst &goto_functions)
void add_po_back_edge(event_idt a, event_idt b)
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)
function_mapt function_map
wmm_grapht::node_indext event_idt
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.
bool has_prefix(const std::string &s, const std::string &prefix)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
instrumentert & instrumenter
bool is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
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
void visit_cfg_asm_fence(goto_programt::instructionst::iterator i_it)
void copy_from(const goto_program_templatet< codeT, guardT > &src)
Copy a full goto program, preserving targets.
Fences for instrumentation.
void add_com_edge(event_idt a, event_idt b)
void collect_cycles(std::set< critical_cyclet > &set_of_cycles, memory_modelt model, const std::set< event_idt > &filter)
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void add_edge(node_indext a, node_indext b)
#define Forall_goto_functions(it, functions)
std::map< unsigned, data_dpt > map_data_dp
source_locationt source_location
void add_instr_to_interleaving(goto_programt::instructionst::iterator it, goto_programt &interleaving)
void dot(const goto_functionst &src, const namespacet &ns, std::ostream &out)
std::set< event_grapht::critical_cyclet > set_of_cycles
#define Forall_goto_program_instructions(it, program)
void visit_cfg_propagate(goto_programt::instructionst::iterator i_it)
std::pair< irep_idt, event_idt > id2node_pairt
#define forall_goto_program_instructions(it, program)
void visit_cfg_fence(goto_programt::instructionst::iterator i_it)
std::vector< std::set< event_idt > > egraph_SCCs
void visit_cfg_assign(value_setst &value_sets, namespacet &ns, goto_programt::instructionst::iterator &i_it, bool no_dependencies)
const code_function_callt & to_code_function_call(const codet &code)
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
instructionst::iterator targett
void visit_cfg_goto(goto_programt::instructionst::iterator i_it, loop_strategyt replicate_body, value_setst &value_sets)