31 var_mapt::const_iterator it=
var_map.find(
object);
88 const std::string &suffix,
98 ns.
lookup(
object).location,
107 return new_symbol.
name;
115 for(
const auto &vars :
var_map)
120 assignment(goto_program, t, source_location, vars.second.w_buff0_used,
122 assignment(goto_program, t, source_location, vars.second.w_buff1_used,
124 assignment(goto_program, t, source_location, vars.second.flush_delayed,
126 assignment(goto_program, t, source_location, vars.second.read_delayed,
128 assignment(goto_program, t, source_location, vars.second.read_delayed_var,
131 for(
const auto &
id : vars.second.r_buff0_thds)
134 for(
const auto &
id : vars.second.r_buff1_thds)
143 goto_functionst::function_mapt::iterator
147 throw "weak memory instrumentation needs an entry point";
162 std::string identifier=
id2string(id_lhs);
164 const size_t pos=identifier.find(
"[]");
166 if(
pos!=std::string::npos)
169 identifier.erase(
pos);
174 const exprt symbol=ns.
lookup(identifier).symbol_expr();
179 t->code.add_source_location()=source_location;
180 t->source_location=source_location;
186 catch(
const std::string &s)
204 assignment(goto_program, target, source_location, vars.read_delayed,
206 assignment(goto_program, target, source_location, vars.read_delayed_var,
211 assignment(goto_program, target, source_location, vars.read_new_var, new_var);
214 assignment(goto_program, target, source_location, write_object, new_var);
220 const std::string identifier=
id2string(write_object);
223 const varst &vars=(*this)(write_object);
250 const varst &vars=(*this)(write_object);
262 target->guard=if_expr;
264 target->source_location=source_location;
276 (void)source_location;
288 const unsigned current_thread)
290 const std::string identifier=
id2string(
object);
293 const varst &vars=(*this)(object);
298 goto_program, target, source_location, vars.
w_buff0,
299 original_instruction.
code.
op1());
319 const exprt cond_expr=
346 const unsigned current_thread)
348 const std::string identifier=
id2string(
object);
353 const varst &vars=(*this)(object);
377 const exprt new_value_expr=
379 buff0_used_and_mine_expr,
382 buff1_used_and_mine_expr,
387 assignment(goto_program, target, source_location,
object, new_value_expr);
398 buff0_used_and_mine_expr,
405 const exprt buff0_or_buff1_used_and_mine_expr=
406 or_exprt(buff0_used_and_mine_expr, buff1_used_and_mine_expr);
414 buff0_or_buff1_used_and_mine_expr,
420 const exprt buff0_thd_expr=
432 const exprt buff1_thd_expr=
441 buff0_or_buff1_used_and_mine_expr,
453 const unsigned current_thread,
454 const bool tso_pso_rmo)
456 const std::string identifier=
id2string(
object);
462 const varst &vars=(*this)(object);
470 const exprt nondet_bool_expr =
474 assignment(goto_program, target, source_location, choice0, nondet_bool_expr);
475 assignment(goto_program, target, source_location, choice2, nondet_bool_expr);
497 goto_program, target, source_location, vars.
flush_delayed, delay_expr);
502 bool instrumented=
false;
508 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
509 std::pair<m_itt, m_itt> ran=
cycles_loc.equal_range(
object);
510 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
511 if(ran_it->second==source_location)
520 if(tso_pso_rmo || !instrumented)
529 const exprt cond_134_expr=
539 const exprt val_134_expr=lhs;
540 const exprt buff0_used_134_expr=buff0_used_expr;
541 const exprt buff1_used_134_expr=buff1_used_expr;
542 const exprt buff0_134_expr=buff0_expr;
543 const exprt buff1_134_expr=buff1_expr;
544 const exprt buff0_thd_134_expr=buff0_thd_expr;
545 const exprt buff1_thd_134_expr=buff1_thd_expr;
550 const exprt cond_267_expr=
and_exprt(buff0_used_expr, buff0_thd_expr);
551 const exprt val_267_expr=buff0_expr;
554 const exprt buff0_267_expr=buff0_expr;
555 const exprt buff1_267_expr=buff1_expr;
562 const exprt cond_5_expr=
568 const exprt val_5_expr=buff1_expr;
569 const exprt buff0_used_5_expr=buff0_used_expr;
571 const exprt buff0_5_expr=buff0_expr;
572 const exprt buff1_5_expr=buff1_expr;
573 const exprt buff0_thd_5_expr=buff0_thd_expr;
637 buff0_used_5_expr))));
653 buff1_used_5_expr))));
669 buff0_thd_5_expr))));
684 buff1_thd_5_expr))));
697 goto_program, target, source_location, choice1, nondet_bool_expr);
705 const exprt val_1_expr=lhs;
706 const exprt buff0_used_1_expr=buff0_used_expr;
707 const exprt buff1_used_1_expr=buff1_used_expr;
708 const exprt buff0_1_expr=buff0_expr;
709 const exprt buff1_1_expr=buff1_expr;
710 const exprt buff0_thd_1_expr=buff0_thd_expr;
711 const exprt buff1_thd_1_expr=buff1_thd_expr;
716 const exprt cond_267_expr=
717 and_exprt(buff0_used_expr, buff0_thd_expr);
718 const exprt val_267_expr=buff0_expr;
721 const exprt buff0_267_expr=buff0_expr;
722 const exprt buff1_267_expr=buff1_expr;
729 const exprt cond_3_expr=
735 const exprt val_3_expr=
if_exprt(choice0_expr, buff0_expr, lhs);
736 const exprt buff0_used_3_expr=choice0_expr;
738 const exprt buff0_3_expr=buff0_expr;
739 const exprt buff1_3_expr=buff1_expr;
746 const exprt cond_4_expr=
750 const exprt val_4_expr=
758 const exprt buff0_used_4_expr=
760 const exprt buff1_used_4_expr=choice0_expr;
761 const exprt buff0_4_expr=buff0_expr;
762 const exprt buff1_4_expr=buff1_expr;
763 const exprt buff0_thd_4_expr=buff0_thd_expr;
764 const exprt buff1_thd_4_expr=
770 const exprt cond_5_expr=
772 and_exprt(buff0_used_expr, buff1_thd_expr),
774 const exprt val_5_expr=
779 const exprt buff0_used_5_expr=choice0_expr;
781 const exprt buff0_5_expr=buff0_expr;
782 const exprt buff1_5_expr=buff1_expr;
871 buff0_used_3_expr))))));
893 buff1_used_3_expr))))));
915 buff0_thd_3_expr))))));
937 buff1_thd_3_expr))))));
940 catch(
const std::string &s)
958 identifier==
"stdin" ||
959 identifier==
"stdout" ||
960 identifier==
"stderr" ||
961 identifier==
"sys_nerr" ||
1009 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
1010 std::pair<m_itt, m_itt> ran=
cycles_loc.equal_range(identifier);
1011 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
1012 if(ran_it->second==source_location)
1050 <<
" reads from "<<
id2string(r_it->second.object)
1120 original_instruction.
swap(instruction);
1134 goto_program, i_it, source_location, e_it->second.object);
1142 e_it->second.object,
1144 (model ==
TSO || model ==
PSO || model ==
RMO));
1157 goto_program, i_it, source_location, r_it->second.object,
1158 e_it->second.object);
1165 goto_program, i_it, source_location,
1166 e_it->second.object, original_instruction,
1176 r_it->second.object)!=
1184 <<e_it->second.object
1191 r_it->second.object, vars.
type);
1202 const exprt nondet_bool_expr =
1222 goto_program, i_it, source_location,
1223 r_it->second.object, rhs);
1229 goto_program, i_it, source_location,
1230 e_it->second.object, original_instruction.
code.
op1());
1247 const exprt cond_expr=
if_exprt(delayed_expr, mem_value_expr,
1248 e_it->second.symbol_expr);
1251 goto_program, i_it, source_location,
1252 e_it->second.object, cond_expr);
1254 goto_program, i_it, source_location,
1271 else if(
is_fence(instruction, ns) ||
1280 original_instruction.
swap(instruction);
1289 for(std::set<irep_idt>::iterator s_it=
past_writes.begin();
1293 goto_program, i_it, source_location, *s_it,