WIP: Z3builder

CMakeLists.txt

@@ -123,8 +123,6 @@ find_library(HIREDIS_LIBRARY
   PATHS
   third_party/hiredis/install/lib)
 
-find_library(ALIVE_LIBRARY alive2 PATHS "${ALIVE_DIR}/build")
-
 find_path(Z3_INCLUDE_DIRECTORY
   NAMES
   z3.h
@@ -148,6 +146,8 @@ find_program(Z3
 
 set(TEST_SOLVER "-z3-path=${Z3}")
 
+find_library(ALIVE_LIBRARY alive2 PATHS "${ALIVE_DIR}/build")
+
 set(SOUPER_CLANG_TOOL_FILES
   lib/ClangTool/Actions.cpp
   include/souper/ClangTool/Actions.h
@@ -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")

failing-test.txt

@@ -0,0 +1,13 @@
+Testing Time: 87.60s
+********************
+Failing Tests (2):
+    Souper :: Pass/clang-pass-profile.c
+    Souper :: Tool/too-many-phis.opt
+
+  Expected Passes    : 342
+  Expected Failures  : 3
+  Unexpected Failures: 2
+
+real	1m27.715s
+user	4m12.942s
+sys	0m15.495s

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

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;