32 #include "../rw_set.h" 49 unsigned tmp_counter=0;
57 goto_programt::instructiont &instruction=*i_it;
59 message.debug() <<instruction.source_location<<
messaget::eom;
61 if(instruction.is_goto() ||
62 instruction.is_assert() ||
63 instruction.is_assume())
76 id2string(
function)+
"$tmp_guard"+std::to_string(tmp_counter++);
85 symbol_table.
move(new_symbol, symbol_ptr);
87 goto_programt::instructiont new_i;
88 new_i.make_assignment();
90 new_i.source_location=instruction.source_location;
91 new_i.function=instruction.function;
94 instruction.guard=symbol_expr;
99 else if(instruction.is_function_call())
113 unsigned unwinding_bound,
115 bool no_dependencies,
117 unsigned input_max_var,
118 unsigned input_max_po_trans,
121 bool render_function,
150 unsigned max_thds = 0;
151 instrumentert instrumenter(symbol_table, goto_functions, message);
152 max_thds=instrumenter.
goto2graph_cfg(value_sets, model, no_dependencies,
157 if(input_max_var!=0 || input_max_po_trans!=0)
159 input_max_po_trans, ignore_arrays);
167 unsigned interesting_scc = 0;
168 unsigned total_cycles = 0;
169 for(
unsigned i=0; i<instrumenter.
num_sccs; i++)
172 message.status()<<
"SCC #"<<i<<
": " 175 total_cycles += instrumenter
180 if(total_cycles == 0)
182 message.status()<<
"program safe -- no need to instrument"<<
messaget::eom;
189 message.status()<<
"cycles collected: "<<instrumenter.
set_of_cycles.size()
195 message.status()<<
"program safe -- no need to instrument"<<
messaget::eom;
230 for(std::set<irep_idt>::iterator it=
237 for(std::set<irep_idt>::iterator it=shared_buffers.
cycles.begin();
238 it!=shared_buffers.
cycles.end(); it++)
240 typedef std::multimap<irep_idt, source_locationt>::iterator m_itt;
241 const std::pair<m_itt, m_itt> ran=
243 for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++)
244 message.result() << ((*it)==
""?
"fence":*it) <<
", " 262 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...
void add_initialization_code(goto_functionst &goto_functions)
irep_idt name
The unique identifier.
const std::string & id2string(const irep_idt &d)
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
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 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)
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...
std::multimap< irep_idt, source_locationt > cycles_r_loc
void collect_cycles_by_SCCs(memory_modelt model)
Note: can be distributed (#define DISTRIBUTED)
static irep_idt entry_point()
std::multimap< irep_idt, source_locationt > id2loc
std::multimap< irep_idt, source_locationt > id2cycloc
goto_function_templatet< goto_programt > goto_functiont
void instrument_with_strategy(instrumentation_strategyt strategy)
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
void weak_memory(memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, 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::multimap< irep_idt, source_locationt > cycles_loc
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
static std::set< event_idt > extract_my_events()
irep_idt base_name
Base (non-scoped) name.
#define Forall_goto_functions(it, functions)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
std::set< irep_idt > cycles
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
std::vector< std::set< event_idt > > egraph_SCCs
std::vector< std::set< event_grapht::critical_cyclet > > set_of_cycles_per_SCC