#include <memory_model.h>

Inheritance diagram for memory_model_baset:

Collaboration diagram for memory_model_baset:

Public Member Functions
	memory_model_baset (const namespacet &_ns)

virtual	~memory_model_baset ()

virtual void	operator() (symex_target_equationt &, message_handlert &)=0

Public Member Functions inherited from partial_order_concurrencyt
	partial_order_concurrencyt (const namespacet &_ns)

virtual	~partial_order_concurrencyt ()

Protected Types
typedef std::map< std::pair< event_it, event_it >, symbol_exprt >	choice_symbolst

typedef std::map< unsigned, event_listt >	per_thread_mapt

Protected Types inherited from partial_order_concurrencyt
typedef std::vector< event_it >	event_listt

typedef std::map< irep_idt, a_rect >	address_mapt

typedef std::map< event_it, unsigned >	numberingt

Protected Member Functions
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 &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) 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...

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

Static Protected Member Functions inherited from partial_order_concurrencyt
static irep_idt	id (event_it event)
	Produce the symbol ID for an event. More...

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-documentation/cbmc-documentation/src/goto-symex/memory_model.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-symex/memory_model.cpp

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ choice_symbolst

◆ per_thread_mapt

Constructor & Destructor Documentation

◆ memory_model_baset()

◆ ~memory_model_baset()

Member Function Documentation

◆ nondet_bool_symbol()

◆ operator()()

◆ po()

◆ read_from()

◆ register_read_from_choice_symbol()

Member Data Documentation

◆ choice_symbols

◆ var_cnt