ilang::Unroller Class Reference

Base class for unrolling ILA execution in different settings. More...

#include <u_unroller.h>

Inheritance diagram for ilang::Unroller:

Public Member Functions
	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 Types
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.

Protected Member Functions
virtual void	DefineDepVar ()=0
	[Application-specific] Define dependant state variables. More...
virtual void	Transition (const int &idx)=0
	[Application-specific] Define next state update functions. More...
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.

Static Protected Member Functions
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
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

Base class for unrolling ILA execution in different settings.

Member Function Documentation

virtual void ilang::Unroller::DefineDepVar ( )

protectedpure virtual

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

Implemented in ilang::MonoUnroll, and ilang::PathUnroll.

virtual void ilang::Unroller::Transition ( const int &  idx )

protectedpure virtual

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

Implemented in ilang::MonoUnroll, and ilang::PathUnroll.

---

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

• u_unroller.h