The base class for memory models. More...

#include <memory_model.h>

Inheritance diagram for ilang::MemoryModel:

Public Types
using	ZExpr = TraceStep::ZExpr
	Type alias for z3::expr.

using	ZExprVec = TraceStep::ZExprVec
	Type for containing a vector of z3::expr.

using	TraceStepPtr = TraceStep::TraceStepPtr
	Type of trace step shared pointers.

using	TraceStepPtrSet = TraceStep::TraceStepPtrSet
	Type of trace steps, we need to collect the set of trace steps (WRITE)

using	TraceStepType = TraceStep::TraceStepType
	Type of trace step type, INIT/INST/FACET.

using	StateNameSet = TraceStep::StateNameSet
	Type of set of state names.

using	AddrDataVec = TraceStep::AddrDataVec
	Type of vector of (addr,data) pair.

typedef std::vector< InstrPtr >	InstrVec
	Type of an instruction vector to represent a sequence.

typedef std::vector< InstrVec >	ProgramTemplate

typedef std::vector < std::vector< TraceStepPtr > >	PerILATraceStepPtrSet

typedef std::map< std::string, StateNameSet >	ILANameStateNameSetMap
	Type of map ila-name to state-set.

Public Member Functions
ZExpr	ConvertZ3 (const ExprPtr &ast, const std::string &suffix) const
	Return the z3 converter used by this memory model.

virtual void	InitSize (const ProgramTemplate &_tmpl)
	To initialize the inner storage space.

virtual void	RegisterSteps (size_t regIdx, const InstrVec &_inst_seq)=0

virtual void	FinishRegisterSteps ()=0

virtual void	ApplyAxioms ()=0
	To apply the axioms, the complete program should be given.

virtual void	SetLocalState (const std::vector< bool > &ordered)

virtual void	AddSingleTraceStepProperty (const ExprPtr &property, std::function< bool(const TraceStep &)> filter)
	Assert a property that some trace step (decided by filter) should follow.

virtual void	GetSingleTraceStepProperty (const ExprPtr &property, std::function< bool(const TraceStep &)> filter, std::function< void(const z3::expr &)> collector)
	Get the z3 expression of a property on a trace step.

virtual void	SetFinalProperty (const ExprPtr &property)=0
	Set the assertion on the final state.

virtual void	AddDoubleTraceStepProperty (std::function< z3::expr(const TraceStep &, const TraceStep &)>, std::function< bool(const TraceStep &, const TraceStep &)>)

	MemoryModel (z3::context &ctx, ZExprVec &_cstrlist, const StateNameSet &shared_states, const ILANameStateNameSetMap &private_states, const InstrLvlAbsPtr &global_ila_ptr)

const TraceStepPtrSet &	GetAllTraceSteps () const
	Determine if an instruction access a shared state.

Protected Types
enum	StaticResult { STATIC_TRUE = 1, STATIC_FALSE, STATIC_UNKNOWN }

enum	AxiomFuncHint { HINT_NONE = 0, HINT_READ = 1, HINT_WRITE }

Protected Member Functions
z3::context &	ctx () const
	Return the context (for variable creation)

TraceStepPtr	CreateGlobalInitStep ()
	A function for dervied classes to create init trace step.

TraceStepPtr	CreateGlobalFinalStep (const ExprPtr &property)
	A function for dervied classes to create final trace step.

z3::expr	HB (const TraceStep &l, const TraceStep &r) const

z3::expr	Sync (const TraceStep &l, const TraceStep &r) const

z3::expr	PO (const TraceStep &l, const TraceStep &r) const

z3::expr	SameAddress (const TraceStep &l, const TraceStep &r, const std::string &sname, AxiomFuncHint lhint=HINT_NONE, AxiomFuncHint rhint=HINT_NONE) const

z3::expr	Decode (const TraceStep &l) const

z3::expr	SameData (const TraceStep &l, const TraceStep &r, const std::string &sname, AxiomFuncHint lhint=HINT_NONE, AxiomFuncHint rhint=HINT_NONE) const

bool	SameCore (const TraceStep &l, const TraceStep &r) const

StaticResult	SameAddressStatic (const TraceStep &l, const TraceStep &r) const

StaticResult	DecodeStatic (const TraceStep &l) const

StaticResult	SameCoreStatic (const TraceStep &l, const TraceStep &r) const

z3::expr	Z3ForallList (const ZExprVec &l) const
	This is to deal with forall (if does not exist, it should be true also)

z3::expr	Z3ExistsList (const ZExprVec &l) const
	This is to apply to exists, (if does not exist, it should be false)

Protected Attributes
TraceStepPtr	_init_trace_step
	The pointer to the initial trace step.

TraceStepPtr	_final_trace_step
	The pointer to the final trace step.

TraceStepPtrSet	_all_trace_steps
	The set of all trace steps.

TraceStepPtrSet	_all_inst_trace_steps
	The set of all instruction trace steps.

PerILATraceStepPtrSet	_ila_trace_steps

const StateNameSet &	m_shared_state_names
	The set of names of shared states.

const ILANameStateNameSetMap &	m_ila_private_state_names
	The internal storage of all private states of all ilas.

InstrLvlAbsPtr	m_p_global_ila
	The pointer to the (dummy) global ILA.

z3::context &	_ctx_

ZExprVec &	_constr
	A reference to the constraint list.

Z3ExprAdapter	_expr2z3_

NestedMemAddrDataAvoider	nested_finder_
	An AST traversor, make sure there are no nested asts.

Detailed Description

The base class for memory models.

Member Typedef Documentation

typedef std::vector<std::vector<TraceStepPtr> > ilang::MemoryModel::PerILATraceStepPtrSet

Type of TraceStep set grouped by ILA (the same sequence as given to the register steps)

typedef std::vector<InstrVec> ilang::MemoryModel::ProgramTemplate

Type of a vector of instruction sequences (currently please represent holes via 0-ary functions)

Member Function Documentation

virtual void ilang::MemoryModel::AddDoubleTraceStepProperty	(	std::function< z3::expr(const TraceStep &, const TraceStep &)>	,
		std::function< bool(const TraceStep &, const TraceStep &)>
	)

virtual

Assert a property that some pair of trace steps (decided by filter) should follow

virtual void ilang::MemoryModel::FinishRegisterSteps ( )

pure virtual

To do some extra bookkeeping work when it is known that no more instruction steps are needed.

Implemented in ilang::Tso, and ilang::Sc.

virtual void ilang::MemoryModel::RegisterSteps	(	size_t	regIdx,
		const InstrVec &	_inst_seq
	)

pure virtual

To create more view operations associated with an instruction, and also to add them to the set

Implemented in ilang::Tso, and ilang::Sc.

virtual void ilang::MemoryModel::SetLocalState ( const std::vector< bool > & ordered )

virtual

To constrain on the local states, based on whether they are in order or not, can be overwritten by the specific model.

Member Data Documentation

z3::context& ilang::MemoryModel::_ctx_

protected

A reference to Z3 context , even in the sence of const, it should allow us to allocate new variables

Z3ExprAdapter ilang::MemoryModel::_expr2z3_

mutableprotected

An adapter that trace step can share, will allocate internally, by the constructor

PerILATraceStepPtrSet ilang::MemoryModel::_ila_trace_steps

protected

The set of TraceStep set grouped by ILA (the same sequence as given to the register steps)

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

memory_model.h

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

Member Function Documentation

Member Data Documentation