Z3 API

Z3 API for Assignment 4

Assignment 4 uses Z3Mgr, Z3SSEMgr, and the convenience methods exposed by SSE.

Z3Mgr

Members	Meanings
SVF::Z3Mgr::storeValue(const z3::expr loc, const z3::expr value)	Store value at the abstract address loc in the Z3 memory array.
SVF::Z3Mgr::loadValue(const z3::expr loc)	Load the value at abstract address loc.
SVF::Z3Mgr::getEvalExpr(z3::expr expr)	Evaluate an expression using a satisfying model for the current constraints.
SVF::Z3Mgr::getSolver()	Return the Z3 solver. Use check() to test satisfiability.
SVF::Z3Mgr::getCtx()	Return the Z3 context used to construct constants and expressions.
SVF::Z3Mgr::checkNegateAssert(z3::expr expr)	Return true when the negation of expr is unsatisfiable, meaning no counterexample exists.
z3::solver::push() / z3::solver::pop()	Save and restore a solver scope when temporarily adding constraints.

Z3SSEMgr and SSE

Members	Meanings
SVF::SSE::getZ3Expr(NodeID varId)	Return the Z3 expression for an SVF variable in the current callingCtx.
SVF::SSE::getMemObjAddress(NodeID objId)	Return the abstract address of an ObjVar.
SVF::Z3SSEMgr::getGepObjAddress(z3::expr pointer, u32_t offset)	Return the abstract address of a field or array element.
SVF::Z3SSEMgr::getGepOffset(const GepStmt* gep, const CallStack& callingCtx)	Compute the flattened offset represented by a GepStmt.
SVF::SSE::addToSolver(z3::expr expr)	Add a constraint to the current solver.
SVF::SSE::resetSolver()	Clear solver constraints and the path-translation calling context.
SVF::SSE::pushCallingCtx(const ICFGNode* callNode) / SVF::SSE::popCallingCtx()	Enter or leave a call context while translating a path.
SVF::SSE::getEvalExpr(z3::expr expr)	Evaluate an expression in a satisfying model.
SVF::SSE::printExprValues()	Print the evaluated SVF variables and abstract memory objects.

callstack is used while traversing the ICFG. callingCtx is a separate stack used while translating the collected path into context-sensitive Z3 expressions.

Use getCtx().int_val(n) for an integer literal such as 0 or 1. getZ3Expr(n) treats n as an SVF variable ID, not as a literal value.

Common Z3 expressions

Expression	Meaning
lhs == rhs, lhs != rhs	Equality and inequality constraints.
lhs < rhs, lhs <= rhs, lhs > rhs, lhs >= rhs	Integer ordering constraints.
cond && other, `cond
z3::ite(cond, trueExpr, falseExpr)	If-then-else expression.
z3::solver::check() == z3::unsat	The current path constraints have no solution.
z3::solver::get_model()	A model, and therefore a potential counterexample, for satisfiable constraints.