47 unsigned tmp_counter=0;
83 symbol_table.
move(new_symbol, symbol_ptr);
92 instruction.
guard=symbol_expr;
111 bool no_dependencies,
113 unsigned input_max_var,
114 unsigned input_max_po_trans,
117 bool render_function,
146 unsigned max_thds = 0;
148 max_thds=instrumenter.
goto2graph_cfg(value_sets, model, no_dependencies,
153 if(input_max_var!=0 || input_max_po_trans!=0)
155 input_max_po_trans, ignore_arrays);
163 unsigned interesting_scc = 0;
164 unsigned total_cycles = 0;
165 for(
unsigned i=0; i<instrumenter.
num_sccs; i++)
168 message.status()<<
"SCC #"<<i<<
": " 171 total_cycles += instrumenter
176 if(total_cycles == 0)
178 message.status()<<
"program safe -- no need to instrument"<<
messaget::eom;
185 message.status()<<
"cycles collected: "<<instrumenter.
set_of_cycles.size()
191 message.status()<<
"program safe -- no need to instrument"<<
messaget::eom;
228 for(std::set<irep_idt>::iterator it=
235 for(std::set<irep_idt>::iterator it=shared_buffers.
cycles.begin();
236 it!=shared_buffers.
cycles.end(); it++)
238 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
239 const std::pair<m_itt, m_itt> ran=
241 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
242 message.result() << ((*it)==
""?
"fence":*it) <<
", " 260 message.status()<<
"Goto-program instrumented" <<
messaget::eom;
unsigned goto2graph_cfg(value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body)
goes through CFG and build a static abstract event graph overapproximating the read/write relations f...
exprt guard
Guard for gotos, assume, assert.
void add_initialization_code(goto_functionst &goto_functions)
irep_idt function
The function this instruction belongs to.
irep_idt name
The unique identifier.
const std::string & id2string(const irep_idt &d)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
std::set< irep_idt > var_to_instr
instrumentation_strategyt
void introduce_temporaries(value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function, goto_programt &goto_program, messaget &message)
all access to shared variables is pushed into assignments
bool is_function_call() const
void weak_memory(value_setst &value_sets, const irep_idt &function, memory_modelt model)
instruments the program for the pairs detected through the CFG
exprt value
Initial value of symbol.
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
void print_outputs(memory_modelt model, bool hide_internals)
Weak Memory Instrumentation for Threaded Goto Programs.
void set_cav11(memory_modelt model)
This class represents an instruction in the GOTO intermediate representation.
void collect_cycles(memory_modelt model)
void set_rendering_options(bool aligned, bool file, bool function)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
void instrument_my_events(const std::set< event_idt > &events)
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...
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
std::multimap< irep_idt, source_locationt > cycles_r_loc
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
#define INITIALIZE_FUNCTION
std::multimap< irep_idt, source_locationt > id2loc
::goto_functiont goto_functiont
std::multimap< irep_idt, source_locationt > id2cycloc
void instrument_with_strategy(instrumentation_strategyt strategy)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
std::multimap< irep_idt, source_locationt > cycles_loc
A generic container class for the GOTO intermediate representation of one function.
typet type
Type of symbol.
static irep_idt entry_point()
mstreamt & status() const
source_locationt source_location
The location of the instruction in the source file.
static std::set< event_idt > extract_my_events()
irep_idt base_name
Base (non-scoped) name.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
void weak_memory(memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message_handler, bool ignore_arrays)
std::set< irep_idt > cycles
goto_programt & goto_program
std::set< event_grapht::critical_cyclet > set_of_cycles
void set_parameters_collection(unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
std::set< irep_idt > affected_by_delay_set
goto_programt coverage_criteriont message_handlert & message_handler
goto_functionst goto_functions
GOTO functions.
std::vector< std::set< event_idt > > egraph_SCCs
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC
Race Detection for Threaded Goto Programs.