ilang::MonoUnroll Class Reference

Application class for unrolling the ILA as a monolithic transition system. More...

#include <u_unroller.h>

Inheritance diagram for ilang::MonoUnroll:

Public Member Functions
	MonoUnroll (z3::context &ctx, const std::string &suff="")
	Default constructor.
	~MonoUnroll ()
	Default destructor.
ZExpr	MonoSubs (const InstrLvlAbsPtr &top, const int &length, const int &pos=0)
	Unroll the ILA with internal states substituted. More...
ZExpr	MonoAssn (const InstrLvlAbsPtr &top, const int &length, const int &pos=0)
	Unroll the ILA while asserting states are equal between each step. More...
ZExpr	MonoNone (const InstrLvlAbsPtr &top, const int &length, const int &pos=0)
	Unroll the ILA without asserting states relations between steps. More...
ZExpr	MonoIncr (const InstrLvlAbsPtr &top, const int &length, const int &pos)
	Incrementally unrolling the ILA using MonoAssn (with transition relation being cached). More...
Public Member Functions inherited from ilang::Unroller
	Unroller (z3::context &ctx, const std::string &suffix)
	Default constructor.
virtual	~Unroller ()
	Default virtual destructor.
void	AddGlobPred (const ExprPtr &p)
	Add a predicate that should be asserted globally.
void	AddInitPred (const ExprPtr &p)
	Add a predicate that should be asserted in the initial condition.
void	AddStepPred (const ExprPtr &p, const int &k)
	Add a predicate that should be asserted at the k-th step.
void	ClearGlobPred ()
	Clear the global predicates.
void	ClearInitPred ()
	Clear the initial predicates.
void	ClearStepPred ()
	Clear the step-specific predicates.
void	ClearPred ()
	Clear all predicates.
ZExpr	CurrState (const ExprPtr &v, const int &t)
	Return the z3::expr representing the current state at the time.
ZExpr	NextState (const ExprPtr &v, const int &t)
	Return the z3::expr representing the next state at the time.
ZExpr	GetZ3Expr (const ExprPtr &e, const int &t)
	Return the z3::expr representing the current-based Expr at the time.
ZExpr	GetZ3Expr (const ExprPtr &e)
	Return the z3::expr representing a unique Expr (regardless of time).
ZExpr	Equal (const ExprPtr &va, const int &ta, const ExprPtr &vb, const int &tb)
	Return the z3::expr representing a and b are equal at their time.
z3::func_decl	GetZ3FuncDecl (const FuncPtr &f) const
	Return the z3::func_decl representing f.

Protected Member Functions
void	DefineDepVar ()
	[Application-specific] Define dependant state variables. More...
void	Transition (const int &idx)
	[Application-specific] Define next state update functions. More...
Protected Member Functions inherited from ilang::Unroller
ZExpr	UnrollSubs (const size_t &len, const int &pos)
	Unroll while substituting internal expression.
ZExpr	UnrollAssn (const size_t &len, const int &pos, bool cache=false)
	Unroll without substituting internal expression.
ZExpr	UnrollNone (const size_t &len, const int &pos)
	Unroll without asserting state equality between each step.

Additional Inherited Members
Protected Types inherited from ilang::Unroller
typedef z3::expr	ZExpr
	Type alias for z3::expr.
typedef z3::expr_vector	ZExprVec
	Type for containing a set of z3::expr.
typedef ExprPtrVec	IExprVec
	Type alias for a set of ExprPtr.
Static Protected Member Functions inherited from ilang::Unroller
static ExprPtr	StateUpdCmpl (const InstrPtr &instr, const ExprPtr &var)
	Return the state update function (unchanged if not defined).
static ExprPtr	DecodeCmpl (const InstrPtr &instr)
	Return the decode function (true if not defined).
static ExprPtr	NewFreeVar (const ExprPtr &var, const std::string &name)
	Create a new free variable (with same sort) under the same host.
Protected Attributes inherited from ilang::Unroller
IExprVec	vars_
	The set of dependant state variables.
IExprVec	k_pred_
	The set of predicates to be asserted of each step.
IExprVec	k_next_
	The set of state update functions of each step.

Detailed Description

Application class for unrolling the ILA as a monolithic transition system.

Member Function Documentation

void ilang::MonoUnroll::DefineDepVar ( )

protectedvirtual

[Application-specific] Define dependant state variables.

• "vars_" should be assigned with the state vars uniquely.
• "vars_" will be cleared before caling this function.
• The var order stored in "vars_" will be the globally agree-upon order.

Implements ilang::Unroller.

ZExpr ilang::MonoUnroll::MonoAssn	(	const InstrLvlAbsPtr &	top,
		const int &	length,
		const int &	pos = 0
	)

Unroll the ILA while asserting states are equal between each step.

Parameters

[in]	top	the top-level ILA.
[in]	length	number of steps to unroll.
[in]	pos	the starting time frame.

ZExpr ilang::MonoUnroll::MonoIncr	(	const InstrLvlAbsPtr &	top,
		const int &	length,
		const int &	pos
	)

Incrementally unrolling the ILA using MonoAssn (with transition relation being cached).

Parameters

[in]	top	the top-level ILA.
[in]	length	number of steps to unroll.
[in]	pos	the starting time frame.

ZExpr ilang::MonoUnroll::MonoNone	(	const InstrLvlAbsPtr &	top,
		const int &	length,
		const int &	pos = 0
	)

Unroll the ILA without asserting states relations between steps.

Parameters

[in]	top	the top-level ILA.
[in]	length	number of steps to unroll.
[in]	pos	the starting time frame.

ZExpr ilang::MonoUnroll::MonoSubs	(	const InstrLvlAbsPtr &	top,
		const int &	length,
		const int &	pos = 0
	)

Unroll the ILA with internal states substituted.

Parameters

[in]	top	the top-level ILA.
[in]	length	number of steps to unroll.
[in]	pos	the starting time frame.

void ilang::MonoUnroll::Transition ( const int &  idx )

protectedvirtual

[Application-specific] Define next state update functions.

• "k_next_" should be assigned with the next state expression.
• "k_next_" follows the global order as stored in "vars_".
• "k_next_" will NOT be cleared before calling (is the only modifier).
• "k_pred_" can be used to store step-specific predicates, e.g. decode.
• "k_pred_" will NOT be cleared before calling (is the only modifier).

Implements ilang::Unroller.

---

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

• u_unroller.h