32 var_mapt::const_iterator it=
var_map.find(
object);
89 const std::string &suffix,
99 ns.
lookup(
object).location,
108 return new_symbol.
name;
116 for(
const auto &vars :
var_map)
121 assignment(goto_program, t, source_location, vars.second.w_buff0_used,
123 assignment(goto_program, t, source_location, vars.second.w_buff1_used,
125 assignment(goto_program, t, source_location, vars.second.flush_delayed,
127 assignment(goto_program, t, source_location, vars.second.read_delayed,
129 assignment(goto_program, t, source_location, vars.second.read_delayed_var,
132 for(
const auto &
id : vars.second.r_buff0_thds)
135 for(
const auto &
id : vars.second.r_buff1_thds)
144 goto_functionst::function_mapt::iterator
148 throw "weak memory instrumentation needs an entry point";
163 std::string identifier=
id2string(id_lhs);
165 const size_t pos=identifier.find(
"[]");
167 if(
pos!=std::string::npos)
170 identifier.erase(
pos);
175 const exprt symbol=ns.
lookup(identifier).symbol_expr();
180 t->code_nonconst().add_source_location() = source_location;
181 t->source_location=source_location;
187 catch(
const std::string &s)
205 assignment(goto_program, target, source_location, vars.read_delayed,
207 assignment(goto_program, target, source_location, vars.read_delayed_var,
212 assignment(goto_program, target, source_location, vars.read_new_var, new_var);
215 assignment(goto_program, target, source_location, write_object, new_var);
221 const std::string identifier=
id2string(write_object);
224 const varst &vars=(*this)(write_object);
251 const varst &vars=(*this)(write_object);
263 target->guard=if_expr;
265 target->source_location=source_location;
277 (void)source_location;
289 const unsigned current_thread)
291 const std::string identifier=
id2string(
object);
294 const varst &vars=(*this)(object);
323 const exprt cond_expr=
350 const unsigned current_thread)
352 const std::string identifier=
id2string(
object);
357 const varst &vars=(*this)(object);
381 const exprt new_value_expr=
383 buff0_used_and_mine_expr,
386 buff1_used_and_mine_expr,
391 assignment(goto_program, target, source_location,
object, new_value_expr);
402 buff0_used_and_mine_expr,
409 const exprt buff0_or_buff1_used_and_mine_expr=
410 or_exprt(buff0_used_and_mine_expr, buff1_used_and_mine_expr);
418 buff0_or_buff1_used_and_mine_expr,
424 const exprt buff0_thd_expr=
436 const exprt buff1_thd_expr=
445 buff0_or_buff1_used_and_mine_expr,
457 const unsigned current_thread,
458 const bool tso_pso_rmo)
460 const std::string identifier=
id2string(
object);
466 const varst &vars=(*this)(object);
474 const exprt nondet_bool_expr =
478 assignment(goto_program, target, source_location, choice0, nondet_bool_expr);
479 assignment(goto_program, target, source_location, choice2, nondet_bool_expr);
501 goto_program, target, source_location, vars.
flush_delayed, delay_expr);
506 bool instrumented=
false;
512 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
513 std::pair<m_itt, m_itt> ran=
cycles_loc.equal_range(
object);
514 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
515 if(ran_it->second==source_location)
524 if(tso_pso_rmo || !instrumented)
533 const exprt cond_134_expr=
543 const exprt val_134_expr=lhs;
544 const exprt buff0_used_134_expr=buff0_used_expr;
545 const exprt buff1_used_134_expr=buff1_used_expr;
546 const exprt buff0_134_expr=buff0_expr;
547 const exprt buff1_134_expr=buff1_expr;
548 const exprt buff0_thd_134_expr=buff0_thd_expr;
549 const exprt buff1_thd_134_expr=buff1_thd_expr;
554 const exprt cond_267_expr=
and_exprt(buff0_used_expr, buff0_thd_expr);
555 const exprt val_267_expr=buff0_expr;
558 const exprt buff0_267_expr=buff0_expr;
559 const exprt buff1_267_expr=buff1_expr;
566 const exprt cond_5_expr=
572 const exprt val_5_expr=buff1_expr;
573 const exprt buff0_used_5_expr=buff0_used_expr;
575 const exprt buff0_5_expr=buff0_expr;
576 const exprt buff1_5_expr=buff1_expr;
577 const exprt buff0_thd_5_expr=buff0_thd_expr;
641 buff0_used_5_expr))));
657 buff1_used_5_expr))));
673 buff0_thd_5_expr))));
688 buff1_thd_5_expr))));
701 goto_program, target, source_location, choice1, nondet_bool_expr);
709 const exprt val_1_expr=lhs;
710 const exprt buff0_used_1_expr=buff0_used_expr;
711 const exprt buff1_used_1_expr=buff1_used_expr;
712 const exprt buff0_1_expr=buff0_expr;
713 const exprt buff1_1_expr=buff1_expr;
714 const exprt buff0_thd_1_expr=buff0_thd_expr;
715 const exprt buff1_thd_1_expr=buff1_thd_expr;
720 const exprt cond_267_expr=
721 and_exprt(buff0_used_expr, buff0_thd_expr);
722 const exprt val_267_expr=buff0_expr;
725 const exprt buff0_267_expr=buff0_expr;
726 const exprt buff1_267_expr=buff1_expr;
733 const exprt cond_3_expr=
739 const exprt val_3_expr=
if_exprt(choice0_expr, buff0_expr, lhs);
740 const exprt buff0_used_3_expr=choice0_expr;
742 const exprt buff0_3_expr=buff0_expr;
743 const exprt buff1_3_expr=buff1_expr;
750 const exprt cond_4_expr=
754 const exprt val_4_expr=
762 const exprt buff0_used_4_expr=
764 const exprt buff1_used_4_expr=choice0_expr;
765 const exprt buff0_4_expr=buff0_expr;
766 const exprt buff1_4_expr=buff1_expr;
767 const exprt buff0_thd_4_expr=buff0_thd_expr;
768 const exprt buff1_thd_4_expr=
774 const exprt cond_5_expr=
776 and_exprt(buff0_used_expr, buff1_thd_expr),
778 const exprt val_5_expr=
783 const exprt buff0_used_5_expr=choice0_expr;
785 const exprt buff0_5_expr=buff0_expr;
786 const exprt buff1_5_expr=buff1_expr;
875 buff0_used_3_expr))))));
897 buff1_used_3_expr))))));
919 buff0_thd_3_expr))))));
941 buff1_thd_3_expr))))));
944 catch(
const std::string &s)
962 identifier==
"stdin" ||
963 identifier==
"stdout" ||
964 identifier==
"stderr" ||
965 identifier==
"sys_nerr" ||
1013 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
1014 std::pair<m_itt, m_itt> ran=
cycles_loc.equal_range(identifier);
1015 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
1016 if(ran_it->second==source_location)
1050 for(
const auto &w_entry : rw_set.
w_entries)
1052 for(
const auto &r_entry : rw_set.
r_entries)
1055 <<
" reads from " <<
id2string(r_entry.second.object)
1123 for(
const auto &w_entry : rw_set.
w_entries)
1130 original_instruction.
swap(instruction);
1140 for(
const auto &r_entry : rw_set.
r_entries)
1144 goto_program, i_it, source_location, r_entry.second.object);
1152 r_entry.second.object,
1154 (model ==
TSO || model ==
PSO || model ==
RMO));
1158 for(
const auto &w_entry : rw_set.
w_entries)
1163 for(
const auto &r_entry : rw_set.
r_entries)
1166 ns, r_entry.second.symbol_expr,
true))
1172 r_entry.second.object,
1173 w_entry.second.object);
1184 w_entry.second.object,
1185 original_instruction,
1193 for(
const auto &r_entry : rw_set.
r_entries)
1197 r_entry.second.object) !=
1205 <<
"writer " << w_entry.second.object <<
" reads "
1223 const exprt nondet_bool_expr =
1246 r_entry.second.object,
1257 w_entry.second.object,
1265 for(
const auto &r_entry : rw_set.
r_entries)
1270 <<
"flush restore: " << r_entry.second.object <<
messaget::eom;
1277 delayed_expr, mem_value_expr, r_entry.second.symbol_expr);
1283 r_entry.second.object,
1286 goto_program, i_it, source_location,
1314 original_instruction.
swap(instruction);
1323 for(std::set<irep_idt>::iterator s_it=
past_writes.begin();
1327 goto_program, i_it, source_location, *s_it,