SVF Z3 API

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

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

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, const CallStack& callingCtx)	return the offset (`u32_t`) given a GepStmt and the current calling context
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(u32_t int_literal)	return the z3 expression for int literal (e.g., 0 and 1). DO NOT use getZ3Expr(0) or getZ3Expr(1) for int constants 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*