Z3 API - SVF-tools/Teaching-Software-Verification GitHub Wiki
We describe the API 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 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 (Assign-3)
| 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 (Assign-4)
| Members | Meanings |
|---|---|
| SVF:: Z3SSEMgr:: createExprForValVar(const ValVar* val) | initialize the expr value for a top-level pointer |
| 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 |
| SVFIR::getValueNode(SVF::Value*) | get the VarID given an SVF Value* |