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 < InstrLvlAbsPtr >	IlaPtrVec
	Type of vector of pointers to the ILAs involved.
typedef std::list< ExprPtr >	StateVarList
	Type of list of state variables.
typedef std::map< std::string, StateVarList >	SharedStatesSet
	Type of map of shared states (set of names -> list of exprs)
typedef std::unique_ptr < MemoryModel >	MemoryModelPtr
typedef std::function < MemoryModelPtr(z3::context &, ZExprVec &, const StateNameSet &, const ILANameStateNameSetMap &, const InstrLvlAbsPtr &)>	MemoryModelCreator
typedef std::shared_ptr < TraceStep >	TraceStepPtr
	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 ZExprVec &	DebugAccessConstrList () const
	Get access to expr vector, will only be usable if unroller is not destroyed, only for DEBUG use.
const TraceStepPtrSet &	DebugAccessAllTraceStepPtrSet () 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

typedef std::function<MemoryModelPtr( z3::context&, ZExprVec&, const StateNameSet&, const ILANameStateNameSetMap&, const InstrLvlAbsPtr& )> ilang::InterIlaUnroller::MemoryModelCreator

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

typedef std::unique_ptr<MemoryModel> ilang::InterIlaUnroller::MemoryModelPtr

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

using ilang::InterIlaUnroller::ProgramTemplate = MemoryModel::ProgramTemplate

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

Member Function Documentation

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

Add a property.

Parameters

[in]	a	property that is going to translated to Z3, note: the state are treated as prestate
[in]	a	filter to choose which trace step to enforce

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]	a	property that is going to translated to Z3, note: the state are treated as prestate
[in]	a	filter to choose which trace step to enforce
[in]	a	collector (callback function) to do something as each time a property is created on a step

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

virtual

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

Parameters

[in]

whether

each template should be treated as ordered or unordered

void ilang::InterIlaUnroller::SetFinalProperty

(

const ExprPtr &

property

)

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

Parameters

[in]

the

property

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

virtual

[Application-specific] Unroll, currently just use PathUnroller

Parameters

[in]

the

program template.

---

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

• inter_ila_unroller.h