11 #include "../rw_set.h" 19 return "$fresh#"+std::to_string(
uniq++);
26 var_mapt::const_iterator it=
var_map.find(
object);
33 const symbolt &symbol=ns.lookup(
object);
40 vars.w_buff0_used=
add(
object, symbol.
base_name,
"$w_buff0_used",
42 vars.w_buff1_used=
add(
object, symbol.
base_name,
"$w_buff1_used",
46 vars.flush_delayed=
add(
object, symbol.
base_name,
"$flush_delayed",
51 vars.read_delayed_var=
60 vars.r_buff0_thds.push_back(
64 "$r_buff0_thd"+std::to_string(cnt),
66 vars.r_buff1_thds.push_back(
70 "$r_buff1_thd"+std::to_string(cnt),
83 const std::string &suffix,
90 new_symbol.
name=identifier;
109 for(
const auto &vars :
var_map)
114 assignment(goto_program, t, source_location, vars.second.w_buff0_used,
116 assignment(goto_program, t, source_location, vars.second.w_buff1_used,
118 assignment(goto_program, t, source_location, vars.second.flush_delayed,
120 assignment(goto_program, t, source_location, vars.second.read_delayed,
122 assignment(goto_program, t, source_location, vars.second.read_delayed_var,
125 for(
const auto &
id : vars.second.r_buff0_thds)
128 for(
const auto &
id : vars.second.r_buff1_thds)
137 goto_functionst::function_mapt::iterator
141 throw "weak memory instrumentation needs an entry point";
156 std::string identifier=
id2string(id_lhs);
158 const size_t pos=identifier.find(
"[]");
160 if(
pos!=std::string::npos)
163 identifier.erase(
pos);
168 const exprt symbol=ns.
lookup(identifier).symbol_expr();
173 t->code.add_source_location()=source_location;
174 t->source_location=source_location;
198 assignment(goto_program, target, source_location, vars.read_delayed,
200 assignment(goto_program, target, source_location, vars.read_delayed_var,
205 assignment(goto_program, target, source_location, vars.read_new_var, new_var);
208 assignment(goto_program, target, source_location, write_object, new_var);
214 const std::string identifier=
id2string(write_object);
217 const varst &vars=(*this)(write_object);
245 const varst &vars=(*this)(write_object);
257 target->guard=if_expr;
259 target->source_location=source_location;
277 goto_programt::instructiont &original_instruction,
278 const unsigned current_thread)
280 const std::string identifier=
id2string(
object);
283 const varst &vars=(*this)(object);
288 goto_program, target, source_location, vars.
w_buff0,
289 original_instruction.code.op1());
309 const exprt cond_expr=
313 target->guard=cond_expr;
316 target->code.add_source_location()=source_location;
317 target->source_location=source_location;
340 const unsigned current_thread)
342 const std::string identifier=
id2string(
object);
347 const varst &vars=(*this)(object);
371 const exprt new_value_expr=
373 buff0_used_and_mine_expr,
376 buff1_used_and_mine_expr,
381 assignment(goto_program, target, source_location,
object, new_value_expr);
392 buff0_used_and_mine_expr,
399 const exprt buff0_or_buff1_used_and_mine_expr=
400 or_exprt(buff0_used_and_mine_expr, buff1_used_and_mine_expr);
408 buff0_or_buff1_used_and_mine_expr,
414 const exprt buff0_thd_expr=
426 const exprt buff1_thd_expr=
435 buff0_or_buff1_used_and_mine_expr,
446 const unsigned current_thread,
447 const bool tso_pso_rmo)
449 const std::string identifier=
id2string(
object);
455 const varst &vars=(*this)(object);
466 assignment(goto_program, target, source_location, choice0, nondet_bool_expr);
467 assignment(goto_program, target, source_location, choice2, nondet_bool_expr);
489 goto_program, target, source_location, vars.
flush_delayed, delay_expr);
494 bool instrumented=
false;
500 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
501 std::pair<m_itt, m_itt> ran=
cycles_loc.equal_range(
object);
502 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
503 if(ran_it->second==source_location)
512 if(tso_pso_rmo || !instrumented)
521 const exprt cond_134_expr=
531 const exprt val_134_expr=lhs;
532 const exprt buff0_used_134_expr=buff0_used_expr;
533 const exprt buff1_used_134_expr=buff1_used_expr;
534 const exprt buff0_134_expr=buff0_expr;
535 const exprt buff1_134_expr=buff1_expr;
536 const exprt buff0_thd_134_expr=buff0_thd_expr;
537 const exprt buff1_thd_134_expr=buff1_thd_expr;
542 const exprt cond_267_expr=
and_exprt(buff0_used_expr, buff0_thd_expr);
543 const exprt val_267_expr=buff0_expr;
546 const exprt buff0_267_expr=buff0_expr;
547 const exprt buff1_267_expr=buff1_expr;
554 const exprt cond_5_expr=
560 const exprt val_5_expr=buff1_expr;
561 const exprt buff0_used_5_expr=buff0_used_expr;
563 const exprt buff0_5_expr=buff0_expr;
564 const exprt buff1_5_expr=buff1_expr;
565 const exprt buff0_thd_5_expr=buff0_thd_expr;
629 buff0_used_5_expr))));
645 buff1_used_5_expr))));
661 buff0_thd_5_expr))));
676 buff1_thd_5_expr))));
689 goto_program, target, source_location, choice1, nondet_bool_expr);
697 const exprt val_1_expr=lhs;
698 const exprt buff0_used_1_expr=buff0_used_expr;
699 const exprt buff1_used_1_expr=buff1_used_expr;
700 const exprt buff0_1_expr=buff0_expr;
701 const exprt buff1_1_expr=buff1_expr;
702 const exprt buff0_thd_1_expr=buff0_thd_expr;
703 const exprt buff1_thd_1_expr=buff1_thd_expr;
708 const exprt cond_267_expr=
709 and_exprt(buff0_used_expr, buff0_thd_expr);
710 const exprt val_267_expr=buff0_expr;
713 const exprt buff0_267_expr=buff0_expr;
714 const exprt buff1_267_expr=buff1_expr;
721 const exprt cond_3_expr=
727 const exprt val_3_expr=
if_exprt(choice0_expr, buff0_expr, lhs);
728 const exprt buff0_used_3_expr=choice0_expr;
730 const exprt buff0_3_expr=buff0_expr;
731 const exprt buff1_3_expr=buff1_expr;
738 const exprt cond_4_expr=
742 const exprt val_4_expr=
750 const exprt buff0_used_4_expr=
752 const exprt buff1_used_4_expr=choice0_expr;
753 const exprt buff0_4_expr=buff0_expr;
754 const exprt buff1_4_expr=buff1_expr;
755 const exprt buff0_thd_4_expr=buff0_thd_expr;
756 const exprt buff1_thd_4_expr=
762 const exprt cond_5_expr=
764 and_exprt(buff0_used_expr, buff1_thd_expr),
766 const exprt val_5_expr=
771 const exprt buff0_used_5_expr=choice0_expr;
773 const exprt buff0_5_expr=buff0_expr;
774 const exprt buff1_5_expr=buff1_expr;
863 buff0_used_3_expr))))));
885 buff1_used_3_expr))))));
907 buff0_thd_3_expr))))));
929 buff1_thd_3_expr))))));
932 catch (std::string s)
950 identifier==
"stdin" ||
951 identifier==
"stdout" ||
952 identifier==
"stderr" ||
953 identifier==
"sys_nerr" ||
1002 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
1003 std::pair<m_itt, m_itt> ran=
cycles_loc.equal_range(identifier);
1004 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
1005 if(ran_it->second==source_location)
1039 <<
" reads from "<<
id2string(r_it->second.object)
1069 goto_programt::instructiont &instruction=*i_it;
1075 if(instruction.is_start_thread())
1081 else if(instruction.is_end_thread())
1084 if(instruction.is_assign())
1103 goto_programt::instructiont original_instruction;
1104 original_instruction.swap(instruction);
1106 original_instruction.source_location;
1109 instruction.make_atomic_begin();
1110 instruction.source_location=source_location;
1119 goto_program, i_it, source_location, e_it->second.object);
1123 goto_program, i_it, source_location, e_it->second.object,
1125 (model==
TSO || model==
PSO || model==
RMO));
1138 goto_program, i_it, source_location, r_it->second.object,
1139 e_it->second.object);
1146 goto_program, i_it, source_location,
1147 e_it->second.object, original_instruction,
1157 r_it->second.object)!=
1165 <<e_it->second.object
1172 r_it->second.object, vars.
type);
1181 instruction.function,
"1");
1205 goto_program, i_it, source_location,
1206 r_it->second.object, rhs);
1212 goto_program, i_it, source_location,
1213 e_it->second.object, original_instruction.code.op1());
1230 const exprt cond_expr=
if_exprt(delayed_expr, mem_value_expr,
1231 e_it->second.symbol_expr);
1234 goto_program, i_it, source_location,
1235 e_it->second.object, cond_expr);
1237 goto_program, i_it, source_location,
1243 i_it->make_atomic_end();
1244 i_it->source_location=source_location;
1255 else if(
is_fence(instruction, ns) ||
1256 (instruction.is_other() &&
1257 instruction.code.get_statement()==ID_fence &&
1258 (instruction.code.get_bool(
"WRfence") ||
1259 instruction.code.get_bool(
"WWfence") ||
1260 instruction.code.get_bool(
"RWfence") ||
1261 instruction.code.get_bool(
"RRfence"))))
1263 goto_programt::instructiont original_instruction;
1264 original_instruction.swap(instruction);
1266 original_instruction.source_location;
1269 instruction.make_atomic_begin();
1270 instruction.source_location=source_location;
1274 for(std::set<irep_idt>::iterator s_it=
past_writes.begin();
1278 goto_program, i_it, source_location, *s_it,
1284 i_it->make_atomic_end();
1285 i_it->source_location=source_location;
1295 else if(instruction.is_function_call())
void add_initialization_code(goto_functionst &goto_functions)
The type of an expression.
irep_idt name
The unique identifier.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
instructionst instructions
The list of instructions in the goto program.
void weak_memory(value_setst &value_sets, const irep_idt &function, memory_modelt model)
instruments the program for the pairs detected through the CFG
const irep_idt & get_identifier() const
#define forall_rw_set_w_entries(it, rw_set)
The null pointer constant.
exprt value
Initial value of symbol.
The trinary if-then-else operator.
void add_initialization(goto_programt &goto_program)
irep_idt choice(const irep_idt &function, const std::string &suffix)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
std::string unique()
returns a unique id (for fresh variables)
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
std::set< irep_idt > instrumentations
goto_functionst & goto_functions
#define forall_rw_set_r_entries(it, rw_set)
void write(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, goto_programt::instructiont &original_instruction, const unsigned current_thread)
instruments write
The boolean constant true.
irep_idt read_delayed_var
void affected_by_delay(symbol_tablet &symbol_table, value_setst &value_sets, goto_functionst &goto_functions)
analysis over the goto-program which computes in affected_by_delay_set the variables (non necessarily...
std::set< irep_idt > past_writes
Operator to dereference a pointer.
static irep_idt entry_point()
void flush_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object)
flushes read (POWER)
shared_bufferst & shared_buffers
std::vector< irep_idt > r_buff1_thds
A side effect that returns a non-deterministically chosen value.
const varst & operator()(const irep_idt &object)
instruments the variable
irep_idt add_fresh_var(const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type)
Operator to return the address of an object.
function_mapt function_map
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
The boolean constant false.
std::multimap< irep_idt, source_locationt > cycles_loc
irep_idt add(const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type, bool added_as_instrumentation)
add a new var for instrumenting the input var
bool has_prefix(const std::string &s, const std::string &prefix)
targett insert_before(const_targett target)
Insertion before the given target.
std::vector< irep_idt > r_buff0_thds
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
void nondet_flush(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread, const bool tso_pso_rmo)
instruments read
Fences for instrumentation.
bool is_buffered(const namespacet &, const symbol_exprt &, bool is_write)
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
irep_idt base_name
Base (non-scoped) name.
symbol_tablet & symbol_table
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
void det_flush(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread)
flush buffers (instruments fence)
std::set< irep_idt > cycles
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
class symbol_tablet & symbol_table
std::set< irep_idt > affected_by_delay_set
bool is_buffered_in_general(const namespacet &, const symbol_exprt &, bool is_write)
void delay_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &read_object, const irep_idt &write_object)
delays a read (POWER)
void assignment(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &id_lhs, const exprt &rhs)
add an assignment in the goto-program
const code_function_callt & to_code_function_call(const codet &code)
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
instructionst::iterator targett