cprover
memory_model_sct Class Reference

#include <memory_model_sc.h>

+ Inheritance diagram for memory_model_sct:
+ Collaboration diagram for memory_model_sct:

Public Member Functions

 memory_model_sct (const namespacet &_ns)
 
virtual void operator() (symex_target_equationt &equation)
 
- Public Member Functions inherited from memory_model_baset
 memory_model_baset (const namespacet &_ns)
 
virtual ~memory_model_baset ()
 
- Public Member Functions inherited from partial_order_concurrencyt
 partial_order_concurrencyt (const namespacet &_ns)
 
virtual ~partial_order_concurrencyt ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

Protected Member Functions

virtual exprt before (event_it e1, event_it e2)
 
virtual bool program_order_is_relaxed (partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const
 
void build_per_thread_map (const symex_target_equationt &equation, per_thread_mapt &dest) const
 
void thread_spawn (symex_target_equationt &equation, const per_thread_mapt &per_thread_map)
 
void program_order (symex_target_equationt &equation)
 
void from_read (symex_target_equationt &equation)
 
void write_serialization_external (symex_target_equationt &equation)
 
- Protected Member Functions inherited from memory_model_baset
bool po (event_it e1, event_it e2)
 In-thread program order. More...
 
symbol_exprt nondet_bool_symbol (const std::string &prefix)
 
void read_from (symex_target_equationt &equation)
 For each read r from every address we collect the choice symbols S via register_read_from_choice_symbol (for potential read-write pairs) and add a constraint r.guard => \/S. More...
 
symbol_exprt register_read_from_choice_symbol (const event_it &r, const event_it &w, symex_target_equationt &equation)
 Introduce a new choice symbol s for the pair (r, w) add constraint s => (w.guard /\ r.lhs=w.lhs) add constraint s => before(w,r) [if w is from another thread]. More...
 
- Protected Member Functions inherited from partial_order_concurrencyt
void build_event_lists (symex_target_equationt &)
 First call add_init_writes then for each shared read/write (or spawn) populate: 1) the address_map (with a list of reads/writes for the address of each event) 2) the numbering map (with per-thread unique number of every event) More...
 
void add_init_writes (symex_target_equationt &)
 For each shared read event and for each shared write event that appears after spawn or has false guard prepend a shared write SSA step with non-deterministic value. More...
 
irep_idt address (event_it event) const
 Produce an address ID for an event. More...
 
symbol_exprt clock (event_it e, axiomt axiom)
 Produce a clock symbol for some event. More...
 
void build_clock_type ()
 Initialize the clock_type so that it can be used to number events. More...
 
void add_constraint (symex_target_equationt &equation, const exprt &cond, const std::string &msg, const symex_targett::sourcet &source) const
 Simplify and add a constraint to equation. More...
 
exprt before (event_it e1, event_it e2, unsigned axioms)
 Build the partial order constraint for two events: if e1 and e2 are in the same atomic section then constrain with equality between their clocks otherwise constrain with e1 clock being less than e2 clock. More...
 

Additional Inherited Members

- Public Types inherited from partial_order_concurrencyt
enum  axiomt { AX_SC_PER_LOCATION =1, AX_NO_THINAIR =2, AX_OBSERVATION =4, AX_PROPAGATION =8 }
 
typedef SSA_stept eventt
 
typedef symex_target_equationt::SSA_stepst eventst
 
typedef eventst::const_iterator event_it
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from partial_order_concurrencyt
static irep_idt rw_clock_id (event_it e, axiomt axiom=AX_PROPAGATION)
 Build identifier for the read/write clock variable. More...
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 
- Protected Types inherited from memory_model_baset
typedef std::map< std::pair< event_it, event_it >, symbol_exprtchoice_symbolst
 
typedef std::map< unsigned, event_listtper_thread_mapt
 
- Protected Types inherited from partial_order_concurrencyt
typedef std::vector< event_itevent_listt
 
typedef std::map< irep_idt, a_rectaddress_mapt
 
typedef std::map< event_it, unsigned > numberingt
 
- Static Protected Member Functions inherited from partial_order_concurrencyt
static irep_idt id (event_it event)
 Produce the symbol ID for an event. More...
 
- Protected Attributes inherited from memory_model_baset
unsigned var_cnt
 
choice_symbolst choice_symbols
 
- Protected Attributes inherited from partial_order_concurrencyt
const namespacetns
 
address_mapt address_map
 
numberingt numbering
 
typet clock_type
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 17 of file memory_model_sc.h.

Constructor & Destructor Documentation

◆ memory_model_sct()

memory_model_sct::memory_model_sct ( const namespacet _ns)
inlineexplicit

Definition at line 20 of file memory_model_sc.h.

Member Function Documentation

◆ before()

exprt memory_model_sct::before ( event_it  e1,
event_it  e2 
)
protectedvirtual

Implements partial_order_concurrencyt.

Reimplemented in memory_model_tsot.

Definition at line 29 of file memory_model_sc.cpp.

◆ build_per_thread_map()

void memory_model_sct::build_per_thread_map ( const symex_target_equationt equation,
per_thread_mapt dest 
) const
protected

Definition at line 45 of file memory_model_sc.cpp.

◆ from_read()

void memory_model_sct::from_read ( symex_target_equationt equation)
protected

Definition at line 248 of file memory_model_sc.cpp.

◆ operator()()

void memory_model_sct::operator() ( symex_target_equationt equation)
virtual

Implements memory_model_baset.

Reimplemented in memory_model_tsot, and memory_model_psot.

Definition at line 16 of file memory_model_sc.cpp.

◆ program_order()

void memory_model_sct::program_order ( symex_target_equationt equation)
protected

Definition at line 149 of file memory_model_sc.cpp.

◆ program_order_is_relaxed()

bool memory_model_sct::program_order_is_relaxed ( partial_order_concurrencyt::event_it  e1,
partial_order_concurrencyt::event_it  e2 
) const
protectedvirtual

Reimplemented in memory_model_tsot, and memory_model_psot.

Definition at line 35 of file memory_model_sc.cpp.

◆ thread_spawn()

void memory_model_sct::thread_spawn ( symex_target_equationt equation,
const per_thread_mapt per_thread_map 
)
protected

Definition at line 66 of file memory_model_sc.cpp.

◆ write_serialization_external()

void memory_model_sct::write_serialization_external ( symex_target_equationt equation)
protected

Definition at line 196 of file memory_model_sc.cpp.


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