SVF Z3 API - SVF-tools/Software-Security-Analysis GitHub Wiki
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, 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* |