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.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);
299 goto_program, target, source_location, vars.
w_buff0,
300 original_instruction.
code.
op1());
320 const exprt cond_expr=
347 const unsigned current_thread)
349 const std::string identifier=
id2string(
object);
354 const varst &vars=(*this)(object);
378 const exprt new_value_expr=
380 buff0_used_and_mine_expr,
383 buff1_used_and_mine_expr,
388 assignment(goto_program, target, source_location,
object, new_value_expr);
399 buff0_used_and_mine_expr,
406 const exprt buff0_or_buff1_used_and_mine_expr=
407 or_exprt(buff0_used_and_mine_expr, buff1_used_and_mine_expr);
415 buff0_or_buff1_used_and_mine_expr,
421 const exprt buff0_thd_expr=
433 const exprt buff1_thd_expr=
442 buff0_or_buff1_used_and_mine_expr,
454 const unsigned current_thread,
455 const bool tso_pso_rmo)
457 const std::string identifier=
id2string(
object);
463 const varst &vars=(*this)(object);
471 const exprt nondet_bool_expr =
475 assignment(goto_program, target, source_location, choice0, nondet_bool_expr);
476 assignment(goto_program, target, source_location, choice2, nondet_bool_expr);
498 goto_program, target, source_location, vars.
flush_delayed, delay_expr);
503 bool instrumented=
false;
509 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
510 std::pair<m_itt, m_itt> ran=
cycles_loc.equal_range(
object);
511 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
512 if(ran_it->second==source_location)
521 if(tso_pso_rmo || !instrumented)
530 const exprt cond_134_expr=
540 const exprt val_134_expr=lhs;
541 const exprt buff0_used_134_expr=buff0_used_expr;
542 const exprt buff1_used_134_expr=buff1_used_expr;
543 const exprt buff0_134_expr=buff0_expr;
544 const exprt buff1_134_expr=buff1_expr;
545 const exprt buff0_thd_134_expr=buff0_thd_expr;
546 const exprt buff1_thd_134_expr=buff1_thd_expr;
551 const exprt cond_267_expr=
and_exprt(buff0_used_expr, buff0_thd_expr);
552 const exprt val_267_expr=buff0_expr;
555 const exprt buff0_267_expr=buff0_expr;
556 const exprt buff1_267_expr=buff1_expr;
563 const exprt cond_5_expr=
569 const exprt val_5_expr=buff1_expr;
570 const exprt buff0_used_5_expr=buff0_used_expr;
572 const exprt buff0_5_expr=buff0_expr;
573 const exprt buff1_5_expr=buff1_expr;
574 const exprt buff0_thd_5_expr=buff0_thd_expr;
638 buff0_used_5_expr))));
654 buff1_used_5_expr))));
670 buff0_thd_5_expr))));
685 buff1_thd_5_expr))));
698 goto_program, target, source_location, choice1, nondet_bool_expr);
706 const exprt val_1_expr=lhs;
707 const exprt buff0_used_1_expr=buff0_used_expr;
708 const exprt buff1_used_1_expr=buff1_used_expr;
709 const exprt buff0_1_expr=buff0_expr;
710 const exprt buff1_1_expr=buff1_expr;
711 const exprt buff0_thd_1_expr=buff0_thd_expr;
712 const exprt buff1_thd_1_expr=buff1_thd_expr;
717 const exprt cond_267_expr=
718 and_exprt(buff0_used_expr, buff0_thd_expr);
719 const exprt val_267_expr=buff0_expr;
722 const exprt buff0_267_expr=buff0_expr;
723 const exprt buff1_267_expr=buff1_expr;
730 const exprt cond_3_expr=
736 const exprt val_3_expr=
if_exprt(choice0_expr, buff0_expr, lhs);
737 const exprt buff0_used_3_expr=choice0_expr;
739 const exprt buff0_3_expr=buff0_expr;
740 const exprt buff1_3_expr=buff1_expr;
747 const exprt cond_4_expr=
751 const exprt val_4_expr=
759 const exprt buff0_used_4_expr=
761 const exprt buff1_used_4_expr=choice0_expr;
762 const exprt buff0_4_expr=buff0_expr;
763 const exprt buff1_4_expr=buff1_expr;
764 const exprt buff0_thd_4_expr=buff0_thd_expr;
765 const exprt buff1_thd_4_expr=
771 const exprt cond_5_expr=
773 and_exprt(buff0_used_expr, buff1_thd_expr),
775 const exprt val_5_expr=
780 const exprt buff0_used_5_expr=choice0_expr;
782 const exprt buff0_5_expr=buff0_expr;
783 const exprt buff1_5_expr=buff1_expr;
872 buff0_used_3_expr))))));
894 buff1_used_3_expr))))));
916 buff0_thd_3_expr))))));
938 buff1_thd_3_expr))))));
941 catch(
const std::string &s)
959 identifier==
"stdin" ||
960 identifier==
"stdout" ||
961 identifier==
"stderr" ||
962 identifier==
"sys_nerr" ||
1010 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
1011 std::pair<m_itt, m_itt> ran=
cycles_loc.equal_range(identifier);
1012 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
1013 if(ran_it->second==source_location)
1047 for(
const auto &w_entry : rw_set.
w_entries)
1049 for(
const auto &r_entry : rw_set.
r_entries)
1052 <<
" reads from " <<
id2string(r_entry.second.object)
1120 for(
const auto &w_entry : rw_set.
w_entries)
1127 original_instruction.
swap(instruction);
1137 for(
const auto &r_entry : rw_set.
r_entries)
1141 goto_program, i_it, source_location, r_entry.second.object);
1149 r_entry.second.object,
1151 (model ==
TSO || model ==
PSO || model ==
RMO));
1155 for(
const auto &w_entry : rw_set.
w_entries)
1160 for(
const auto &r_entry : rw_set.
r_entries)
1163 ns, r_entry.second.symbol_expr,
true))
1169 r_entry.second.object,
1170 w_entry.second.object);
1181 w_entry.second.object,
1182 original_instruction,
1190 for(
const auto &r_entry : rw_set.
r_entries)
1194 r_entry.second.object) !=
1202 <<
"writer " << w_entry.second.object <<
" reads "
1220 const exprt nondet_bool_expr =
1243 r_entry.second.object,
1254 w_entry.second.object,
1255 original_instruction.
code.
op1());
1262 for(
const auto &r_entry : rw_set.
r_entries)
1267 <<
"flush restore: " << r_entry.second.object <<
messaget::eom;
1274 delayed_expr, mem_value_expr, r_entry.second.symbol_expr);
1280 r_entry.second.object,
1283 goto_program, i_it, source_location,
1301 else if(
is_fence(instruction, ns) ||
1310 original_instruction.
swap(instruction);
1319 for(std::set<irep_idt>::iterator s_it=
past_writes.begin();
1323 goto_program, i_it, source_location, *s_it,