ilang::TraceStep Class Reference

The class for trace step (an instance of instruction) As in the unrolling, there may be multiple instances of the same instructions, so we have the trace steps. More...

#include <memory_model.h>

Inheritance diagram for ilang::TraceStep:

Public Types
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
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.

Protected Attributes
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.

Friends
class	MemoryModel
	Add friend, so it can get access to the types.

Detailed Description

The class for trace step (an instance of instruction) As in the unrolling, there may be multiple instances of the same instructions, so we have the trace steps.

Constructor & Destructor Documentation

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

To create a trace step, you need to know the instruction also should give a constraint set: INST_EVT

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

This function allows you to overwrite the timestamp instead of creating a new one: INIT_EVT

Member Function Documentation

ZExpr ilang::TraceStep::ConvertZ3OnThisStep

(

const ExprPtr &

ast

)

const

Translate an arbitrary expr using the frame number of this step (so it refers to the var used in this step)

size_t ilang::TraceStep::pos_suffix

(

)

const

Return the position suffix (for facet, they should have the same suffix as the main step to ensure they use the same var)

Member Data Documentation

ZExprVec& ilang::TraceStep::_cstr

protected

The reference to the constratint set, so it can add constraints when needed

StateNameSet ilang::TraceStep::_read_state_set

protected

Set of states (should be global) that are read by this event: Type : FACET_EVT

StateNameSet ilang::TraceStep::_write_state_set

protected

Set of states (should be global) that are written by this event: Type : FACET_EVT

---

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

• memory_model.h