SVF Z3 API

We describe the API of Z3Mgr and its subclasses Z3ExampleMgr (used in Lab-Exercise-2) and Z3SSEMgr (used in Assignment-2).

Z3Mgr (Z3 Manager)

Members	Meanings
SVF:: Z3Mgr::storeValue(const z3::expr loc, const z3::expr value)	store value to the location loc in loc2ValMap (which is a Z3 array for handling memory operations)
SVF:: Z3Mgr::loadValue(const z3::expr loc)	retrieve the value at location loc in loc2ValMap
SVF:: Z3Mgr::getZ3Expr(u32_t idx)	return the Z3 expression based on the ID of an SVFVar
SVF:: Z3Mgr::updateZ3Expr(u32_t idx, z3::expr target)	update expression for an SVFVar given its ID
SVF:: Z3Mgr::getEvalExpr(z3::expr e)	return evaluated value of an expression if the expression has a solution (model); asserts unsat otherwise
SVF:: Z3Mgr::getSolver	return the Z3 solver
SVF:: Z3Mgr::getCtx	return the Z3 context
SVF:: Z3Mgr::resetZ3ExprMap	reset added expressions and clean all declared values
solver.push()	creates a new scope by saving the current stack
solver.pop()	pop removes any expressions performed between it and the matching push

Z3ExampleMgr (Lab-Exercise-2)

Members	Meanings
SVF::Z3ExampleMgr::getZ3Expr(u32_t val)	return the Z3 expression given a constant integer value (e.g., getZ3Expr(5) returns the expression 5)
SVF::Z3ExampleMgr::getZ3Expr(std::string exprName)	return the Z3 expression based on a variable's name
SVF::Z3ExampleMgr::getMemObjAddress(std::string exprName)	return the virtual memory address based on an object's name
SVF::Z3ExampleMgr::getGepObjAddress(z3::expr pointer, u32_t offset)	return the virtual memory address of a field given a base pointer and offset
SVF::Z3ExampleMgr::addToSolver(z3::expr e)	add a Z3 expression into the solver
SVF::Z3ExampleMgr::resetSolver()	reset added expressions and clean all declared values
SVF::Z3ExampleMgr::printExprValues()	print the values of all Z3 expressions

Z3SSEMgr (Assignment-2)

Members	Meanings
SVF:: Z3SSEMgr:: createExprForObjVar(const ObjVar* obj)	initialize the expr value for an object (address-taken variables and constants)
SVF:: Z3SSEMgr::getMemObjAddress(u32_t idx)	return the address expr of a ObjVar
SVF:: Z3SSEMgr::getGepObjAddress(z3::expr pointer, u32_t offset)	return the field address given a pointer pointing to a struct object and an offset
SVF:: Z3SSEMgr::getGepOffset(const GepStmt* gep)	return the offset (u32_t) given a GepStmt
SVF:: Z3SSEMgr:: printExprValues	dump the values of all expressions added to the solver
SVF::Z3SSEMgr::callingCtxToStr	return the calling context in the form of string.
SVF::Z3SSEMgr::getZ3Expr(u32_t idx, const CallStack& callingCtx)	return the z3 expression given an SVFVarID and a calling context
SVF::SSE::getZ3Expr(u32_t idx)	return the z3 expression given an SVFVarID and the current calling context callingCtx
SVF::SSE::getCtx().int_val(0)	return the z3 expression for int literal 0 (don't use getZ3Expr(0) in Assignment-2)
SVF::SSE::getEvalExpr(z3::expr e)	checks if the constraints added to the Z3 solver are satisfiable. If so, evaluates e within this model, returning the evaluated result like bool, int, real and string
SVF::Z3Mgr::printZ3Exprs()	print all z3 expressions in the solver without solving or evaluation
SVFIR::getValueNode(SVF::Value*)	get the VarID given an SVF Value*