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.

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].

- Protected Member Functions inherited from partial_order_concurrencyt

void build_event_lists (symex_target_equationt &equation, message_handlert &message_handler)

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)

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.

irep_idt address (event_it event) const

Produce an address ID for an event.

symbol_exprt clock (event_it e, axiomt axiom)

Produce a clock symbol for some event.

void build_clock_type ()

Initialize the clock_type so that it can be used to number events.

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.

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.

virtual exprt before (event_it e1, event_it e2)=0

Protected Attributes

unsigned var_cnt

choice_symbolst choice_symbols

- Protected Attributes inherited from partial_order_concurrencyt

const namespacet & ns

address_mapt address_map

numberingt numbering

typet clock_type

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

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

- Static Protected Member Functions inherited from partial_order_concurrencyt

static irep_idt id (event_it event)

Produce the symbol ID for an event.

Detailed Description

Definition at line 17 of file memory_model.h.

Member Typedef Documentation

◆ choice_symbolst

typedef std::map<std::pair<event_it, event_it>, symbol_exprt> memory_model_baset::choice_symbolst

protected

Definition at line 38 of file memory_model.h.

◆ per_thread_mapt

typedef std::map<unsigned, event_listt> memory_model_baset::per_thread_mapt

protected

Definition at line 60 of file memory_model.h.

Constructor & Destructor Documentation

◆ memory_model_baset()

memory_model_baset::memory_model_baset ( const namespacet & _ns )

explicit

Definition at line 16 of file memory_model.cpp.

◆ ~memory_model_baset()

memory_model_baset::~memory_model_baset ( )

virtual

Definition at line 21 of file memory_model.cpp.

Member Function Documentation

◆ nondet_bool_symbol()

symbol_exprt memory_model_baset::nondet_bool_symbol ( const std::string & prefix )

protected

Definition at line 25 of file memory_model.cpp.

◆ operator()()

virtual void memory_model_baset::operator() ( symex_target_equationt & ,

message_handlert &

)

pure virtual

Implemented in memory_model_psot, memory_model_sct, and memory_model_tsot.

◆ po()

bool memory_model_baset::po ( event_it e1,

event_it e2

)

protected

In-thread program order.

Parameters: e1 preceding event

e2 following event

Returns: true if e1 precedes e2 in program order

Definition at line 31 of file memory_model.cpp.

◆ read_from()

void memory_model_baset::read_from ( symex_target_equationt & equation )

protected

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.

Parameters: equation symex equation where the new constraint should be added

Definition at line 43 of file memory_model.cpp.

◆ register_read_from_choice_symbol()

symbol_exprt memory_model_baset::register_read_from_choice_symbol ( const event_it & r,

const event_it & w,

symex_target_equationt & equation

)

protected

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].

Parameters: r read event

w write event

equation symex equation where the new constraints should be added

Returns: the new choice symbol

Definition at line 83 of file memory_model.cpp.

Member Data Documentation

◆ choice_symbols

choice_symbolst memory_model_baset::choice_symbols

protected

Definition at line 39 of file memory_model.h.

◆ var_cnt

unsigned memory_model_baset::var_cnt

protected

Definition at line 33 of file memory_model.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/memory_model.h
/home/runner/work/cbmc/cbmc/src/goto-symex/memory_model.cpp