Class of TSO trace step. More...

#include <sc_manual.h>

Inheritance diagram for ilang::ScTraceStep:

Public Types
typedef std::shared_ptr < TraceStep >	TraceStepPtr
	Type of trace step pointer.

Public Types inherited from ilang::TraceStep
enum	TraceStepType { INST_EVT, FACET_EVT, INIT_EVT, FINAL_EVT }
	The type of trace step type.

typedef z3::expr	ZExpr
	Type alias for z3::expr.

typedef std::vector< ZExpr >	ZExprVec
	Type for containing a set of z3::expr.

typedef std::shared_ptr < TraceStep >	TraceStepPtr
	Type of trace step pointer.

typedef std::set< TraceStepPtr >	TraceStepPtrSet
	Type of set of trace steps.

typedef std::set< std::string >	StateNameSet
	Type of state name set.

typedef std::vector< std::pair < ExprPtr, ExprPtr > >	AddrDataVec
	Type of (addr,data) pair vector.

typedef std::unordered_map < std::string, AddrDataVec >	MRFVal
	Map from state name to memory read pair.

Public Member Functions
	ScTraceStep (const InstrPtr &inst, ZExprVec &cstr, z3::context &ctx, size_t pos)
	To create a trace step (for inst, we don't need it for facet/init)

Public Member Functions inherited from ilang::TraceStep
InstrLvlAbsPtr	host () const
	Return the host ILA.

std::string	name () const
	Return the name.

const StateNameSet &	get_inst_read_set () const
	Return the set of states read by inst/parent-inst.

const StateNameSet &	get_inst_write_set () const
	Return the set of states written by inst/parent-inst.

const TraceStepType &	type () const
	Return the type of the trace step.

bool	is_init_tracestep () const
	Decide if the trace step is the initial trace step (a short-cut)

bool	is_facet_tracestep () const
	Decide if the trace step is the facet trace step (a short-cut)

bool	is_final_tracestep () const
	Decide if the trace step is the facet trace step (a short-cut)

InstrPtr	inst () const
	Return the associated instruction for facet / instruction event.

size_t	pos_suffix () const

Z3ExprAdapter &	z3adapter () const
	Return the adapter.

z3::context &	ctx ()
	Return the context (for variable creation)

ExprPtr	final_property ()
	Return final property.

	TraceStep (const InstrPtr &inst, ZExprVec &cstr, z3::context &ctx, size_t pos)

	TraceStep (const InstrPtr &inst, ZExprVec &cstr, z3::context &ctx, ZExpr _ts_overwrite, size_t pos)

	TraceStep (const InstrPtr &ref_inst, ZExprVec &cstr, z3::context &ctx, const std::string &fevt_name, size_t pos)
	To create a facet event: FACET_EVT.

	TraceStep (const ExprPtr &property, ZExprVec &cstr, z3::context &ctx, const InstrLvlAbsPtr &host)
	To create a final event: FINAL_EVT.

virtual	~TraceStep ()
	Destructor, make it virtual.

void	AddStateAccess (const std::string &name, AccessType acc_type)
	To update the set for FACET_EVT.

void	AddStateAccess (const StateNameSet &s, AccessType acc_type)
	To update the set for FACET_EVT.

ZExpr	ConvertZ3OnThisStep (const ExprPtr &ast) const

bool	Access (AccessType acc_type, const std::string &name) const
	To determine if the instruction READ/WRITE a certain state.

bool	Access (AccessType acc_type, const StateNameSet &stateset) const
	To determine if the instruction READ/WRITE a certain set.

std::string	Print (z3::model &m) const
	Print out a trace step for debug purpose.

Additional Inherited Members
Protected Attributes inherited from ilang::TraceStep
TraceStepType	_type
	the type of this trace step (event)

InstrPtr	_inst
	The pointer to the instruction executed in this step.

InstrPtr	_parent_inst
	The pointer to the referred instruction.

StateNameSet	_read_state_set

StateNameSet	_write_state_set

StateNameSet	_inst_read_set
	Set of states (that are read by inst or parent-inst)

StateNameSet	_inst_write_set
	Set of states (that are written by inst or parent-inst)

ZExprVec &	_cstr

std::string	_name
	The name of trace step.

z3::expr	timestamp
	The time stamp.

size_t	_pos_suffix
	The relative position.

Z3ExprAdapter	_expr2z3_
	Keep an adapter that trace steps (won't shared w. others)

z3::context &	_ctx_
	Keep a context to allocate z3 vars.

InstrLvlAbsPtr	_host_final_
	Host for Final Event.

ExprPtr	_final_property
	The cache for the property to witness on the final step.

Detailed Description

Class of TSO trace step.

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

sc_manual.h

Public Types

Public Member Functions

Additional Inherited Members

Detailed Description