ilang  0.9.1
ILAng: A Modeling and Verification Platform for SoCs
Public Types | Public Member Functions | Protected Attributes | Friends | List of all members
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:
ilang::ScTraceStep ilang::TsoTraceStep

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< ZExprZExprVec
 Type for containing a set of z3::expr.
 
typedef std::shared_ptr< TraceStepTraceStepPtr
 Type of trace step pointer.
 
typedef std::set< TraceStepPtrTraceStepPtrSet
 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, AddrDataVecMRFVal
 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 StateNameSetget_inst_read_set () const
 Return the set of states read by inst/parent-inst.
 
const StateNameSetget_inst_write_set () const
 Return the set of states written by inst/parent-inst.
 
const TraceStepTypetype () 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
 
Z3ExprAdapterz3adapter () 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

◆ TraceStep() [1/2]

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

◆ TraceStep() [2/2]

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

◆ ConvertZ3OnThisStep()

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)

◆ pos_suffix()

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

◆ _cstr

ZExprVec& ilang::TraceStep::_cstr
protected

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

◆ _read_state_set

StateNameSet ilang::TraceStep::_read_state_set
protected

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

◆ _write_state_set

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: