Moved everything SMT-related to LLVM and updated the cmake scripts.

Differential Revision: https://reviews.llvm.org/D54978

llvm-svn: 356929

clang/CMakeLists.txt

@@ -447,34 +447,9 @@ option(CLANG_BUILD_TOOLS
 option(CLANG_ENABLE_ARCMT "Build ARCMT." ON)
 option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON)
 
-set(CLANG_ANALYZER_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.")
-
-find_package(Z3 4.7.1)
-
-if (CLANG_ANALYZER_Z3_INSTALL_DIR)
-  if (NOT Z3_FOUND)
-    message(FATAL_ERROR "Z3 4.7.1 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR: ${CLANG_ANALYZER_Z3_INSTALL_DIR}.")
-  endif()
-endif()
-
-set(CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
-
-option(CLANG_ANALYZER_ENABLE_Z3_SOLVER
-  "Enable Support for the Z3 constraint solver in the Clang Static Analyzer."
-  ${CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT}
-)
-
-if (CLANG_ANALYZER_ENABLE_Z3_SOLVER)
-  if (NOT Z3_FOUND)
-    message(FATAL_ERROR "CLANG_ANALYZER_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.")
-  endif()
-
-  set(CLANG_ANALYZER_WITH_Z3 1)
-endif()
-
 option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF)
 
-if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_ENABLE_Z3_SOLVER))
+if(NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT)
   message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3")
 endif()
 

clang/cmake/modules/FindZ3.cmake

@@ -1,51 +0,0 @@
-# Looking for Z3 in CLANG_ANALYZER_Z3_INSTALL_DIR
-find_path(Z3_INCLUDE_DIR NAMES z3.h
-   NO_DEFAULT_PATH
-   PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}/include
-   PATH_SUFFIXES libz3 z3
-   )
-
-find_library(Z3_LIBRARIES NAMES z3 libz3
-   NO_DEFAULT_PATH
-   PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}
-   PATH_SUFFIXES lib bin
-   )
-
-find_program(Z3_EXECUTABLE z3
-   NO_DEFAULT_PATH
-   PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}
-   PATH_SUFFIXES bin
-   )
-
-# If Z3 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR look in the default directories
-find_path(Z3_INCLUDE_DIR NAMES z3.h
-   PATH_SUFFIXES libz3 z3
-   )
-
-find_library(Z3_LIBRARIES NAMES z3 libz3
-   PATH_SUFFIXES lib bin
-   )
-
-find_program(Z3_EXECUTABLE z3
-   PATH_SUFFIXES bin
-   )
-
-if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
-    execute_process (COMMAND ${Z3_EXECUTABLE} -version
-      OUTPUT_VARIABLE libz3_version_str
-      ERROR_QUIET
-      OUTPUT_STRIP_TRAILING_WHITESPACE)
-
-    string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"
-           Z3_VERSION_STRING "${libz3_version_str}")
-    unset(libz3_version_str)
-endif()
-
-# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
-# all listed variables are TRUE
-include(FindPackageHandleStandardArgs)
-FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3
-                                  REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR
-                                  VERSION_VAR Z3_VERSION_STRING)
-
-mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)

clang/include/clang/Config/config.h.cmake

@@ -57,9 +57,6 @@
 /* Define if we have libxml2 */
 #cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML}
 
-/* Define if we have z3 and want to build it */
-#cmakedefine CLANG_ANALYZER_WITH_Z3 ${CLANG_ANALYZER_WITH_Z3}
-
 /* Define if we have sys/resource.h (rlimits) */
 #cmakedefine CLANG_HAVE_RLIMITS ${CLANG_HAVE_RLIMITS}
 

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

@@ -18,15 +18,15 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 
 typedef llvm::ImmutableSet<
-    std::pair<clang::ento::SymbolRef, const clang::ento::SMTExpr *>>
+    std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
     ConstraintSMTType;
 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType)
 
 namespace clang {
 namespace ento {
 
 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
-  mutable SMTSolverRef Solver = CreateZ3Solver();
+  mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
 
 public:
   SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
@@ -44,7 +44,8 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
     QualType RetTy;
     bool hasComparison;
 
-    SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
+    llvm::SMTExprRef Exp =
+        SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
 
     // Create zero comparison for implicit boolean cast, with reversed
     // assumption
@@ -80,12 +81,12 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
 
     QualType RetTy;
     // The expression may be casted, so we cannot call getZ3DataExpr() directly
-    SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
-    SMTExprRef Exp =
+    llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
+    llvm::SMTExprRef Exp =
         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
 
     // Negate the constraint
-    SMTExprRef NotExp =
+    llvm::SMTExprRef NotExp =
         SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
 
     ConditionTruthVal isSat = checkModel(State, Sym, Exp);
@@ -118,7 +119,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
       // this method tries to get the interpretation (the actual value) from
       // the solver, which is currently not cached.
 
-      SMTExprRef Exp =
+      llvm::SMTExprRef Exp =
           SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
 
       Solver->reset();
@@ -134,7 +135,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
         return nullptr;
 
       // A value has been obtained, check if it is the only value
-      SMTExprRef NotExp = SMTConv::fromBinOp(
+      llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
           Solver, Exp, BO_NE,
           Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
                               : Solver->mkBitvector(Value, Value.getBitWidth()),
@@ -277,7 +278,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
 protected:
   // Check whether a new model is satisfiable, and update the program state.
   virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
-                                     const SMTExprRef &Exp) {
+                                     const llvm::SMTExprRef &Exp) {
     // Check the model, avoid simplifying AST to save time
     if (checkModel(State, Sym, Exp).isConstrainedTrue())
       return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
@@ -294,9 +295,9 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
 
     // Construct the logical AND of all the constraints
     if (I != IE) {
-      std::vector<SMTExprRef> ASTs;
+      std::vector<llvm::SMTExprRef> ASTs;
 
-      SMTExprRef Constraint = I++->second;
+      llvm::SMTExprRef Constraint = I++->second;
       while (I != IE) {
         Constraint = Solver->mkAnd(Constraint, I++->second);
       }
@@ -307,7 +308,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
 
   // Generate and check a Z3 model, using the given constraint.
   ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
-                               const SMTExprRef &Exp) const {
+                               const llvm::SMTExprRef &Exp) const {
     ProgramStateRef NewState =
         State->add<ConstraintSMT>(std::make_pair(Sym, Exp));