Author: esteffin Date: Sat Oct 13 12:45:48 2018 New Revision: 344464 URL: http://llvm.org/viewvc/llvm-project?rev=344464&view=rev Log: [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 Modified: cfe/trunk/CMakeLists.txt cfe/trunk/cmake/modules/FindZ3.cmake cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/CMakeLists.txt URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/CMakeLists.txt?rev=344464&r1=344463&r2=344464&view=diff ============================================================================== --- cfe/trunk/CMakeLists.txt (original) +++ cfe/trunk/CMakeLists.txt Sat Oct 13 12:45:48 2018 @@ -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) Modified: cfe/trunk/cmake/modules/FindZ3.cmake URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/cmake/modules/FindZ3.cmake?rev=344464&r1=344463&r2=344464&view=diff ============================================================================== --- cfe/trunk/cmake/modules/FindZ3.cmake (original) +++ cfe/trunk/cmake/modules/FindZ3.cmake Sat Oct 13 12:45:48 2018 @@ -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 Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=344464&r1=344463&r2=344464&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Sat Oct 13 12:45:48 2018 @@ -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(ProgramS 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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
