10 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_SHARED_BUFFERS_H 11 #define CPROVER_GOTO_INSTRUMENT_WMM_SHARED_BUFFERS_H 44 throw "sorry, CAV11 only available for TSO";
110 const unsigned current_thread);
117 const unsigned current_thread);
124 const unsigned current_thread,
125 const bool tso_pso_rmo);
142 assignment(goto_program, t, source_location, id_lhs,
143 ns.
lookup(id_rhs).symbol_expr());
162 const std::string function_base_name =
166 return add(function_base_name+
"_weak_choice",
167 function_base_name+
"_weak_choice", suffix,
bool_typet());
249 const std::string &suffix,
251 bool added_as_instrumentation);
256 const std::string &suffix,
259 return add(
object, base_name, suffix, type,
true);
266 const std::string &suffix,
269 return add(
object, base_name, suffix, type,
false);
275 #endif // CPROVER_GOTO_INSTRUMENT_WMM_SHARED_BUFFERS_H void add_initialization_code(goto_functionst &goto_functions)
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
void weak_memory(value_setst &value_sets, const irep_idt &function, memory_modelt model)
instruments the program for the pairs detected through the CFG
shared_bufferst(symbol_tablet &_symbol_table, unsigned _nb_threads, messaget &_message)
bool track(const irep_idt &id) const
void add_initialization(goto_programt &goto_program)
irep_idt choice(const irep_idt &function, const std::string &suffix)
std::string unique()
returns a unique id (for fresh variables)
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...
bool is_buffered_in_general(const symbol_exprt &, bool is_write)
irep_idt add(const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type)
void set_cav11(memory_modelt model)
This class represents an instruction in the GOTO intermediate representation.
std::set< irep_idt > instrumentations
goto_functionst & goto_functions
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
irep_idt read_delayed_var
instructionst::iterator targett
std::map< irep_idt, varst > var_mapt
std::multimap< irep_idt, source_locationt > cycles_r_loc
cfg_visitort(shared_bufferst &_shared, symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
std::set< irep_idt > past_writes
void weak_memory(value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, memory_modelt model, goto_functionst &goto_functions)
void flush_read(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object)
flushes read (POWER)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
shared_bufferst & shared_buffers
std::vector< irep_idt > r_buff1_thds
bool has_prefix(const std::string &s, const std::string &prefix)
const varst & operator()(const irep_idt &object)
instruments the variable
A collection of goto functions.
irep_idt add_fresh_var(const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type)
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void assignment(goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &id_lhs, const irep_idt &id_rhs)
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
std::vector< irep_idt > r_buff0_thds
A generic container class for the GOTO intermediate representation of one function.
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
bool is_buffered(const namespacet &, const symbol_exprt &, bool is_write)
Base class for all expressions.
symbol_tablet & symbol_table
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
Expression to hold a symbol (variable)
class symbol_tablet & symbol_table
std::set< irep_idt > affected_by_delay_set
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().