#include <SymbolicExprGraphSolver.h>

Inheritance diagram for SymbolicExprGraphSolver:

[legend]

Collaboration diagram for SymbolicExprGraphSolver:

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

virtual SMTExprVec	getCtrlDeps (BasicBlock B, const SymbolicExprGraph G, void *Args=nullptr)
	Get the condition of paths reaching the block B.

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

virtual SMTExprVec	getDataDeps (const SEGNodeBase N, void Args=nullptr)
	Model node n's data dependence.

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

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 SMTExprVec	getDeps (const SEGNodeBase N, const SEGNodeBase M)

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

virtual void	push ()

virtual void	pop (unsigned N=1)

virtual void	reset ()

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)

Protected Attributes
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

Detailed Description

SEGSolver and its child classes have an assumption that the data deps of a SEGNode will not be obtained by all getDeps interfaces if it has been obtained before and has not been popped by pop().

This assumption may be not friendly, which should be redesigned or add more interfaces in the future.

Member Function Documentation

◆ encodeOpcodeNode()

SMTExpr SymbolicExprGraphSolver::encodeOpcodeNode ( const SEGOpcodeNode * N )

TODO The following features have not been/cannot be modeled:
1. casts involving fp, we do not consider precision lost.
2. AddrSpaceCast, currently, since it can be complex operation, we do nothing. It should be modeled as the source/target address space.
3. QNaN is not modeled, meaning nothing can be NaN.
4. floating point types in composite types are modeled as int.
E.g. {intN_t x=2, float y=1.2} is modeled as {intN_t x = 2, int' y = 1}, here sizeof(float) == sizeof(int')

Note that z3 only has real type which is not the same as float or double. If we use z3::real to model floating point type, we will frequently use Z3_mk_bv2int and Z3_mk_int2bv (because bv cannot cast to real directly). However, the functions are not reliable or not precise (uninterpreted) according to the documents.

◆ getCtrlDepsPair()

virtual std::pair<SMTExprVec, SMTExprVec> SymbolicExprGraphSolver::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 in DTSymbolicExprGraphSolver.

◆ getDeps()

SMTExprVec SymbolicExprGraphSolver::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 if M is in the same Block with N, N's Ctrl Dep will not be included in the return results.

Reimplemented in DTSymbolicExprGraphSolver.

◆ getDepsPair()

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

virtual

Same as SymbolicExprGraphSolver::getDeps(const SEGNodeBase*, const SEGNodeBase*), except that ctrl deps and data deps are split to two parts

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