#include <memory_model_pso.h>

Inheritance diagram for memory_model_psot:

Collaboration diagram for memory_model_psot:

Public Member Functions
	memory_model_psot (const namespacet &_ns)

virtual void	operator() (symex_target_equationt &equation, message_handlert &)

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

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

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

Protected Member Functions
virtual bool	program_order_is_relaxed (partial_order_concurrencyt::event_it e1, partial_order_concurrencyt::event_it e2) const

Protected Member Functions inherited from memory_model_tsot
virtual exprt	before (event_it e1, event_it e2)

void	program_order (symex_target_equationt &equation)

Protected Member Functions inherited from memory_model_sct
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.

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.

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.

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.

Protected Types inherited from memory_model_baset
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

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

Protected Attributes inherited from memory_model_baset
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

Detailed Description

Definition at line 17 of file memory_model_pso.h.

Constructor & Destructor Documentation

◆ memory_model_psot()

memory_model_psot::memory_model_psot ( const namespacet & _ns )

inlineexplicit

Definition at line 20 of file memory_model_pso.h.

Member Function Documentation

◆ operator()()

void memory_model_psot::operator()	(	symex_target_equationt &	equation,
		message_handlert &	message_handler
	)

virtual

Reimplemented from memory_model_tsot.

Definition at line 14 of file memory_model_pso.cpp.

◆ program_order_is_relaxed()

bool memory_model_psot::program_order_is_relaxed	(	partial_order_concurrencyt::event_it	e1,
		partial_order_concurrencyt::event_it	e2
	)		const

protectedvirtual

Reimplemented from memory_model_tsot.

Definition at line 31 of file memory_model_pso.cpp.

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

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

Public Member Functions