From 428a14eb79857ae9c27a408a0a2629f4816596eb Mon Sep 17 00:00:00 2001 From: JoelYYoung <56264140+JoelYYoung@users.noreply.github.com> Date: Wed, 16 Sep 2026 05:17:34 +0000 Subject: [PATCH] Add manual Z3 lab --- CMakeLists.txt | 1 + Lab-Z3/CMakeLists.txt | 19 +++ Lab-Z3/Z3Examples.cpp | 352 ++++++++++++++++++++++++++++++++++++++++++ Lab-Z3/Z3Examples.h | 153 ++++++++++++++++++ Lab-Z3/Z3Mgr.cpp | 93 +++++++++++ Lab-Z3/Z3Mgr.h | 157 +++++++++++++++++++ Lab-Z3/test.cpp | 122 +++++++++++++++ 7 files changed, 897 insertions(+) create mode 100644 Lab-Z3/CMakeLists.txt create mode 100644 Lab-Z3/Z3Examples.cpp create mode 100644 Lab-Z3/Z3Examples.h create mode 100644 Lab-Z3/Z3Mgr.cpp create mode 100644 Lab-Z3/Z3Mgr.h create mode 100644 Lab-Z3/test.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 3e6534d..1671fd5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -169,4 +169,5 @@ add_subdirectory(CodeGraph) add_subdirectory(Assignment-1) add_subdirectory(Assignment-2) add_subdirectory(Assignment-3) +add_subdirectory(Lab-Z3) add_subdirectory(Assignment-4) diff --git a/Lab-Z3/CMakeLists.txt b/Lab-Z3/CMakeLists.txt new file mode 100644 index 0000000..35e899d --- /dev/null +++ b/Lab-Z3/CMakeLists.txt @@ -0,0 +1,19 @@ +set(SOURCES + Z3Examples.cpp + Z3Mgr.cpp + test.cpp +) + +add_executable(lab-z3 ${SOURCES}) +target_link_libraries(lab-z3 ${SVF_LIB} ${llvm_libs} ${Z3_LIBRARIES}) + +set_target_properties(lab-z3 PROPERTIES + RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) + +foreach(i RANGE 0 10) + add_test( + NAME lab-z3-test${i} + COMMAND lab-z3 test${i} + WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/bin + ) +endforeach() diff --git a/Lab-Z3/Z3Examples.cpp b/Lab-Z3/Z3Examples.cpp new file mode 100644 index 0000000..09c46d2 --- /dev/null +++ b/Lab-Z3/Z3Examples.cpp @@ -0,0 +1,352 @@ +//===- Z3Examples.cpp -- Manual assertion-based verification ------------===// +// +// SVF: Static Value-Flow Analysis +// +// Copyright (C) <2013-2022> +// + +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. + +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. + +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . +// +//===----------------------------------------------------------------------===// +/* + * Manual assertion-based verification with Z3 + * + * Created on: Feb 19, 2024 + */ + +#include "Z3Examples.h" + +using namespace SVF; +using namespace z3; + +/* +int main() { + int* p; + int q; + int* r; + int x; + + p = malloc(); + q = 5; + *p = q; + x = *p; + assert(x == 5); +} +*/ +void Z3Examples::test0() { + // int* p; + expr p = getZ3Expr("p"); + + // int q; + expr q = getZ3Expr("q"); + + // int* r; + expr r = getZ3Expr("r"); + + // int x; + expr x = getZ3Expr("x"); + + // p = malloc(); + addToSolver(p == getMemObjAddress("malloc")); + + // q = 5; + addToSolver(q == 5); + + // *p = q; + storeValue(p, q); + + // x = *p; + addToSolver(x == loadValue(p)); +} + +/* +int main() { + int a; + int b; + a = 0; + b = a + 1; + assert(b > 0); +} +*/ +void Z3Examples::test1() { + // int a; + expr a = getZ3Expr("a"); + // int b; + expr b = getZ3Expr("b"); + /// TODO: Write the Z3 expressions for the program above +} + +/* +int main() { + int* p; + int q; + int b; + p = malloc(); + *p = 0; + q = *p; + *p = 3; + b = *p + 1; + assert(b > 3); +} +*/ +void Z3Examples::test2() { + // int* p; + expr p = getZ3Expr("p"); + // int q; + expr q = getZ3Expr("q"); + // int b; + expr b = getZ3Expr("b"); + /// TODO: Write the Z3 expressions for the program above +} + +/* +int main() { + int** p; + int* q; + int* r; + int x; + + p = malloc1(); + q = malloc2(); + *p = q; + *q = 10; + r = *p; + x = *r; + assert(x == 10); +} +*/ +void Z3Examples::test3() { + // int** p; + expr p = getZ3Expr("p"); + + // int* q; + expr q = getZ3Expr("q"); + + // int* r; + expr r = getZ3Expr("r"); + + // int x; + expr x = getZ3Expr("x"); + + /// TODO: Write the Z3 expressions for the program above +} + +/* +int main() { + int* p; + int* x; + int* y; + int a; + int b; + p = malloc(); + x = &p[0]; + y = &p[1]; + *x = 10; + *y = 11; + a = *x; + b = *y; + assert((a + b) > 20); +} +*/ +void Z3Examples::test4() { + // int* p; + expr p = getZ3Expr("p"); + + // int* x; + expr x = getZ3Expr("x"); + + // int* y; + expr y = getZ3Expr("y"); + + // int a; + expr a = getZ3Expr("a"); + + // int b; + expr b = getZ3Expr("b"); + + /// TODO: Write the Z3 expressions for the program above +} + +/* +int main(int argv) { + int a; + int b; + int b1; + a = argv + 1; + b = 5; + if (a > 10) + b = a; + b1 = b; + assert(b1 >= 5); +} +*/ +void Z3Examples::test5() { + // int argv; + expr argv = getZ3Expr("argv"); + + // int a; + expr a = getZ3Expr("a"); + + // int b; + expr b = getZ3Expr("b"); + + // int b1; + expr b1 = getZ3Expr("b1"); + + /// TODO: Write the Z3 expressions for the program above +} + +/* +int main() { + int* a = malloc1(); + int* b = malloc2(); + *a = 5; + *b = 10; + int* p; + if (*a < *b) + p = a; + else + p = b; + assert(*p == 5); +} +*/ +void Z3Examples::test6() { + // int* a; + expr a = getZ3Expr("a"); + // int* b; + expr b = getZ3Expr("b"); + + /// TODO: Write the Z3 expressions for the program above +} + +/* +int main() { + int a = 1, b = 2, c = 3; + int d; + if (a > 0) + d = b + c; + else + d = b - c; + assert(d == 5); +} +*/ +void Z3Examples::test7() { + // int a = 1, b = 2, c = 3; + expr a = getZ3Expr("a"); + expr b = getZ3Expr("b"); + expr c = getZ3Expr("c"); + // int d; + expr d = getZ3Expr("d"); + + /// TODO: Write the Z3 expressions for the program above +} + +/* +int main() { + int arr[2] = {0, 1}; + int a = 10; + int* p; + if (a > 5) + p = &arr[0]; + else + p = &arr[1]; + assert(*p == 0); +} +*/ +void Z3Examples::test8() { + // int arr[2]; + expr arr = getZ3Expr("arr"); + // int* p; + expr p = getZ3Expr("p"); + + /// TODO: Write the Z3 expressions for the program above +} + +/* +struct A { + int f0; + int* f1; +}; + +int main() { + struct A* p; + int* x; + int* q; + int** r; + int* y; + int z; + + p = malloc1(); + x = malloc2(); + *x = 5; + q = &(p->f0); + *q = 10; + r = &(p->f1); + *r = x; + y = *r; + z = *q + *y; + assert(z == 15); +} +*/ +void Z3Examples::test9() { + // struct A* p; + expr p = getZ3Expr("p"); + + // int* x; + expr x = getZ3Expr("x"); + + // int* q; + expr q = getZ3Expr("q"); + + // int** r; + expr r = getZ3Expr("r"); + + // int* y; + expr y = getZ3Expr("y"); + + // int z; + expr z = getZ3Expr("z"); + + /// TODO: Write the Z3 expressions for the program above +} + +/* +int foo(int z) { + int k = z; + return k; +} + +int main() { + int x; + int y; + y = foo(2); + x = foo(3); + assert(x == 3 && y == 2); +} +*/ +void Z3Examples::test10() { + // int x; + expr x = getZ3Expr("x"); + + // int y; + expr y = getZ3Expr("y"); + + // int z; + expr z = getZ3Expr("z"); + + // int k; + expr k = getZ3Expr("k"); + + /// TODO: Write the Z3 expressions for the program above +} diff --git a/Lab-Z3/Z3Examples.h b/Lab-Z3/Z3Examples.h new file mode 100644 index 0000000..053400d --- /dev/null +++ b/Lab-Z3/Z3Examples.h @@ -0,0 +1,153 @@ +//===- Z3Examples.h -- Manual assertion-based verification --------------===// +// +// SVF: Static Value-Flow Analysis +// +// Copyright (C) <2013-2022> +// + +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. + +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. + +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . +// +//===----------------------------------------------------------------------===// +/* + * Manual assertion-based verification with Z3 + * + * Created on: Feb 19, 2024 + */ + +#ifndef SOFTWARE_ANALYSIS_STUDIO_LAB_Z3_Z3EXAMPLES_H +#define SOFTWARE_ANALYSIS_STUDIO_LAB_Z3_Z3EXAMPLES_H + +#include "Z3Mgr.h" +#include +#include +#include +#include +#include + +namespace SVF { + +class Z3Examples : public Z3Mgr { +public: + Z3Examples(u32_t max) + : Z3Mgr(max) + , maxNumOfExpr(max) + , currentExprIdx(0) {} + + /// Return a Z3 integer value + inline z3::expr getZ3Expr(u32_t val) { + return ctx.int_val(val); + } + + /// Return true if an expression with this name exists + inline bool hasZ3Expr(const std::string& exprName) const { + return strToIDMap.find(exprName) != strToIDMap.end(); + } + + /// Return a Z3 expression with the given name, creating it if necessary + inline z3::expr getZ3Expr(const std::string& exprName) { + auto it = strToIDMap.find(exprName); + if (it != strToIDMap.end()) + return Z3Mgr::getZ3Expr(it->second); + + strToIDMap[exprName] = ++currentExprIdx; + assert(maxNumOfExpr >= currentExprIdx && "expression count exceeds the upper limit"); + z3::expr e = ctx.int_const(exprName.c_str()); + updateZ3Expr(currentExprIdx, e); + return e; + } + + /// Return an address expression for an object with the given name + inline z3::expr getMemObjAddress(const std::string& exprName) { + z3::expr e = getZ3Expr(exprName); + auto iter = strToIDMap.find(exprName); + assert(iter != strToIDMap.end() && "address expression not found?"); + e = getZ3Expr(Z3Mgr::getVirtualMemAddress(iter->second)); + updateZ3Expr(iter->second, e); + return e; + } + + /// Return a field or array-element address from a base pointer and offset + inline z3::expr getGepObjAddress(z3::expr pointer, u32_t offset) { + std::string baseObjName = pointer.to_string(); + auto iter = strToIDMap.find(baseObjName); + assert(iter != strToIDMap.end() && "GEP base-object expression not found?"); + u32_t baseObjID = iter->second; + u32_t gepObj = baseObjID + offset; + if (baseObjID == gepObj) + return pointer; + + // GEP object IDs start halfway through the expression map in this lab. + gepObj += maxNumOfExpr / 2; + z3::expr e = getZ3Expr(Z3Mgr::getVirtualMemAddress(gepObj)); + updateZ3Expr(gepObj, e); + return e; + } + + /// Add a Z3 expression to the solver + void addToSolver(z3::expr e) { + solver.add(e); + } + + /// Reset the solver and expression maps + void resetSolver() { + solver.reset(); + strToIDMap.clear(); + currentExprIdx = 0; + clearVarID2ExprMap(); + } + + /// Print all named expression values after evaluation + void printExprValues() { + std::cout.flags(std::ios::left); + std::cout << "-----------Var and Value-----------\n"; + for (const auto& entry : strToIDMap) { + z3::expr e = Z3Mgr::getEvalExpr(Z3Mgr::getZ3Expr(entry.second)); + if (e.is_numeral()) { + s32_t value = e.get_numeral_int64(); + std::stringstream exprName; + exprName << "Var" << entry.second << " (" << entry.first << ")"; + std::cout << std::setw(25) << exprName.str(); + if (Z3Mgr::isVirtualMemAddress(value)) + std::cout << "\t Value: " << std::hex << "0x" << value << "\n"; + else + std::cout << "\t Value: " << std::dec << value << "\n"; + } + } + std::cout << "-----------------------------------------\n"; + } + + /// TODO: Write Z3 expressions for each example + ///@{ + void test0(); + void test1(); + void test2(); + void test3(); + void test4(); + void test5(); + void test6(); + void test7(); + void test8(); + void test9(); + void test10(); + ///@} + +private: + std::map strToIDMap; + u32_t maxNumOfExpr; + u32_t currentExprIdx; +}; + +} // namespace SVF + +#endif // SOFTWARE_ANALYSIS_STUDIO_LAB_Z3_Z3EXAMPLES_H diff --git a/Lab-Z3/Z3Mgr.cpp b/Lab-Z3/Z3Mgr.cpp new file mode 100644 index 0000000..48d3bd9 --- /dev/null +++ b/Lab-Z3/Z3Mgr.cpp @@ -0,0 +1,93 @@ +//===- Z3Mgr.cpp -- Z3 manager for software verification ----------------===// +// +// SVF: Static Value-Flow Analysis +// +// Copyright (C) <2013-2022> +// + +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. + +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. + +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . +// +//===----------------------------------------------------------------------===// +/* + * Z3 manager for software verification + * + * Created on: Feb 19, 2024 + */ + +#include "Z3Mgr.h" +#include +#include +#include + +using namespace SVF; +using namespace z3; + +/// Store and select for loc2ValMap, i.e., store and load. +/// The address is evaluated before loc2ValMap is accessed. +z3::expr Z3Mgr::storeValue(const z3::expr loc, const z3::expr value) { + z3::expr addr = getEvalExpr(loc); + assert(isVirtualMemAddress(addr) && "pointer operand is not a virtual address?"); + z3::expr loc2ValMap = varID2ExprMap[lastSlot]; + loc2ValMap = z3::store(loc2ValMap, addr, value); + varID2ExprMap.set(lastSlot, loc2ValMap); + return loc2ValMap; +} + +z3::expr Z3Mgr::loadValue(const z3::expr loc) { + z3::expr addr = getEvalExpr(loc); + assert(isVirtualMemAddress(addr) && "pointer operand is not a virtual address?"); + z3::expr loc2ValMap = varID2ExprMap[lastSlot]; + return z3::select(loc2ValMap, addr); +} + +/// Return an integer value from an expression if it is a numeral +s32_t Z3Mgr::z3Expr2NumValue(z3::expr e) { + z3::expr val = getEvalExpr(e); + if (val.is_numeral()) + return val.get_numeral_int64(); + assert(false && "expression is not a numeral"); + abort(); +} + +/// Evaluate an expression using a model satisfying the current constraints +z3::expr Z3Mgr::getEvalExpr(z3::expr e) { + z3::check_result result = solver.check(); + assert(result != z3::unsat && "constraints are unsatisfiable"); + z3::model model = solver.get_model(); + return model.eval(e); +} + +/// Print all expression values after evaluation +void Z3Mgr::printExprValues() { + std::cout.flags(std::ios::left); + std::cout << "-----------Var and Value-----------\n"; + for (u32_t i = 0; i < lastSlot; ++i) { + expr e = getEvalExpr(varID2ExprMap[i]); + if (e.is_numeral()) { + s32_t value = e.get_numeral_int64(); + std::stringstream exprName; + exprName << "Var" << i; + std::cout << std::setw(25) << exprName.str(); + if (isVirtualMemAddress(value)) + std::cout << "\t Value: " << std::hex << "0x" << value << "\n"; + else + std::cout << "\t Value: " << std::dec << value << "\n"; + } + } + std::cout << "-----------------------------------------\n"; +} + +void Z3Mgr::printZ3Exprs() { + std::cout << solver << "\n"; +} diff --git a/Lab-Z3/Z3Mgr.h b/Lab-Z3/Z3Mgr.h new file mode 100644 index 0000000..4a42e8a --- /dev/null +++ b/Lab-Z3/Z3Mgr.h @@ -0,0 +1,157 @@ +//===- Z3Mgr.h -- Z3 manager for software verification ------------------===// +// +// SVF: Static Value-Flow Analysis +// +// Copyright (C) <2013-2022> +// + +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. + +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. + +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . +// +//===----------------------------------------------------------------------===// +/* + * Z3 manager for software verification + * + * Created on: Feb 19, 2024 + */ + +#ifndef SOFTWARE_ANALYSIS_STUDIO_LAB_Z3_Z3MGR_H +#define SOFTWARE_ANALYSIS_STUDIO_LAB_Z3_Z3MGR_H + +#include "z3++.h" + +namespace SVF { + +#ifdef DEBUGINFO +#define DBOP(X) X; +#else +#define DBOP(X) +#endif + +// An ObjVar's ID in SVFIR is marked using AddressMask (0x7f000000) to mimic a +// virtual memory address. This is not a physical runtime address. The flipped +// mask strips the address marker. +#define AddressMask 0x7f000000 +#define FlippedAddressMask (AddressMask ^ 0xffffffff) + +typedef unsigned u32_t; +typedef signed s32_t; + +/// Z3 manager interface +class Z3Mgr { +public: + /// Constructor + Z3Mgr(u32_t numOfMapElems) + : solver(ctx) + , varID2ExprMap(ctx) + , lastSlot(numOfMapElems) { + resetZ3ExprMap(); + } + + /// Reset and reinitialize Z3 expressions. + /// varID2ExprMap maps a variable ID to its Z3 expression. + /// loc2ValMap maps an address location to its stored value. + inline void resetZ3ExprMap() { + varID2ExprMap.resize(lastSlot + 1); + z3::expr loc2ValMap = ctx.constant("loc2ValMap", ctx.array_sort(ctx.int_sort(), ctx.int_sort())); + updateZ3Expr(lastSlot, loc2ValMap); + } + + /// Store and select for loc2ValMap, i.e., store and load + z3::expr storeValue(const z3::expr loc, const z3::expr value); + z3::expr loadValue(const z3::expr loc); + + /// The virtual address starts with 0x7f...... + idx + inline u32_t getVirtualMemAddress(u32_t idx) const { + return AddressMask + idx; + } + + inline bool isVirtualMemAddress(u32_t val) { + return (val > 0 && (val & AddressMask) == AddressMask); + } + + inline bool isVirtualMemAddress(z3::expr e) { + z3::expr val = getEvalExpr(e); + if (val.is_numeral()) + return isVirtualMemAddress(z3Expr2NumValue(val)); + return false; + } + + /// Return the internal index if idx is an address; otherwise return idx + inline u32_t getInternalID(u32_t idx) const { + return (idx & FlippedAddressMask); + } + + /// Return a Z3 expression based on a variable ID + inline z3::expr getZ3Expr(u32_t idx) const { + assert(getInternalID(idx) == idx && "variable idx overflow > 0x7f000000?"); + assert(varID2ExprMap.size() >= idx + 1 && "idx out of bounds; increase map size!"); + return varID2ExprMap[getInternalID(idx)]; + } + + /// Update an expression when processing an assignment + inline void updateZ3Expr(u32_t idx, z3::expr target) { + assert(varID2ExprMap.size() >= idx + 1 && "idx out of bounds; increase map size!"); + varID2ExprMap.set(getInternalID(idx), target); + } + + /// Return an integer value from an expression if it is a numeral + s32_t z3Expr2NumValue(z3::expr e); + + /// Evaluate an expression using a model satisfying the current constraints + z3::expr getEvalExpr(z3::expr e); + + /// Print all expression values after evaluation + void printExprValues(); + + /// Print all Z3 expressions + void printZ3Exprs(); + + /// Return the Z3 solver + inline z3::solver& getSolver() { + return solver; + } + + /// Return the Z3 context + inline z3::context& getCtx() { + return ctx; + } + + /// Clean up the expression map + inline void clearVarID2ExprMap() { + while (!varID2ExprMap.empty()) + varID2ExprMap.pop_back(); + resetZ3ExprMap(); + } + + /// Add not(Q) to the solver. Return true when no counterexample exists. + bool checkNegateAssert(z3::expr q) { + getSolver().push(); + getSolver().add(!q); + bool result = getSolver().check() == z3::unsat; + getSolver().pop(); + return result; + } + +protected: + z3::context ctx; + z3::solver solver; + +private: + z3::expr_vector varID2ExprMap; + u32_t lastSlot; +}; + +} // namespace SVF + +#endif // SOFTWARE_ANALYSIS_STUDIO_LAB_Z3_Z3MGR_H diff --git a/Lab-Z3/test.cpp b/Lab-Z3/test.cpp new file mode 100644 index 0000000..c11a9bb --- /dev/null +++ b/Lab-Z3/test.cpp @@ -0,0 +1,122 @@ +//===- test.cpp -- Manual assertion-based verification driver ------------===// +// +// SVF: Static Value-Flow Analysis +// +// Copyright (C) <2013-2022> +// + +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. + +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. + +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . +// +//===----------------------------------------------------------------------===// +/* + * Manual symbolic execution for assertion-based verification + * + * Created on: Feb 19, 2024 + */ + +#include "Util/SVFUtil.h" +#include "Z3Examples.h" + +using namespace SVF; +using namespace SVFUtil; + +/* + * Lab-Z3 main function entry. + * To run test0, use `bin/lab-z3 test0`. + * To debug it, set "program" to "${workspaceFolder}/bin/lab-z3" and + * "args" to ["test0"] in .vscode/launch.json. + */ +int main(int argc, char** argv) { + if (argc != 2) { + std::cerr << "Usage: ./lab-z3 test0" << std::endl; + return 1; + } + + Z3Examples z3Mgr(1000); + bool result = false; + std::string testName = argv[1]; + + if (testName == "test0") { + z3Mgr.test0(); + // assert(x == 5); + z3::expr assertCond = z3Mgr.getZ3Expr("x") == z3Mgr.getZ3Expr(5); + result = z3Mgr.checkNegateAssert(assertCond); + } + else if (testName == "test1") { + z3Mgr.test1(); + // assert(b > 0); + // TODO: Write the assertion check + } + else if (testName == "test2") { + z3Mgr.test2(); + // assert(b > 3); + // TODO: Write the assertion check + } + else if (testName == "test3") { + z3Mgr.test3(); + // assert(x == 10); + // TODO: Write the assertion check + } + else if (testName == "test4") { + z3Mgr.test4(); + // assert((a + b) > 20); + // TODO: Write the assertion check + } + else if (testName == "test5") { + z3Mgr.test5(); + // assert(b1 >= 5); + // TODO: Write the assertion check + } + else if (testName == "test6") { + z3Mgr.test6(); + // assert(*p == 5); + // TODO: Write the assertion check + } + else if (testName == "test7") { + z3Mgr.test7(); + // assert(d == 5); + // TODO: Write the assertion check + } + else if (testName == "test8") { + z3Mgr.test8(); + // assert(*p == 0); + // TODO: Write the assertion check + } + else if (testName == "test9") { + z3Mgr.test9(); + // assert(z == 15); + // TODO: Write the assertion check + } + else if (testName == "test10") { + z3Mgr.test10(); + // assert(x == 3 && y == 2); + // TODO: Write the assertion check + } + else { + std::cerr << "Invalid test name: " << testName << std::endl; + return 1; + } + + if (result) { + std::cout << testName << " passed!!" << std::endl; + } + else { + std::cout << SVFUtil::errMsg(testName) + << SVFUtil::errMsg(" assertion check failed!!") << std::endl; + assert(result); + } + + z3Mgr.resetSolver(); + return 0; +}