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

Base class for unrolling multiple ILAs. There are two ways of unrolling: ordered and unordered. Ordered unrolling assumes an ordered program template, despite that some may not exist in the final outcome. By default the state with the same name among ILAs is considered as the same shared state. More...

#include <inter_ila_unroller.h>

Public Types

using ZExpr = MemoryModel::ZExpr
 Type alias for z3::expr.
 
using ZExprVec = MemoryModel::ZExprVec
 Type for containing a vector of z3::expr.
 
using StateNameSet = MemoryModel::StateNameSet
 Type of state name set.
 
using InstrVec = MemoryModel::InstrVec
 Type of an instruction vector to represent a sequence.
 
using ProgramTemplate = MemoryModel::ProgramTemplate
 
using ILANameStateNameSetMap = MemoryModel::ILANameStateNameSetMap
 Type of map ila-name to state-set.
 
using TraceStepPtrSet = MemoryModel::TraceStepPtrSet
 Type of set of trace step pointers (DEBUG use)
 
typedef std::vector< InstrLvlAbsPtrIlaPtrVec
 Type of vector of pointers to the ILAs involved.
 
typedef std::list< ExprPtrStateVarList
 Type of list of state variables.
 
typedef std::map< std::string, StateVarListSharedStatesSet
 Type of map of shared states (set of names -> list of exprs)
 
typedef std::unique_ptr< MemoryModelMemoryModelPtr
 
typedef std::function< MemoryModelPtr(z3::context &, ZExprVec &, const StateNameSet &, const ILANameStateNameSetMap &, const InstrLvlAbsPtr &)> MemoryModelCreator
 
typedef std::shared_ptr< TraceStepTraceStepPtr
 Type of trace step pointer.
 

Public Member Functions

 InterIlaUnroller (z3::context &ctx, const IlaPtrVec &iv, MemoryModelCreator mm_selector)
 Default constructor. mm_selector is used to create mm internally.
 
virtual ~InterIlaUnroller ()
 Default destructor.
 
void GenSysInitConstraints ()
 it generates the initial constraints and put them on to the constraint list and check should be called before unroll
 
virtual void Unroll (const ProgramTemplate &tmpl)
 [Application-specific] Unroll, currently just use PathUnroller More...
 
virtual void LinkStates (const std::vector< bool > &ordered)
 [Application-specific] Link states, where each trace step read from More...
 
void AddSingleTraceStepProperty (const ExprPtr &property, std::function< bool(const TraceStep &)> filter)
 Add a property. More...
 
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, so you can play with it. More...
 
void SetFinalProperty (const ExprPtr &property)
 Set final property (you should only call this function only ONCE) More...
 
bool CheckSat ()
 Check and potentially set the model: return true if sat , false o.w.
 
z3::model & GetModel ()
 Get the model: the reference will only be usable if unroller is not destroyed.
 
const ZExprVecDebugAccessConstrList () const
 Get access to expr vector, will only be usable if unroller is not destroyed, only for DEBUG use.
 
const TraceStepPtrSetDebugAccessAllTraceStepPtrSet () const
 Get access to expr vector, will only be usable if unroller is not destroyed, only for DEBUG use.
 
void Push ()
 Push the size of current set of constraints.
 
void Pop ()
 Restore the previous set of constraints.
 

Protected Member Functions

void FindSharedStates ()
 It create a name list. There is no need to create an ExprPtr list because their hosts are different and will generate different z3exprs.
 
bool CurrConstrSat ()
 Sanity check if the current constraints are satisfiable.
 
ZExpr ConjPred (const ZExprVec &vec) const
 Conjunct (AND) all the predicates in the set.
 

Protected Attributes

IlaPtrVec sys_ila_
 The ILAs of an SoC.
 
InstrLvlAbsPtr global_ila_
 The ILA of the system.
 
StateNameSet shared_states_
 Set of names of shared states.
 
ILANameStateNameSetMap private_states_
 Map from ila-name to set-of-state-names.
 
ZExprVec cstr_
 The set of constraints that should be asserted.
 
ZExprVec init_shared_vars_z3_
 The set of constraints that should be asserted.
 

Friends

class MemoryModel
 

Detailed Description

Base class for unrolling multiple ILAs. There are two ways of unrolling: ordered and unordered. Ordered unrolling assumes an ordered program template, despite that some may not exist in the final outcome. By default the state with the same name among ILAs is considered as the same shared state.

Member Typedef Documentation

◆ MemoryModelCreator

Type of memory model creator, nees to be the same as the ctor of MemoryModelClass

◆ MemoryModelPtr

Type of memory model pointer, we enforce ownership strictly, so it cannot be used else where

◆ ProgramTemplate

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

Member Function Documentation

◆ AddSingleTraceStepProperty()

void ilang::InterIlaUnroller::AddSingleTraceStepProperty ( const ExprPtr property,
std::function< bool(const TraceStep &)>  filter 
)

Add a property.

Parameters
[in]aproperty that is going to translated to Z3, note: the state are treated as prestate
[in]afilter to choose which trace step to enforce

◆ GetSingleTraceStepProperty()

void ilang::InterIlaUnroller::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, so you can play with it.

Parameters
[in]aproperty that is going to translated to Z3, note: the state are treated as prestate
[in]afilter to choose which trace step to enforce
[in]acollector (callback function) to do something as each time a property is created on a step

◆ LinkStates()

virtual void ilang::InterIlaUnroller::LinkStates ( const std::vector< bool > &  ordered)
virtual

[Application-specific] Link states, where each trace step read from

Parameters
[in]whethereach template should be treated as ordered or unordered

◆ SetFinalProperty()

void ilang::InterIlaUnroller::SetFinalProperty ( const ExprPtr property)

Set final property (you should only call this function only ONCE)

Parameters
[in]theproperty

◆ Unroll()

virtual void ilang::InterIlaUnroller::Unroll ( const ProgramTemplate tmpl)
virtual

[Application-specific] Unroll, currently just use PathUnroller

Parameters
[in]theprogram template.

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