cprover
shared_bufferst Class Reference

#include <shared_buffers.h>

Collaboration diagram for shared_bufferst:
[legend]

Classes

class  cfg_visitort
 
class  varst
 

Public Types

typedef std::map< irep_idt, varstvar_mapt
 

Public Member Functions

 shared_bufferst (symbol_tablet &_symbol_table, unsigned _nb_threads, messaget &_message)
 
void set_cav11 (memory_modelt model)
 
const varstoperator() (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_idtcycles
 
std::multimap< irep_idt, source_locationtcycles_loc
 
std::multimap< irep_idt, source_locationtcycles_r_loc
 
std::set< irep_idtaffected_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_tabletsymbol_table
 
unsigned nb_threads
 
std::set< irep_idtinstrumentations
 
unsigned uniq
 
bool cav11
 
messagetmessage
 

Detailed Description

Definition at line 28 of file shared_buffers.h.

Member Typedef Documentation

§ var_mapt

Definition at line 76 of file shared_buffers.h.

Constructor & Destructor Documentation

§ shared_bufferst()

shared_bufferst::shared_bufferst ( symbol_tablet _symbol_table,
unsigned  _nb_threads,
messaget _message 
)
inline

Definition at line 31 of file shared_buffers.h.

Member Function Documentation

§ add() [1/2]

irep_idt shared_bufferst::add ( const irep_idt object,
const irep_idt base_name,
const std::string &  suffix,
const typet type,
bool  instrument 
)
protected

add a new var for instrumenting the input var

parameters: var, suffix, type of the var, added as an instrumentation
Returns
identifier of the new 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()().

§ add() [2/2]

irep_idt shared_bufferst::add ( const irep_idt object,
const irep_idt base_name,
const std::string &  suffix,
const typet type 
)
inlineprotected

Definition at line 253 of file shared_buffers.h.

References add().

§ add_fresh_var()

irep_idt shared_bufferst::add_fresh_var ( const irep_idt object,
const irep_idt base_name,
const std::string &  suffix,
const typet type 
)
inlineprotected

Definition at line 263 of file shared_buffers.h.

References add(), and add_initialization().

Referenced by delay_read().

§ add_initialization()

void shared_bufferst::add_initialization ( goto_programt goto_program)
protected

§ add_initialization_code()

void shared_bufferst::add_initialization_code ( goto_functionst goto_functions)

§ affected_by_delay()

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(), and message.

Referenced by choice(), and weak_memory().

§ assignment() [1/2]

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 
)

§ assignment() [2/2]

void shared_bufferst::assignment ( goto_programt goto_program,
goto_programt::targett t,
const source_locationt source_location,
const irep_idt id_lhs,
const irep_idt id_rhs 
)
inline

Definition at line 134 of file shared_buffers.h.

References assignment(), namespacet::lookup(), and symbol_table.

§ choice()

irep_idt shared_bufferst::choice ( const irep_idt function,
const std::string &  suffix 
)
inline

§ delay_read()

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 
)

§ det_flush()

§ flush_read()

void shared_bufferst::flush_read ( goto_programt goto_program,
goto_programt::targett t,
const source_locationt source_location,
const irep_idt write_object 
)

§ is_buffered()

bool shared_bufferst::is_buffered ( const namespacet ns,
const symbol_exprt symbol_expr,
bool  is_write 
)

§ is_buffered_in_general()

bool shared_bufferst::is_buffered_in_general ( const namespacet ns,
const symbol_exprt symbol_expr,
bool  is_write 
)

§ nondet_flush()

§ operator()()

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.

§ set_cav11()

void shared_bufferst::set_cav11 ( memory_modelt  model)
inline

Definition at line 41 of file shared_buffers.h.

References cav11, and TSO.

Referenced by weak_memory().

§ track()

bool shared_bufferst::track ( const irep_idt id) const
inline

§ unique()

std::string shared_bufferst::unique ( void  )
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().

§ weak_memory()

void shared_bufferst::weak_memory ( value_setst value_sets,
symbol_tablet symbol_table,
goto_programt goto_program,
memory_modelt  model,
goto_functionst goto_functions 
)

§ write()

Member Data Documentation

§ affected_by_delay_set

std::set<irep_idt> shared_bufferst::affected_by_delay_set

Definition at line 233 of file shared_buffers.h.

Referenced by affected_by_delay(), and weak_memory().

§ cav11

bool shared_bufferst::cav11
protected

Definition at line 241 of file shared_buffers.h.

Referenced by is_buffered_in_general(), and set_cav11().

§ cycles

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().

§ cycles_loc

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().

§ cycles_r_loc

std::multimap<irep_idt, source_locationt> shared_bufferst::cycles_r_loc

Definition at line 85 of file shared_buffers.h.

Referenced by weak_memory().

§ instrumentations

std::set<irep_idt> shared_bufferst::instrumentations
protected

Definition at line 229 of file shared_buffers.h.

Referenced by add(), and is_buffered().

§ message

messaget& shared_bufferst::message
protected

§ nb_threads

unsigned shared_bufferst::nb_threads
protected

Definition at line 226 of file shared_buffers.h.

Referenced by operator()(), and write().

§ symbol_table

class symbol_tablet& shared_bufferst::symbol_table
protected

§ uniq

unsigned shared_bufferst::uniq
protected

Definition at line 237 of file shared_buffers.h.

Referenced by unique().

§ var_map

var_mapt shared_bufferst::var_map

Definition at line 77 of file shared_buffers.h.

Referenced by add_initialization(), and operator()().


The documentation for this class was generated from the following files: