ilang  0.9.1
ILAng: A Modeling and Verification Platform for SoCs
Public Types | Public Member Functions | List of all members
ilang::ScTraceStep Class Reference

Class of TSO trace step. More...

#include <sc_manual.h>

Inheritance diagram for ilang::ScTraceStep:
ilang::TraceStep

Public Types

typedef std::shared_ptr< TraceStepTraceStepPtr
 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< 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

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

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: