Z3 API

We describe APIs of Z3Mgr and its subclasses Z3ExampleMgr (used in Assignment-3) and Z3SSEMgr (used in Assignment-4).

Z3Mgr (Z3 Manager)

Members	Meanings
SVF:: Z3Mgr::storeValue(const z3::expr loc, const z3::expr value)	store value to the location loc of loc2ValMap, which is an Z3's array type for handling memory operations
SVF:: Z3Mgr::loadValue(const z3::expr loc)	retrieve the value from location loc of 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), otherwise assertion unsat
SVF:: Z3Mgr::getSolver	return the Z3's solver
SVF:: Z3Mgr::getCtx	return the Z3's context
SVF:: Z3Mgr::resetZ3ExprMap	reset added expressions and clean all declared values

Z3ExampleMgr (Assign-3)

Members	Meanings
SVF::Z3ExampleMgr::getZ3Expr(u32_t val)	return the Z3 expression based on the ID of an SVFVar
SVF::Z3ExampleMgr::getZ3Expr(std::string exprName)	return the Z3 expression based on the variable's name
getMemObjAddress(std::string exprName)	return the address expr of a ObjVar based on the variable's name
getGepObjAddress(z3::expr pointer, u32_t offset)	return the offset (u32_t) given a pointer type expression
addToSolver(z3::expr e)	add the expression to solver
resetSolver()	clean all constraints and reset the solver
printExprValues()	print the current point

Z3SSEMgr (Assign-4)

Members	Meanings
SVF:: Z3SSEMgr:: createExprForValVar(const ValVar* val)	declare the expr type for each top-level pointers
SVF:: Z3SSEMgr:: createExprForObjVar(const ObjVar* obj)	initialize the expr value for each objects (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 points 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 added expressions in the solver