cprover
|
#include <shared_buffers.h>
Classes | |
class | cfg_visitort |
class | varst |
Public Types | |
typedef std::map< irep_idt, varst > | var_mapt |
Public Member Functions | |
shared_bufferst (symbol_tablet &_symbol_table, unsigned _nb_threads, messaget &_message) | |
void | set_cav11 (memory_modelt model) |
const varst & | operator() (const irep_idt &object) |
instruments the variable More... | |
void | add_initialization_code (goto_functionst &goto_functions) |
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) More... | |
void | flush_read (goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object) |
flushes read (POWER) More... | |
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 More... | |
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) More... | |
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 More... | |
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 More... | |
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) |
bool | track (const irep_idt &id) const |
irep_idt | choice (const irep_idt &function, const std::string &suffix) |
bool | is_buffered (const namespacet &, const symbol_exprt &, bool is_write) |
bool | is_buffered_in_general (const namespacet &, const symbol_exprt &, bool is_write) |
void | weak_memory (value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, memory_modelt model, goto_functionst &goto_functions) |
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 shared themselves) whose value could be changed as effect of a read delay More... | |
Public Attributes | |
var_mapt | var_map |
std::set< irep_idt > | cycles |
std::multimap< irep_idt, source_locationt > | cycles_loc |
std::multimap< irep_idt, source_locationt > | cycles_r_loc |
std::set< irep_idt > | affected_by_delay_set |
Protected Member Functions | |
std::string | unique () |
returns a unique id (for fresh variables) More... | |
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 More... | |
irep_idt | add (const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type) |
irep_idt | add_fresh_var (const irep_idt &object, const irep_idt &base_name, const std::string &suffix, const typet &type) |
void | add_initialization (goto_programt &goto_program) |
Protected Attributes | |
class symbol_tablet & | symbol_table |
unsigned | nb_threads |
std::set< irep_idt > | instrumentations |
unsigned | uniq |
bool | cav11 |
messaget & | message |
Definition at line 28 of file shared_buffers.h.
typedef std::map<irep_idt, varst> shared_bufferst::var_mapt |
Definition at line 76 of file shared_buffers.h.
|
inline |
Definition at line 31 of file shared_buffers.h.
|
protected |
add a new var for instrumenting the input var
Definition at line 80 of file shared_buffers.cpp.
References symbolt::base_name, id2string(), instrumentations, symbolt::is_static_lifetime, irept::make_nil(), symbol_tablet::move(), symbolt::name, symbol_table, symbolt::type, and symbolt::value.
Referenced by add(), add_fresh_var(), choice(), and operator()().
|
inlineprotected |
Definition at line 253 of file shared_buffers.h.
References add().
|
protected |
Definition at line 104 of file shared_buffers.cpp.
References assignment(), goto_program_templatet< codeT, guardT >::instructions, irept::make_nil(), pointer_type(), symbol_table, and var_map.
Referenced by add_initialization_code().
void shared_bufferst::add_initialization_code | ( | goto_functionst & | goto_functions | ) |
Definition at line 133 of file shared_buffers.cpp.
References add_initialization(), goto_functions_templatet< bodyT >::entry_point(), goto_functions_templatet< bodyT >::function_map, and main().
Referenced by weak_memory().
void shared_bufferst::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 shared themselves) whose value could be changed as effect of a read delay
Definition at line 1015 of file shared_buffers.cpp.
References affected_by_delay_set, messaget::debug(), messaget::eom(), Forall_goto_functions, Forall_goto_program_instructions, forall_rw_set_r_entries, forall_rw_set_w_entries, id2string(), is_buffered_in_general(), message, and symbol_table.
Referenced by weak_memory().
void shared_bufferst::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
Definition at line 148 of file shared_buffers.cpp.
References ASSIGN, messaget::eom(), id2string(), goto_program_templatet< codeT, guardT >::insert_before(), namespacet::lookup(), message, pos(), symbol_table, and messaget::warning().
Referenced by add_initialization(), assignment(), delay_read(), det_flush(), flush_read(), nondet_flush(), shared_bufferst::cfg_visitort::weak_memory(), and write().
|
inline |
Definition at line 134 of file shared_buffers.h.
References assignment(), namespacet::lookup(), and symbol_table.
Definition at line 159 of file shared_buffers.h.
References add(), symbolt::base_name, symbol_tablet::has_symbol(), id2string(), symbol_tablet::lookup(), and symbol_table.
Referenced by nondet_flush(), and shared_bufferst::cfg_visitort::weak_memory().
void shared_bufferst::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)
Definition at line 187 of file shared_buffers.cpp.
References add_fresh_var(), assignment(), messaget::debug(), messaget::eom(), id2string(), message, shared_bufferst::varst::read_delayed, shared_bufferst::varst::read_delayed_var, shared_bufferst::varst::type, and unique().
Referenced by shared_bufferst::cfg_visitort::weak_memory().
void shared_bufferst::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)
Definition at line 335 of file shared_buffers.cpp.
References assignment(), messaget::debug(), messaget::eom(), id2string(), message, shared_bufferst::varst::r_buff0_thds, shared_bufferst::varst::r_buff1_thds, shared_bufferst::varst::type, shared_bufferst::varst::w_buff0, shared_bufferst::varst::w_buff0_used, shared_bufferst::varst::w_buff1, and shared_bufferst::varst::w_buff1_used.
Referenced by shared_bufferst::cfg_visitort::weak_memory().
void shared_bufferst::flush_read | ( | goto_programt & | goto_program, |
goto_programt::targett & | t, | ||
const source_locationt & | source_location, | ||
const irep_idt & | write_object | ||
) |
flushes read (POWER)
Definition at line 236 of file shared_buffers.cpp.
References assignment(), ASSUME, goto_program_templatet< codeT, guardT >::insert_before(), shared_bufferst::varst::read_delayed, shared_bufferst::varst::read_delayed_var, exprt::source_location(), and shared_bufferst::varst::type.
Referenced by shared_bufferst::cfg_visitort::weak_memory().
bool shared_bufferst::is_buffered | ( | const namespacet & | ns, |
const symbol_exprt & | symbol_expr, | ||
bool | is_write | ||
) |
Definition at line 938 of file shared_buffers.cpp.
References CPROVER_PREFIX, symbol_exprt::get_identifier(), has_prefix(), id2string(), instrumentations, is_buffered_in_general(), symbolt::is_static_lifetime, symbolt::is_thread_local, and namespacet::lookup().
Referenced by shared_bufferst::cfg_visitort::weak_memory().
bool shared_bufferst::is_buffered_in_general | ( | const namespacet & | ns, |
const symbol_exprt & | symbol_expr, | ||
bool | is_write | ||
) |
Definition at line 972 of file shared_buffers.cpp.
References cav11, cycles, cycles_loc, symbol_exprt::get_identifier(), and exprt::source_location().
Referenced by affected_by_delay(), and is_buffered().
void shared_bufferst::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
Definition at line 441 of file shared_buffers.cpp.
References assignment(), choice(), cycles, cycles_loc, messaget::debug(), messaget::eom(), shared_bufferst::varst::flush_delayed, id2string(), shared_bufferst::varst::mem_tmp, message, shared_bufferst::varst::r_buff0_thds, shared_bufferst::varst::r_buff1_thds, shared_bufferst::varst::type, shared_bufferst::varst::w_buff0, shared_bufferst::varst::w_buff0_used, shared_bufferst::varst::w_buff1, shared_bufferst::varst::w_buff1_used, and messaget::warning().
Referenced by shared_bufferst::cfg_visitort::weak_memory().
const shared_bufferst::varst & shared_bufferst::operator() | ( | const irep_idt & | object | ) |
instruments the variable
Definition at line 23 of file shared_buffers.cpp.
References add(), symbolt::base_name, nb_threads, pointer_type(), symbol_table, symbolt::type, and var_map.
|
inline |
Definition at line 41 of file shared_buffers.h.
Referenced by weak_memory().
|
inline |
Definition at line 146 of file shared_buffers.h.
References CPROVER_PREFIX, has_prefix(), id2string(), symbolt::is_thread_local, namespacet::lookup(), and symbol_table.
|
protected |
returns a unique id (for fresh variables)
Definition at line 16 of file shared_buffers.cpp.
References messaget::debug(), messaget::eom(), message, and uniq.
Referenced by delay_read().
void shared_bufferst::weak_memory | ( | value_setst & | value_sets, |
symbol_tablet & | symbol_table, | ||
goto_programt & | goto_program, | ||
memory_modelt | model, | ||
goto_functionst & | goto_functions | ||
) |
void shared_bufferst::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
Definition at line 272 of file shared_buffers.cpp.
References ASSERT, assignment(), messaget::debug(), messaget::eom(), id2string(), goto_program_templatet< codeT, guardT >::insert_before(), message, nb_threads, shared_bufferst::varst::r_buff0_thds, shared_bufferst::varst::r_buff1_thds, exprt::type(), shared_bufferst::varst::w_buff0, shared_bufferst::varst::w_buff0_used, shared_bufferst::varst::w_buff1, and shared_bufferst::varst::w_buff1_used.
Referenced by shared_bufferst::cfg_visitort::weak_memory().
std::set<irep_idt> shared_bufferst::affected_by_delay_set |
Definition at line 233 of file shared_buffers.h.
Referenced by affected_by_delay(), weak_memory(), and shared_bufferst::cfg_visitort::weak_memory().
|
protected |
Definition at line 241 of file shared_buffers.h.
Referenced by is_buffered_in_general(), and set_cav11().
std::set<irep_idt> shared_bufferst::cycles |
Definition at line 81 of file shared_buffers.h.
Referenced by is_buffered_in_general(), nondet_flush(), and weak_memory().
std::multimap<irep_idt, source_locationt> shared_bufferst::cycles_loc |
Definition at line 83 of file shared_buffers.h.
Referenced by is_buffered_in_general(), nondet_flush(), and weak_memory().
std::multimap<irep_idt, source_locationt> shared_bufferst::cycles_r_loc |
Definition at line 85 of file shared_buffers.h.
Referenced by weak_memory().
|
protected |
Definition at line 229 of file shared_buffers.h.
Referenced by add(), and is_buffered().
|
protected |
Definition at line 244 of file shared_buffers.h.
Referenced by affected_by_delay(), assignment(), delay_read(), det_flush(), nondet_flush(), unique(), shared_bufferst::cfg_visitort::weak_memory(), and write().
|
protected |
Definition at line 226 of file shared_buffers.h.
Referenced by operator()(), and write().
|
protected |
Definition at line 223 of file shared_buffers.h.
Referenced by add(), add_initialization(), affected_by_delay(), assignment(), choice(), operator()(), and track().
|
protected |
Definition at line 237 of file shared_buffers.h.
Referenced by unique().
var_mapt shared_bufferst::var_map |
Definition at line 77 of file shared_buffers.h.
Referenced by add_initialization(), and operator()().