Class of TSO. More...

#include <tso_manual.h>

Inheritance diagram for ilang::Tso:

Public Types
typedef std::shared_ptr < TsoTraceStep >	TsoTraceStepPtr
	Type of trace step pointer.

typedef std::set< TsoTraceStepPtr >	TsoTraceStepPtrSet
	Type of trace steps, we need to collect the set of trace steps (WRITE)

Public Types inherited from ilang::MemoryModel
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
virtual void	RegisterSteps (size_t regIdx, const InstrVec &_inst_seq) override

virtual void	FinishRegisterSteps () override

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

virtual void	SetFinalProperty (const ExprPtr &property) override
	Set the final property, this is implementation-specific.

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

Public Member Functions inherited from ilang::MemoryModel
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	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	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.

Static Public Attributes
static InterIlaUnroller::MemoryModelCreator	TsoModel
	Declaration of memory model creator that chooses Tso.

Protected Attributes
TraceStepPtrSet	WRITE_list

TraceStepPtrSet	READ_list

TraceStepPtrSet	FENCE_list

TraceStepPtrSet	RMW_list

TraceStepPtrSet	PureWrite_list

Protected Attributes inherited from ilang::MemoryModel
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.

Additional Inherited Members
Protected Types inherited from ilang::MemoryModel
enum	StaticResult { STATIC_TRUE = 1, STATIC_FALSE, STATIC_UNKNOWN }

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

Protected Member Functions inherited from ilang::MemoryModel
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)