47 identifier==
"stdin" ||
48 identifier==
"stdout" ||
49 identifier==
"stderr" ||
50 identifier==
"sys_nerr" ||
54 const size_t pos=identifier.find(
"[]");
56 if(
pos!=std::string::npos)
59 identifier.erase(
pos);
74 catch(
const std::string &exception)
99 visitor.
visit_cfg(value_sets, model, no_dependencies, duplicate_body,
102 std::vector<std::size_t> subgraph_index;
106 for(std::map<event_idt, event_idt>::const_iterator
111 const std::size_t sg=subgraph_index[it->second];
119 unsigned interesting_sccs=0;
125 << interesting_sccs <<
" interesting SCCs"
136 std::size_t instr_counter=0;
137 for(goto_functionst::function_mapt::const_iterator
141 instr_counter+=it->second.body.instructions.size();
151 bool no_dependencies,
154 std::set<instrumentert::cfg_visitort::nodet> &ending_vertex)
158 instrumenter.message.debug()
168 instrumenter.goto_functions.function_map[function_id]);
173 instrumenter.goto_functions.function_map[function_id].body;
181 max_thread=max_thread+1;
182 coming_from=current_thread;
183 current_thread=max_thread;
186 current_thread=coming_from;
187 thread=current_thread;
189 instrumenter.message.debug() <<
"visit instruction "<<instruction.
type
202 #elif defined ATOMIC_FENCE
203 visit_cfg_fence(i_it, function_id);
206 visit_cfg_propagate(i_it);
223 else if(
is_fence(instruction, instrumenter.ns))
225 instrumenter.message.debug() <<
"Constructing a fence" <<
messaget::eom;
226 visit_cfg_fence(i_it, function_id);
228 else if(model!=
TSO &&
is_lwfence(instruction, instrumenter.ns))
230 visit_cfg_lwfence(i_it, function_id);
232 else if(model==
TSO &&
is_lwfence(instruction, instrumenter.ns))
235 visit_cfg_skip(i_it);
240 visit_cfg_asm_fence(i_it, function_id);
244 visit_cfg_function_call(value_sets, i_it, model,
245 no_dependencies, replicate_body);
261 #ifdef CONTEXT_INSENSITIVE
264 visit_cfg_propagate(i_it);
265 add_all_pos(it, out_nodes[function_id], in_pos[i_it]);
271 visit_cfg_propagate(i_it);
275 std::pair<unsigned, data_dpt> new_dp(thread, data_dp);
277 data_dp.print(instrumenter.message);
279 if(instrumenter.goto_functions.function_map[function_id]
280 .body.instructions.empty())
286 goto_programt::instructionst::iterator it =
287 instrumenter.goto_functions.function_map[function_id]
288 .body.instructions.end();
290 ending_vertex=in_pos[it];
295 goto_programt::instructionst::iterator i_it)
299 in_pos[i_it].
clear();
301 if(in_pos.find(in)!=in_pos.end())
302 for(
const auto &node : in_pos[in])
303 in_pos[i_it].insert(node);
319 if(instrumenter.map_function_graph.find(id_function)!=
320 instrumenter.map_function_graph.end())
325 .function_map[id_function].body.instructions;
334 goto_programt::instructionst::iterator i_it=body.end();
338 goto_programt::instructionst::iterator targ=body.begin();
340 std::set<event_idt> in_nodes;
341 std::set<event_idt> out_nodes;
344 if(in_pos.find(targ)!=in_pos.end())
347 if(updated.find(targ)!=updated.end())
350 for(std::set<nodet>::const_iterator to=in_pos[targ].begin();
351 to!=in_pos[targ].end(); ++to)
352 in_nodes.insert(to->first);
353 for(std::set<nodet>::const_iterator from=in_pos[i_it].begin();
354 from!=in_pos[i_it].end(); ++from)
355 out_nodes.insert(from->first);
359 instrumenter.message.debug() <<
"else case" <<
messaget::eom;
361 for(goto_programt::instructionst::iterator cur=i_it;
365 for(
const auto &in : cur->incoming_edges)
368 if(in_pos.find(in)!=in_pos.end() &&
369 updated.find(in)!=updated.end())
374 else if(in_pos.find(in)!=in_pos.end())
383 if(out_pos.find(targ)!=out_pos.end())
385 for(std::set<nodet>::const_iterator to=out_pos[targ].begin();
386 to!=out_pos[targ].end(); ++to)
387 in_nodes.insert(to->first);
388 for(std::set<nodet>::const_iterator from=in_pos[i_it].begin();
389 from!=in_pos[i_it].end(); ++from)
390 out_nodes.insert(from->first);
395 instrumenter.map_function_graph[id_function]=
396 std::make_pair(in_nodes, out_nodes);
419 instrumenter.message.debug() <<
"contains_shared_array called for "
420 << targ->source_location.get_line() <<
" and "
424 instrumenter.message.debug() <<
"Do we have an array at line "
436 instrumenter.message.debug() <<
"Writes: "<<rw_set.
w_entries.size()
441 const irep_idt var=r_it->second.object;
442 instrumenter.message.debug() <<
"Is "<<var<<
" an array?"
444 if(
id2string(var).find(
"[]")!=std::string::npos
445 && !instrumenter.local(var))
451 const irep_idt var=w_it->second.object;
452 instrumenter.message.debug()<<
"Is "<<var<<
" an array?"<<
messaget::eom;
453 if(
id2string(var).find(
"[]")!=std::string::npos
454 && !instrumenter.local(var))
477 for(
const auto &target : i_it->targets)
480 if(in_pos.find(target)!=in_pos.end())
482 if(in_pos[i_it].empty())
485 bool duplicate_this=
false;
487 switch(replicate_body)
490 duplicate_this = contains_shared_array(
505 duplicate_this=
false;
510 visit_cfg_duplicate(goto_program, target, i_it);
512 visit_cfg_backedge(target, i_it);
522 instrumenter.message.status() <<
"Duplication..." <<
messaget::eom;
524 bool found_pos=
false;
527 if(in_pos[targ].empty())
530 for(; new_targ != goto_program.
instructions.end(); ++new_targ)
532 if(in_pos.find(new_targ)!=in_pos.end() && !in_pos[new_targ].empty())
543 || new_targ->source_location.get_function()
544 !=targ->source_location.get_function()
545 || new_targ->source_location.get_file()
546 !=targ->source_location.get_file())
551 const std::set<nodet> &up_set=in_pos[(found_pos ? new_targ : targ)];
552 const std::set<nodet> &down_set=in_pos[i_it];
554 for(std::set<nodet>::const_iterator begin_it=up_set.begin();
555 begin_it!=up_set.end(); ++begin_it)
556 instrumenter.message.debug() <<
"Up " << begin_it->first <<
messaget::eom;
558 for(std::set<nodet>::const_iterator begin_it=down_set.begin();
559 begin_it!=down_set.end(); ++begin_it)
560 instrumenter.message.debug() <<
"Down " << begin_it->first <<
messaget::eom;
562 for(std::set<nodet>::const_iterator begin_it=up_set.begin();
563 begin_it!=up_set.end(); ++begin_it)
565 for(std::set<nodet>::const_iterator end_it=down_set.begin();
566 end_it!=down_set.end(); ++end_it)
587 if(updated.find(targ)!=updated.end())
590 for(std::set<nodet>::const_iterator to=in_pos[targ].begin();
591 to!=in_pos[targ].end(); ++to)
592 for(std::set<nodet>::const_iterator from=in_pos[i_it].begin();
593 from!=in_pos[i_it].end(); ++from)
594 if(from->first!=to->first)
596 if(
egraph[from->first].thread!=
egraph[to->first].thread)
598 instrumenter.message.debug() << from->first <<
"-po->"
606 instrumenter.message.debug() <<
"else case" <<
messaget::eom;
612 for(
const auto &in : cur->incoming_edges)
614 if(in_pos.find(in)!=in_pos.end()
615 && updated.find(in)!=updated.end())
620 else if(in_pos.find(in)!=in_pos.end())
629 if(out_pos.find(targ)!=out_pos.end())
631 for(std::set<nodet>::const_iterator to=out_pos[targ].begin();
632 to!=out_pos[targ].end(); ++to)
633 for(std::set<nodet>::const_iterator from=in_pos[i_it].begin();
634 from!=in_pos[i_it].end(); ++from)
635 if(from->first!=to->first)
637 if(
egraph[from->first].thread!=
egraph[to->first].thread)
639 instrumenter.message.debug() << from->first<<
"-po->"
651 goto_programt::instructionst::iterator i_it,
663 visit_cfg_propagate(i_it);
671 instrumenter.message.debug() <<
"backward goto" <<
messaget::eom;
688 goto_programt::instructionst::iterator i_it,
690 bool no_dependencies,
700 enter_function(fun_id);
701 #ifdef CONTEXT_INSENSITIVE
702 stack_fun.push(cur_fun);
707 if(!inline_function_cond(fun_id))
711 if(instrumenter.map_function_graph.find(fun_id)!=
712 instrumenter.map_function_graph.end())
721 visit_cfg_function(value_sets, model, no_dependencies, fun_id,
723 updated.insert(i_it);
730 visit_cfg_function(value_sets, model, no_dependencies, replicate_body,
731 fun_id, in_pos[i_it]);
732 updated.insert(i_it);
735 leave_function(fun_id);
736 #ifdef CONTEXT_INSENSITIVE
737 cur_fun=stack_fun.pop();
740 catch(
const std::string &s)
742 instrumenter.message.warning() <<
"sorry, doesn't handle recursion "
743 <<
"(function " << fun_id <<
"; .cpp) "
749 goto_programt::instructionst::iterator i_it,
757 instrumenter.unique_id++,
762 egraph[new_fence_node](new_fence_event);
765 instrumenter.map_vertex_gnode.insert(
766 std::make_pair(new_fence_node, new_fence_gnode));
769 if(in_pos.find(in)!=in_pos.end())
771 for(
const auto &node : in_pos[in])
773 if(
egraph[node.first].thread!=thread)
775 instrumenter.message.debug() << node.first<<
"-po->"<<new_fence_node
782 in_pos[i_it].clear();
783 in_pos[i_it].insert(
nodet(new_fence_node, new_fence_gnode));
784 updated.insert(i_it);
788 goto_programt::instructionst::iterator i_it,
803 instrumenter.unique_id++,
815 egraph[new_fence_node](new_fence_event);
818 instrumenter.map_vertex_gnode.insert(
819 std::make_pair(new_fence_node, new_fence_gnode));
822 if(in_pos.find(in)!=in_pos.end())
824 for(
const auto &node : in_pos[in])
826 if(
egraph[node.first].thread!=thread)
828 instrumenter.message.debug() << node.first<<
"-po->"<<new_fence_node
835 in_pos[i_it].clear();
836 in_pos[i_it].insert(
nodet(new_fence_node, new_fence_gnode));
837 updated.insert(i_it);
843 goto_programt::instructionst::iterator &i_it,
865 event_idt previous=std::numeric_limits<event_idt>::max();
866 event_idt previous_gnode=std::numeric_limits<event_idt>::max();
873 if(!instruction.
labels.empty() && instruction.
labels.front()==
"ASSERT")
883 const irep_idt &read=r_it->second.object;
898 instrumenter.unique_id++,
904 egraph[new_read_node]=new_read_event;
905 instrumenter.message.debug() <<
"new Read"<<read<<
" @thread"
907 <<(
local(read)?
"local":
"shared")<<
") #"<<new_read_node
911 unknown_read_nodes.insert(new_read_node);
915 instrumenter.map_vertex_gnode.insert(
916 std::make_pair(new_read_node, new_read_gnode));
921 if(in_pos.find(in)!=in_pos.end())
923 for(
const auto &node : in_pos[in])
925 if(
egraph[node.first].thread!=thread)
927 instrumenter.message.debug() << node.first<<
"-po->"
936 previous=new_read_node;
937 previous_gnode=new_read_gnode;
940 const std::pair<id2nodet::iterator, id2nodet::iterator>
941 with_same_var=map_writes.equal_range(read);
942 for(id2nodet::iterator id_it=with_same_var.first;
943 id_it!=with_same_var.second; id_it++)
946 instrumenter.message.debug() << id_it->second<<
"<-com->"
948 std::map<event_idt, event_idt>::const_iterator entry=
949 instrumenter.map_vertex_gnode.find(id_it->second);
950 assert(entry!=instrumenter.map_vertex_gnode.end());
959 for(std::set<event_idt>::const_iterator id_it=
960 unknown_write_nodes.begin();
961 id_it!=unknown_write_nodes.end();
965 instrumenter.message.debug() << *id_it<<
"<-com->"
967 std::map<event_idt, event_idt>::const_iterator entry=
968 instrumenter.map_vertex_gnode.find(*id_it);
969 assert(entry!=instrumenter.map_vertex_gnode.end());
985 const irep_idt &write=w_it->second.object;
987 instrumenter.message.debug() <<
"WRITE: " << write <<
messaget::eom;
1001 instrumenter.unique_id++,
1007 egraph[new_write_node](new_write_event);
1008 instrumenter.
message.
debug() <<
"new Write "<<write<<
" @thread"<<(thread)
1010 << (
local(write)?
"local":
"shared")<<
") #"<<new_write_node
1013 if(write==ID_unknown)
1014 unknown_read_nodes.insert(new_write_node);
1018 instrumenter.map_vertex_gnode.insert(
1019 std::pair<event_idt, event_idt>(new_write_node, new_write_gnode));
1022 if(previous!=std::numeric_limits<event_idt>::max())
1024 instrumenter.message.debug() << previous<<
"-po->"<<new_write_node
1033 if(in_pos.find(in)!=in_pos.end())
1035 for(
const auto &node : in_pos[in])
1037 if(
egraph[node.first].thread!=thread)
1039 instrumenter.message.debug() << node.first<<
"-po->"
1049 const std::pair<id2nodet::iterator, id2nodet::iterator>
1050 r_with_same_var=map_reads.equal_range(write);
1051 for(id2nodet::iterator idr_it=r_with_same_var.first;
1052 idr_it!=r_with_same_var.second; idr_it++)
1053 if(
egraph[idr_it->second].thread!=new_write_event.
thread)
1055 instrumenter.message.debug() <<idr_it->second<<
"<-com->"
1057 std::map<event_idt, event_idt>::const_iterator entry=
1058 instrumenter.map_vertex_gnode.find(idr_it->second);
1059 assert(entry!=instrumenter.map_vertex_gnode.end());
1068 const std::pair<id2nodet::iterator, id2nodet::iterator>
1069 w_with_same_var=map_writes.equal_range(write);
1070 for(id2nodet::iterator idw_it=w_with_same_var.first;
1071 idw_it!=w_with_same_var.second; idw_it++)
1072 if(
egraph[idw_it->second].thread!=new_write_event.
thread)
1074 instrumenter.message.debug() << idw_it->second<<
"<-com->"
1076 std::map<event_idt, event_idt>::const_iterator entry=
1077 instrumenter.map_vertex_gnode.find(idw_it->second);
1078 assert(entry!=instrumenter.map_vertex_gnode.end());
1087 for(std::set<event_idt>::const_iterator id_it=
1088 unknown_write_nodes.begin();
1089 id_it!=unknown_write_nodes.end();
1093 instrumenter.message.debug() << *id_it<<
"<-com->"
1095 std::map<event_idt, event_idt>::const_iterator entry=
1096 instrumenter.map_vertex_gnode.find(*id_it);
1097 assert(entry!=instrumenter.map_vertex_gnode.end());
1106 for(std::set<event_idt>::const_iterator id_it=
1107 unknown_read_nodes.begin();
1108 id_it!=unknown_read_nodes.end();
1112 instrumenter.message.debug() << *id_it<<
"<-com->"
1114 std::map<event_idt, event_idt>::const_iterator entry=
1115 instrumenter.map_vertex_gnode.find(*id_it);
1116 assert(entry!=instrumenter.map_vertex_gnode.end());
1126 previous=new_write_node;
1127 previous_gnode=new_write_gnode;
1130 if(previous!=std::numeric_limits<event_idt>::max())
1132 in_pos[i_it].clear();
1133 in_pos[i_it].insert(
nodet(previous, previous_gnode));
1134 updated.insert(i_it);
1139 visit_cfg_skip(i_it);
1143 if(!no_dependencies)
1148 const irep_idt &write=write_it->second.object;
1149 const irep_idt &read=read_it->second.object;
1150 instrumenter.message.debug() <<
"dp: Write:"<<write<<
"; Read:"<<read
1154 data_dp.dp_analysis(read_p,
local(read), write_p,
local(write));
1161 const irep_idt &read2=read2_it->second.object;
1162 const irep_idt &read=read_it->second.object;
1167 data_dp.dp_analysis(read_p,
local(read), read2_p,
local(read2));
1174 goto_programt::instructionst::iterator i_it,
1182 instrumenter.unique_id++,
1187 egraph[new_fence_node](new_fence_event);
1190 instrumenter.map_vertex_gnode.insert(
1191 std::make_pair(new_fence_node, new_fence_gnode));
1194 if(in_pos.find(in)!=in_pos.end())
1196 for(
const auto &node : in_pos[in])
1198 instrumenter.message.debug() << node.first<<
"-po->"<<new_fence_node
1206 s.insert(
nodet(new_fence_node, new_fence_gnode));
1208 updated.insert(i_it);
1210 in_pos[i_it].clear();
1211 in_pos[i_it].insert(
nodet(new_fence_node, new_fence_gnode));
1212 updated.insert(i_it);
1216 goto_programt::instructionst::iterator i_it)
1218 visit_cfg_propagate(i_it);
1222 goto_programt::instructionst::iterator it,
1225 if(it->is_return() ||
1230 it->is_start_thread() ||
1231 it->is_end_thread())
1234 if(it->is_atomic_begin() ||
1235 it->is_atomic_end())
1241 if(it->is_function_call())
1257 e_it!=cyc.
end() && ++e_it!=cyc.
end(); ++e_it)
1266 bool thread_found=
false;
1271 if(p_it->source_location==current_location)
1273 current_po=&f_it->second.body;
1287 bool exists_n=
false;
1289 for(wmm_grapht::edgest::const_iterator edge_it=pos_cur.begin();
1290 edge_it!=pos_cur.end(); edge_it++)
1292 if(pos_next.find(edge_it->first)!=pos_next.end())
1300 if((++e_it)!=cyc.
end() || !exists_n)
1306 if(i_it->source_location==current_location)
1309 for(goto_programt::instructionst::iterator same_loc=i_it;
1311 && same_loc->source_location==i_it->source_location;
1325 bool in_cycle=
false;
1328 if(it->source_location==current_location)
1333 if(it->source_location==next_location)
1345 if(int_it->is_goto())
1347 for(
const auto &t : int_it->targets)
1349 bool target_in_cycle=
false;
1354 target_in_cycle=
true;
1358 if(!target_in_cycle)
1371 map.insert(std::make_pair(
1373 std::move(one_interleaving)));
1381 bmct bmc(no_option, symbol_table, no_message);
1383 bool is_spurious=bmc.run(this_interleaving);
1397 for(std::set<event_grapht::critical_cyclet>::iterator
1403 std::set<event_grapht::critical_cyclet>::iterator next=it;
1418 for(std::set<event_grapht::critical_cyclet>::iterator it=
1424 std::set<event_grapht::critical_cyclet>::iterator next=it;
1441 const std::set<event_grapht::critical_cyclet> &set,
1444 std::ofstream &output,
1446 std::ofstream &table,
1448 bool hide_internals)
1451 std::map<unsigned, std::set<event_idt> > same_po;
1452 unsigned max_thread=0;
1456 std::map<irep_idt, std::set<event_idt> > same_file;
1459 std::map<std::string, std::string> map_id2var;
1460 std::map<std::string, std::string> map_var2id;
1462 for(std::set<event_grapht::critical_cyclet>::const_iterator it =
1463 set.begin(); it!=set.end(); it++)
1465 #ifdef PRINT_UNSAFES
1468 it->print_dot(
dot, colour++, model);
1469 ref << it->print_name(model, hide_internals) <<
'\n';
1470 output << it->print_output() <<
'\n';
1471 all << it->print_all(model, map_id2var, map_var2id, hide_internals)
1475 for(std::list<event_idt>::const_iterator it_e=it->begin();
1476 it_e!=it->end(); it_e++)
1481 same_po[ev.
thread].insert(*it_e);
1492 dot << ev.
id <<
"[label=\"\\\\lb {" << ev.
id <<
"}";
1494 dot << ev.
thread <<
"\",color=red,shape=box];\n";
1502 for(
unsigned i=0; i<=max_thread; i++)
1503 if(!same_po[i].empty())
1505 dot <<
"{rank=same; thread_" << i
1506 <<
"[shape=plaintext, label=\"thread " << i <<
"\"];";
1507 for(std::set<event_idt>::iterator it=same_po[i].begin();
1508 it!=same_po[i].end(); it++)
1517 for(std::map<
irep_idt, std::set<event_idt> >::const_iterator it=
1519 it!=same_file.end(); it++)
1522 dot <<
" label=\"" << it->first <<
"\";\n";
1523 for(std::set<event_idt>::const_iterator ev_it=it->second.begin();
1524 ev_it!=it->second.end(); ev_it++)
1526 dot <<
" " <<
egraph[*ev_it].id <<
";\n";
1533 table << std::string(80,
'-');
1534 for(std::map<std::string, std::string>::const_iterator
1535 m_it=map_id2var.begin();
1536 m_it!=map_id2var.end();
1539 table <<
"\n| " << m_it->first <<
" : " << m_it->second;
1542 table << std::string(80,
'-');
1550 std::ofstream output;
1552 std::ofstream table;
1554 dot.open(
"cycles.dot");
1555 ref.open(
"ref.txt");
1556 output.open(
"output.txt");
1557 all.open(
"all.txt");
1558 table.open(
"table.txt");
1560 dot <<
"digraph G {\n";
1561 dot <<
"nodesep=1; ranksep=1;\n";
1566 model, hide_internals);
1571 std::ofstream local_dot;
1573 local_dot.open(name.c_str());
1575 local_dot <<
"digraph G {\n";
1576 local_dot <<
"nodesep=1; ranksep=1;\n";
1578 table, model, hide_internals);
1582 dot << i <<
"[label=\"SCC " << i <<
"\",link=\"" <<
"scc_" << i;
1605 std::set<event_grapht::critical_cyclet>());
1606 for(std::vector<std::set<event_idt> >::const_iterator it=
egraph_SCCs.begin();
1612 class pthread_argumentt
1617 const std::set<event_idt> &filter;
1618 std::set<event_grapht::critical_cyclet> &cycles;
1622 const std::set<event_idt> &_filter,
1623 std::set<event_grapht::critical_cyclet> &_cycles)
1624 :instr(_instr), mem(_mem), filter(_filter), cycles(_cycles)
1630 void *collect_cycles_in_thread(
void *arg)
1633 pthread_argumentt *p_arg=
reinterpret_cast<pthread_argumentt*
>(arg);
1636 const std::set<event_idt> &filter=p_arg->filter;
1637 std::set<event_grapht::critical_cyclet> &cycles=p_arg->cycles;
1646 const unsigned number_of_sccs=
num_sccs;
1647 std::set<unsigned> interesting_SCCs;
1650 pthread_t *threads=
new pthread_t[
num_sccs+1];
1653 std::set<event_grapht::critical_cyclet>());
1655 for(std::vector<std::set<unsigned> >::const_iterator it=
egraph_SCCs.begin();
1659 interesting_SCCs.insert(scc);
1662 int rc=pthread_create(&threads[scc++], NULL,
1663 collect_cycles_in_thread, &arg);
1669 for(
unsigned i=0; i<number_of_sccs; i++)
1670 if(interesting_SCCs.find(i)!=interesting_SCCs.end())
1672 int rc=pthread_join(threads[i], NULL);