Inheritance diagram for DTSymbolicExprGraphSolver:

Collaboration diagram for DTSymbolicExprGraphSolver:

Public Member Functions
	DTSymbolicExprGraphSolver (SMTFactory &Fcty, TSDataLayout &D, ExternalMemorySpec MemSpec, ExternalIOSpec IOSpec, const DomTree *T)

virtual SMTExprVec	getCtrlDeps (BasicBlock B, const SymbolicExprGraph G, void *Args=nullptr)

virtual std::pair< SMTExprVec, SMTExprVec >	getCtrlDepsPair (BasicBlock B, const SymbolicExprGraph G, void *Args=nullptr)

virtual SMTExprVec	getDataDeps (const SEGNodeBase N, void Args=nullptr)

virtual SMTExprVec	getPhiGated (const SEGPhiNode PhiNode, const SEGPhiNode::IncomeNode InNode, void Args=nullptr)

virtual void	reset ()

virtual SMTExprVec	getDeps (const SEGNodeBase N, const SEGNodeBase M)

Public Member Functions inherited from SymbolicExprGraphSolver
	SymbolicExprGraphSolver (SMTFactory &Fcty, TSDataLayout &D, ExternalMemorySpec MemSepc, ExternalIOSpec IOSpec)

SMTExprVec	getCtrlDeps (const SEGNodeBase N, void Args=nullptr)
	Get the condition of paths reaching node n.

SMTExprVec	getPhiGated (const SEGPhiNode PhiNode, const SEGNodeBase Value, BasicBlock BB, void Args=nullptr)

SMTExprVec	getPhiGated (const SEGPhiNode PhiNode, const SEGNodeBase Value, void *Args=nullptr)

virtual std::pair< SMTExprVec, SMTExprVec >	getDepsPair (const SEGNodeBase N, const SEGNodeBase M)

virtual void	push ()

virtual void	pop (unsigned N=1)

virtual SMTResultType	check ()

const std::unordered_set< const SEGArgumentNode * > &	getUsedFunctionArguments ()

std::pair< std::vector< const SEGCallSiteOutputNode * >::iterator, std::vector< const SEGCallSiteOutputNode * >::iterator >	getUsedCallSiteOutputs (bool Restart=false)

const SEGNodeBase *	getNodeFromSymbol (std::string Symbol)
	return the SEG node for the given symbol

SMTExpr	getOrInsertExpr (const SEGNodeBase *N)

SMTExpr	encodeOpcodeNode (const SEGOpcodeNode *N)

virtual SMTExpr	encodeBinaryOpcodeNode (const SEGOpcodeNode *N)

virtual SMTExpr	encodeCompareOpcodeNode (const SEGOpcodeNode *N)

virtual SMTExpr	encodeCastOpcodeNode (const SEGOpcodeNode *N)

virtual SMTExpr	encodeGEPOpcodeNode (const SEGOpcodeNode *N)

virtual SMTExpr	encodeExtractElementOpcodeNode (const SEGOpcodeNode *N)

virtual SMTExpr	encodeInsertElementOpcodeNode (const SEGOpcodeNode *N)

virtual SMTExpr	encodeSelectOpcodeNode (const SEGOpcodeNode *N)

virtual SMTExpr	encodeConcatOpcodeNode (const SEGOpcodeNode *N)

Additional Inherited Members
Protected Attributes inherited from SymbolicExprGraphSolver
std::unordered_map< const SEGNodeBase *, SMTExpr >	NodeExprMap
	each node in seg is a z3 variable

std::unordered_map< std::string, const SEGNodeBase * >	NodeSymbolNameMap
	map the symbol name used by Z3 in context ctx to the SEG node

TSDataLayout &	DL

ExternalMemorySpec *	MemSpec = nullptr

ExternalIOSpec *	IOSpec = nullptr

PushPopCache< const SEGNodeBase * >	ConstraintCache

PushPopCache< BasicBlock * >	BBCache

Member Function Documentation

◆ getCtrlDeps()

SMTExprVec DTSymbolicExprGraphSolver::getCtrlDeps	(	BasicBlock *	B,
		const SymbolicExprGraph *	G,
		void *	Args = `nullptr`
	)

virtual

Get the condition of paths reaching the block B In this solver, the args should be a basic block

Reimplemented from SymbolicExprGraphSolver.

◆ getCtrlDepsPair()

virtual std::pair<SMTExprVec, SMTExprVec> DTSymbolicExprGraphSolver::getCtrlDepsPair	(	BasicBlock *	B,
		const SymbolicExprGraph *	G,
		void *	Args = `nullptr`
	)

inlinevirtual

Get the condition of paths reaching the block B. CtrlDeps and DataDeps are split in the return value as a pair <CtrlDeps, DataDeps>. For example, if the ctrl dep is a AND b, then the data dep is a=... AND b=...

Reimplemented from SymbolicExprGraphSolver.

◆ getDataDeps()

SMTExprVec DTSymbolicExprGraphSolver::getDataDeps	(	const SEGNodeBase *	N,
		void *	Args = `nullptr`
	)

virtual

Model node n's data dependence In this solver, the args should be a basic block

Reimplemented from SymbolicExprGraphSolver.

◆ getDeps()

SMTExprVec DTSymbolicExprGraphSolver::getDeps	(	const SEGNodeBase *	N,
		const SEGNodeBase *	M
	)

virtual

Get the condition of paths reaching the assignment N = M If M is nullptr, it returns the data & ctrl deps of N. Note that M must be a child of N, and path conditions for PrevB will not be returned.

Reimplemented from SymbolicExprGraphSolver.

◆ getPhiGated()

SMTExprVec DTSymbolicExprGraphSolver::getPhiGated	(	const SEGPhiNode *	PhiNode,
		const SEGPhiNode::IncomeNode	InNode,
		void *	Args = `nullptr`
	)

virtual

Return gated function for a child of a phiNode This is the most accurate for a phi incoming node, since it is identified with incoming BB and the value. In this solver, the args should be a basic block

Reimplemented from SymbolicExprGraphSolver.

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

/builds/prismers/clearblue/include/IR/SEG/SymbolicExprGraphSolver.h
/builds/prismers/clearblue/lib/IR/SEG/SymbolicExprGraphSolver.cpp

Public Member Functions

Additional Inherited Members

Member Function Documentation

◆ getCtrlDeps()

◆ getCtrlDepsPair()

◆ getDataDeps()

◆ getDeps()

◆ getPhiGated()