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,
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
A codet representing an assignment in the program.
const irep_idt & get_statement() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const source_locationt & source_location() const
The Boolean constant false.
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
This class represents an instruction in the GOTO intermediate representation.
source_locationt source_location
The location of the instruction in the source file.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
goto_program_instruction_typet type
What kind of instruction?
bool is_end_thread() const
const codet & get_code() const
Get the code represented by this instruction.
bool is_start_thread() const
bool is_function_call() const
void swap(instructiont &instruction)
Swap two instructions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
The trinary if-then-else operator.
bool get_bool(const irep_namet &name) const
mstreamt & warning() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
shared_bufferst & shared_buffers
void weak_memory(value_setst &value_sets, const irep_idt &function_id, memory_modelt model)
instruments the program for the pairs detected through the CFG
symbol_tablet & symbol_table
std::set< irep_idt > past_writes
goto_functionst & goto_functions
std::vector< irep_idt > r_buff0_thds
irep_idt read_delayed_var
std::vector< irep_idt > r_buff1_thds
std::multimap< irep_idt, source_locationt > cycles_loc
const varst & operator()(const irep_idt &object)
instruments the variable
void nondet_flush(const irep_idt &function_id, 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
std::string unique()
returns a unique id (for fresh variables)
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
void affected_by_delay(value_setst &value_sets, goto_functionst &goto_functions)
analysis over the goto-program which computes in affected_by_delay_set the variables (non necessarily...
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)
irep_idt add_fresh_var(const symbolt &object, const std::string &suffix, const typet &type)
void add_initialization(goto_programt &goto_program)
bool is_buffered_in_general(const symbol_exprt &, bool is_write)
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
irep_idt add(const symbolt &object, const std::string &suffix, const typet &type, bool added_as_instrumentation)
add a new var for instrumenting the input var
std::set< irep_idt > affected_by_delay_set
std::set< irep_idt > cycles
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 flush_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object)
flushes read (POWER)
irep_idt choice(const irep_idt &function_id, const std::string &suffix)
void add_initialization_code(goto_functionst &goto_functions)
bool is_buffered(const namespacet &, const symbol_exprt &, bool is_write)
std::set< irep_idt > instrumentations
class symbol_tablet & symbol_table
A side_effect_exprt that returns a non-deterministically chosen value.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
The Boolean constant true.
The type of an expression, extends irept.
bool has_prefix(const std::string &s, const std::string &prefix)
bool is_fence(const goto_programt::instructiont &instruction, const namespacet &ns)
bool is_lwfence(const goto_programt::instructiont &instruction, const namespacet &ns)
Fences for instrumentation.
int main(int argc, char *argv[])
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
Race Detection for Threaded Goto Programs.
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.