ilang  0.9.1
ILAng: A Modeling and Verification Platform for SoCs
Public Types | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
ilang::MemoryModel Class Referenceabstract

The base class for memory models. More...

#include <memory_model.h>

Inheritance diagram for ilang::MemoryModel:
ilang::Sc ilang::Tso

Public Types

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< InstrPtrInstrVec
 Type of an instruction vector to represent a sequence.
 
typedef std::vector< InstrVecProgramTemplate
 
typedef std::vector< std::vector< TraceStepPtr > > PerILATraceStepPtrSet
 
typedef std::map< std::string, StateNameSetILANameStateNameSetMap
 Type of map ila-name to state-set.
 

Public Member Functions

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 RegisterSteps (size_t regIdx, const InstrVec &_inst_seq)=0
 
virtual void FinishRegisterSteps ()=0
 
virtual void ApplyAxioms ()=0
 To apply the axioms, the complete program should be given.
 
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 SetFinalProperty (const ExprPtr &property)=0
 Set the assertion on the final state.
 
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 TraceStepPtrSetGetAllTraceSteps () const
 Determine if an instruction access a shared state.
 

Protected Types

enum  StaticResult { STATIC_TRUE = 1, STATIC_FALSE, STATIC_UNKNOWN }
 
enum  AxiomFuncHint { HINT_NONE = 0, HINT_READ = 1, HINT_WRITE }
 

Protected Member Functions

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)
 

Protected Attributes

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 StateNameSetm_shared_state_names
 The set of names of shared states.
 
const ILANameStateNameSetMapm_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.
 

Detailed Description

The base class for memory models.

Member Typedef Documentation

◆ PerILATraceStepPtrSet

typedef std::vector<std::vector<TraceStepPtr> > ilang::MemoryModel::PerILATraceStepPtrSet

Type of TraceStep set grouped by ILA (the same sequence as given to the register steps)

◆ ProgramTemplate

Type of a vector of instruction sequences (currently please represent holes via 0-ary functions)

Member Function Documentation

◆ AddDoubleTraceStepProperty()

virtual void ilang::MemoryModel::AddDoubleTraceStepProperty ( std::function< z3::expr(const TraceStep &, const TraceStep &)>  ,
std::function< bool(const TraceStep &, const TraceStep &)>   
)
virtual

Assert a property that some pair of trace steps (decided by filter) should follow

◆ FinishRegisterSteps()

virtual void ilang::MemoryModel::FinishRegisterSteps ( )
pure virtual

To do some extra bookkeeping work when it is known that no more instruction steps are needed.

Implemented in ilang::Tso, and ilang::Sc.

◆ RegisterSteps()

virtual void ilang::MemoryModel::RegisterSteps ( size_t  regIdx,
const InstrVec _inst_seq 
)
pure virtual

To create more view operations associated with an instruction, and also to add them to the set

Implemented in ilang::Tso, and ilang::Sc.

◆ SetLocalState()

virtual void ilang::MemoryModel::SetLocalState ( const std::vector< bool > &  ordered)
virtual

To constrain on the local states, based on whether they are in order or not, can be overwritten by the specific model.

Member Data Documentation

◆ _ctx_

z3::context& ilang::MemoryModel::_ctx_
protected

A reference to Z3 context , even in the sence of const, it should allow us to allocate new variables

◆ _expr2z3_

Z3ExprAdapter ilang::MemoryModel::_expr2z3_
mutableprotected

An adapter that trace step can share, will allocate internally, by the constructor

◆ _ila_trace_steps

PerILATraceStepPtrSet ilang::MemoryModel::_ila_trace_steps
protected

The set of TraceStep set grouped by ILA (the same sequence as given to the register steps)


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