33 var_mapt::const_iterator it=
var_map.find(
object);
73 const std::string &suffix,
92 return new_symbol.
name;
100 for(
const auto &vars :
var_map)
105 assignment(goto_program, t, source_location, vars.second.w_buff0_used,
107 assignment(goto_program, t, source_location, vars.second.w_buff1_used,
109 assignment(goto_program, t, source_location, vars.second.flush_delayed,
111 assignment(goto_program, t, source_location, vars.second.read_delayed,
113 assignment(goto_program, t, source_location, vars.second.read_delayed_var,
116 for(
const auto &
id : vars.second.r_buff0_thds)
119 for(
const auto &
id : vars.second.r_buff1_thds)
128 goto_functionst::function_mapt::iterator
132 throw "weak memory instrumentation needs an entry point";
147 std::string identifier=
id2string(id_lhs);
149 const size_t pos=identifier.find(
"[]");
151 if(
pos!=std::string::npos)
154 identifier.erase(
pos);
159 const exprt symbol=ns.
lookup(identifier).symbol_expr();
164 t->code_nonconst().add_source_location() = source_location;
165 t->source_location=source_location;
171 catch(
const std::string &s)
189 assignment(goto_program, target, source_location, vars.read_delayed,
191 assignment(goto_program, target, source_location, vars.read_delayed_var,
196 assignment(goto_program, target, source_location, vars.read_new_var, new_var);
199 assignment(goto_program, target, source_location, write_object, new_var);
205 const std::string identifier=
id2string(write_object);
208 const varst &vars=(*this)(write_object);
235 const varst &vars=(*this)(write_object);
247 target->guard=if_expr;
249 target->source_location=source_location;
261 (void)source_location;
273 const unsigned current_thread)
275 const std::string identifier=
id2string(
object);
278 const varst &vars=(*this)(object);
307 const exprt cond_expr=
334 const unsigned current_thread)
336 const std::string identifier=
id2string(
object);
341 const varst &vars=(*this)(object);
365 const exprt new_value_expr=
367 buff0_used_and_mine_expr,
370 buff1_used_and_mine_expr,
375 assignment(goto_program, target, source_location,
object, new_value_expr);
386 buff0_used_and_mine_expr,
393 const exprt buff0_or_buff1_used_and_mine_expr=
394 or_exprt(buff0_used_and_mine_expr, buff1_used_and_mine_expr);
402 buff0_or_buff1_used_and_mine_expr,
408 const exprt buff0_thd_expr=
420 const exprt buff1_thd_expr=
429 buff0_or_buff1_used_and_mine_expr,
441 const unsigned current_thread,
442 const bool tso_pso_rmo)
444 const std::string identifier=
id2string(
object);
450 const varst &vars=(*this)(object);
458 const exprt nondet_bool_expr =
462 assignment(goto_program, target, source_location, choice0, nondet_bool_expr);
463 assignment(goto_program, target, source_location, choice2, nondet_bool_expr);
485 goto_program, target, source_location, vars.
flush_delayed, delay_expr);
490 bool instrumented=
false;
496 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
497 std::pair<m_itt, m_itt> ran=
cycles_loc.equal_range(
object);
498 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
499 if(ran_it->second==source_location)
508 if(tso_pso_rmo || !instrumented)
517 const exprt cond_134_expr=
527 const exprt val_134_expr=lhs;
528 const exprt buff0_used_134_expr=buff0_used_expr;
529 const exprt buff1_used_134_expr=buff1_used_expr;
530 const exprt buff0_134_expr=buff0_expr;
531 const exprt buff1_134_expr=buff1_expr;
532 const exprt buff0_thd_134_expr=buff0_thd_expr;
533 const exprt buff1_thd_134_expr=buff1_thd_expr;
538 const exprt cond_267_expr=
and_exprt(buff0_used_expr, buff0_thd_expr);
539 const exprt val_267_expr=buff0_expr;
542 const exprt buff0_267_expr=buff0_expr;
543 const exprt buff1_267_expr=buff1_expr;
550 const exprt cond_5_expr=
556 const exprt val_5_expr=buff1_expr;
557 const exprt buff0_used_5_expr=buff0_used_expr;
559 const exprt buff0_5_expr=buff0_expr;
560 const exprt buff1_5_expr=buff1_expr;
561 const exprt buff0_thd_5_expr=buff0_thd_expr;
625 buff0_used_5_expr))));
641 buff1_used_5_expr))));
657 buff0_thd_5_expr))));
672 buff1_thd_5_expr))));
685 goto_program, target, source_location, choice1, nondet_bool_expr);
693 const exprt val_1_expr=lhs;
694 const exprt buff0_used_1_expr=buff0_used_expr;
695 const exprt buff1_used_1_expr=buff1_used_expr;
696 const exprt buff0_1_expr=buff0_expr;
697 const exprt buff1_1_expr=buff1_expr;
698 const exprt buff0_thd_1_expr=buff0_thd_expr;
699 const exprt buff1_thd_1_expr=buff1_thd_expr;
704 const exprt cond_267_expr=
705 and_exprt(buff0_used_expr, buff0_thd_expr);
706 const exprt val_267_expr=buff0_expr;
709 const exprt buff0_267_expr=buff0_expr;
710 const exprt buff1_267_expr=buff1_expr;
717 const exprt cond_3_expr=
723 const exprt val_3_expr=
if_exprt(choice0_expr, buff0_expr, lhs);
724 const exprt buff0_used_3_expr=choice0_expr;
726 const exprt buff0_3_expr=buff0_expr;
727 const exprt buff1_3_expr=buff1_expr;
734 const exprt cond_4_expr=
738 const exprt val_4_expr=
746 const exprt buff0_used_4_expr=
748 const exprt buff1_used_4_expr=choice0_expr;
749 const exprt buff0_4_expr=buff0_expr;
750 const exprt buff1_4_expr=buff1_expr;
751 const exprt buff0_thd_4_expr=buff0_thd_expr;
752 const exprt buff1_thd_4_expr=
758 const exprt cond_5_expr=
760 and_exprt(buff0_used_expr, buff1_thd_expr),
762 const exprt val_5_expr=
767 const exprt buff0_used_5_expr=choice0_expr;
769 const exprt buff0_5_expr=buff0_expr;
770 const exprt buff1_5_expr=buff1_expr;
859 buff0_used_3_expr))))));
881 buff1_used_3_expr))))));
903 buff0_thd_3_expr))))));
925 buff1_thd_3_expr))))));
928 catch(
const std::string &s)
946 identifier==
"stdin" ||
947 identifier==
"stdout" ||
948 identifier==
"stderr" ||
949 identifier==
"sys_nerr" ||
997 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
998 std::pair<m_itt, m_itt> ran=
cycles_loc.equal_range(identifier);
999 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
1000 if(ran_it->second==source_location)
1034 for(
const auto &w_entry : rw_set.
w_entries)
1036 for(
const auto &r_entry : rw_set.
r_entries)
1039 <<
" reads from " <<
id2string(r_entry.second.object)
1107 for(
const auto &w_entry : rw_set.
w_entries)
1114 original_instruction.
swap(instruction);
1124 for(
const auto &r_entry : rw_set.
r_entries)
1128 goto_program, i_it, source_location, r_entry.second.object);
1136 r_entry.second.object,
1138 (model ==
TSO || model ==
PSO || model ==
RMO));
1142 for(
const auto &w_entry : rw_set.
w_entries)
1147 for(
const auto &r_entry : rw_set.
r_entries)
1150 ns, r_entry.second.symbol_expr,
true))
1156 r_entry.second.object,
1157 w_entry.second.object);
1168 w_entry.second.object,
1169 original_instruction,
1177 for(
const auto &r_entry : rw_set.
r_entries)
1181 r_entry.second.object) !=
1189 <<
"writer " << w_entry.second.object <<
" reads "
1207 const exprt nondet_bool_expr =
1230 r_entry.second.object,
1241 w_entry.second.object,
1249 for(
const auto &r_entry : rw_set.
r_entries)
1254 <<
"flush restore: " << r_entry.second.object <<
messaget::eom;
1261 delayed_expr, mem_value_expr, r_entry.second.symbol_expr);
1267 r_entry.second.object,
1270 goto_program, i_it, source_location,
1298 original_instruction.
swap(instruction);
1307 for(std::set<irep_idt>::iterator s_it=
past_writes.begin();
1311 goto_program, i_it, source_location, *s_it,