ilang::PathUnroll Class Reference

Application class for unrolling a path of instruction sequence. More...

#include <u_unroller.h>

Inheritance diagram for ilang::PathUnroll:

Public Types
typedef std::vector< InstrPtr >	InstrVec
	Type of a list of instruction sequence.

Public Member Functions
	PathUnroll (z3::context &ctx, const std::string &suff="")
	Default constructor.
	~PathUnroll ()
	Default destructor.
ZExpr	PathSubs (const std::vector< InstrPtr > &seq, const int &pos=0)
	Unroll a sequence of instructions with internal states substituted. More...
ZExpr	PathAssn (const std::vector< InstrPtr > &seq, const int &pos=0)
	Unroll a sequence of instructions while asserting states are equal between each step. More...
ZExpr	PathNone (const std::vector< InstrPtr > &seq, const int &pos=0)
	Unroll a sequence of instructions without asserting states relations between steps. "N(var_i) == var_i.nxt_suff". 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 a path of instruction sequence.

Member Function Documentation

void ilang::PathUnroll::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::PathUnroll::PathAssn	(	const std::vector< InstrPtr > &	seq,
		const int &	pos = 0
	)

Unroll a sequence of instructions while asserting states are equal between each step.

Parameters

[in]	seq	the sequence of instructions.
[in]	pos	the starting time frame.

ZExpr ilang::PathUnroll::PathNone	(	const std::vector< InstrPtr > &	seq,
		const int &	pos = 0
	)

Unroll a sequence of instructions without asserting states relations between steps. "N(var_i) == var_i.nxt_suff".

Parameters

[in]	seq	the sequence of instructions.
[in]	pos	the starting time frame.

ZExpr ilang::PathUnroll::PathSubs	(	const std::vector< InstrPtr > &	seq,
		const int &	pos = 0
	)

Unroll a sequence of instructions with internal states substituted.

Parameters

[in]	seq	the sequence of instructions.
[in]	pos	the starting time frame.

void ilang::PathUnroll::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