[analyzer] Improved cmake configuration for Z3

Summary:
Enhanced support for Z3 in the cmake configuration of clang; now it is possible to specify any arbitrary Z3 install prefix (CLANG_ANALYZER_Z3_PREFIX) to cmake with lib (or bin) and include folders. Before the patch only in cmake default locations
were searched (https://cmake.org/cmake/help/v3.4/command/find_path.html).

Specifying any CLANG_ANALYZER_Z3_PREFIX will force also CLANG_ANALYZER_BUILD_Z3 to ON.

Removed also Z3 4.5 version requirement since it was not checked, and now Clang works with Z3 4.7

Reviewers: NoQ, george.karpenkov, mikhail.ramalho

Reviewed By: george.karpenkov

Subscribers: rnkovacs, NoQ, esteffin, george.karpenkov, delcypher, ddcc, mgorny, xazax.hun, szepet, a.sidorin, Szelethus

Tags: #clang

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

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@344464 91177308-0d34-0410-b5e6-96231b3b80d8

CMakeLists.txt

@@ -394,22 +394,35 @@ option(CLANG_BUILD_TOOLS
 option(CLANG_ENABLE_ARCMT "Build ARCMT." ON)
 option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON)
 
-option(CLANG_ANALYZER_BUILD_Z3
-  "Build the static analyzer with the Z3 constraint manager." OFF)
+set(CLANG_ANALYZER_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.")
 
-option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF)
+find_package(Z3 4.7.1 EXACT)
 
-if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_BUILD_Z3))
-  message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3")
+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()
 
-if(CLANG_ANALYZER_BUILD_Z3)
-  find_package(Z3 4.5)
-  if(Z3_FOUND)
-    set(CLANG_ANALYZER_WITH_Z3 1)
-  else()
-    message(FATAL_ERROR "Cannot find Z3 header file or shared library")
+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))
+  message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3")
 endif()
 
 if(CLANG_ENABLE_ARCMT)

cmake/modules/FindZ3.cmake

@@ -1,13 +1,36 @@
+# 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)
+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_EXECUTABLE)
+if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
     execute_process (COMMAND ${Z3_EXECUTABLE} -version
       OUTPUT_VARIABLE libz3_version_str
       ERROR_QUIET

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

@@ -926,7 +926,7 @@ SMTSolverRef clang::ento::CreateZ3Solver() {
   return llvm::make_unique<Z3Solver>();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-                           "with -DCLANG_ANALYZER_BUILD_Z3=ON",
+                           "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
                            false);
   return nullptr;
 #endif
@@ -938,7 +938,7 @@ ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
   return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-                           "with -DCLANG_ANALYZER_BUILD_Z3=ON",
+                           "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
                            false);
   return nullptr;
 #endif