Initial version of the z3 expression builder

google · Feb 11, 2019 · 7d806c4 · 7d806c4
1 parent 233bbd1
commit 7d806c4
Show file tree

Hide file tree

Showing 9 changed files with 451 additions and 9 deletions.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -162,6 +162,7 @@ set(SOUPER_EXTRACTOR_FILES
   lib/Extractor/ExprBuilder.cpp
   lib/Extractor/KLEEBuilder.cpp
   lib/Extractor/Solver.cpp
+  lib/Extractor/Z3Builder.cpp
   include/souper/Extractor/Candidates.h
   include/souper/Extractor/ExprBuilder.h
   include/souper/Extractor/Solver.h
@@ -363,7 +364,7 @@ if(NOT GO_EXECUTABLE STREQUAL "GO_EXECUTABLE-NOTFOUND")
     PROPERTIES COMPILE_FLAGS "${LLVM_CXXFLAGS}")
   target_include_directories(souperweb-backend PRIVATE "${LLVM_INCLUDEDIR}")
 
-  target_link_libraries(souperweb-backend souperTool souperExtractor souperKVStore souperSMTLIB2 souperParser souperInst ${HIREDIS_LIBRARY})
+  target_link_libraries(souperweb-backend souperTool souperExtractor souperKVStore souperSMTLIB2 souperParser souperInst ${HIREDIS_LIBRARY} ${Z3_LIBRARY})
 
   add_custom_target(souperweb ALL COMMAND ${GO_EXECUTABLE} build -o ${CMAKE_BINARY_DIR}/souperweb ${CMAKE_SOURCE_DIR}/tools/souperweb.go
                                   COMMENT "Building souperweb")

diff --git a/include/souper/Extractor/ExprBuilder.h b/include/souper/Extractor/ExprBuilder.h
@@ -40,7 +40,8 @@ class ExprBuilder {
   const unsigned MAX_PHI_DEPTH = 25;
 public:
   enum Builder {
-    KLEE
+    KLEE,
+    Z3
   };
 
   ExprBuilder(InstContext &IC) : LIC(&IC) {}
@@ -108,6 +109,7 @@ std::string BuildQuery(InstContext &IC, const BlockPCs &BPCs,
        std::vector<Inst *> *ModelVars, bool Negate=false);
 
 std::unique_ptr<ExprBuilder> createKLEEBuilder(InstContext &IC);
+std::unique_ptr<ExprBuilder> createZ3Builder(InstContext &IC);
 }
 
 #endif  // SOUPER_EXTRACTOR_EXPRBUILDER_H
diff --git a/lib/Extractor/ExprBuilder.cpp b/lib/Extractor/ExprBuilder.cpp
@@ -25,7 +25,9 @@ static llvm::cl::opt<souper::ExprBuilder::Builder> SMTExprBuilder(
     llvm::cl::desc("SMT-LIBv2 expression builder (default=klee)"),
     llvm::cl::values(clEnumValN(souper::ExprBuilder::KLEE, "klee",
                                 "Use KLEE's Expr library")),
-    llvm::cl::init(souper::ExprBuilder::KLEE));
+    llvm::cl::values(clEnumValN(souper::ExprBuilder::Z3, "z3",
+                                "Use Z3 API")),
+    llvm::cl::init(souper::ExprBuilder::Z3));
 
 bool ExprBuilder::getUBPaths(Inst *I, UBPath *Current,
                              std::vector<std::unique_ptr<UBPath>> &Paths,
@@ -954,6 +956,9 @@ std::string BuildQuery(InstContext &IC, const BlockPCs &BPCs,
   case ExprBuilder::KLEE:
     EB = createKLEEBuilder(IC);
     break;
+  case ExprBuilder::Z3:
+    EB = createZ3Builder(IC);
+    break;
   default:
     llvm::report_fatal_error("cannot reach here");
     break;