[analyzer] Add new Z3 constraint manager backend

Summary: Implement new Z3 constraint manager backend.

Reviewers: zaks.anna, dcoughlin, NoQ, xazax.hun

Subscribers: mgorny, cfe-commits

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

llvm-svn: 299463

clang/CMakeLists.txt

@@ -186,6 +186,8 @@ if (LIBXML2_FOUND)
   set(CLANG_HAVE_LIBXML 1)
 endif()
 
+find_package(Z3 4.5)
+
 include(CheckIncludeFile)
 check_include_file(sys/resource.h CLANG_HAVE_RLIMITS)
 
@@ -330,10 +332,6 @@ if (APPLE)
   endif()
 endif()
 
-configure_file(
-  ${CLANG_SOURCE_DIR}/include/clang/Config/config.h.cmake
-  ${CLANG_BINARY_DIR}/include/clang/Config/config.h)
-
 include(CMakeParseArguments)
 include(AddClang)
 
@@ -371,8 +369,19 @@ option(CLANG_BUILD_TOOLS
 option(CLANG_ENABLE_ARCMT "Build ARCMT." ON)
 option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON)
 
-if (NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT)
-  message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT")
+option(CLANG_ANALYZER_BUILD_Z3
+  "Build the static analyzer with the Z3 constraint manager." OFF)
+
+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")
+endif()
+
+if(CLANG_ANALYZER_BUILD_Z3)
+  if(Z3_FOUND)
+    set(CLANG_ANALYZER_WITH_Z3 1)
+  else()
+    message(FATAL_ERROR "Cannot find Z3 header file or shared library")
+  endif()
 endif()
 
 if(CLANG_ENABLE_ARCMT)
@@ -687,3 +696,7 @@ endif()
 if (LLVM_ADD_NATIVE_VISUALIZERS_TO_SOLUTION)
   add_subdirectory(utils/ClangVisualizers)
 endif()
+
+configure_file(
+  ${CLANG_SOURCE_DIR}/include/clang/Config/config.h.cmake
+  ${CLANG_BINARY_DIR}/include/clang/Config/config.h)

clang/cmake/modules/FindZ3.cmake

@@ -0,0 +1,28 @@
+find_path(Z3_INCLUDE_DIR NAMES z3.h
+   PATH_SUFFIXES libz3
+   )
+
+find_library(Z3_LIBRARIES NAMES z3 libz3
+   )
+
+find_program(Z3_EXECUTABLE z3)
+
+if(Z3_INCLUDE_DIR 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

@@ -38,6 +38,9 @@
 /* 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/Analyses.def

@@ -22,6 +22,7 @@ ANALYSIS_STORE(RegionStore, "region", "Use region-based analyzer store", CreateR
 #endif
 
 ANALYSIS_CONSTRAINTS(RangeConstraints, "range", "Use constraint tracking of concrete value ranges", CreateRangeConstraintManager)
+ANALYSIS_CONSTRAINTS(Z3Constraints, "z3", "Use Z3 contraint solver", CreateZ3ConstraintManager)
 
 #ifndef ANALYSIS_DIAGNOSTICS
 #define ANALYSIS_DIAGNOSTICS(NAME, CMDFLAG, DESC, CREATEFN)

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

@@ -184,6 +184,9 @@ std::unique_ptr<ConstraintManager>
 CreateRangeConstraintManager(ProgramStateManager &statemgr,
                              SubEngine *subengine);
 
+std::unique_ptr<ConstraintManager>
+CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine);
+
 } // end GR namespace
 
 } // end clang namespace

clang/lib/StaticAnalyzer/Core/CMakeLists.txt

@@ -1,5 +1,12 @@
 set(LLVM_LINK_COMPONENTS support)
 
+# Link Z3 if the user wants to build it.
+if(CLANG_ANALYZER_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_clang_library(clangStaticAnalyzerCore
   APSIntType.cpp
   AnalysisManager.cpp
@@ -43,11 +50,20 @@ add_clang_library(clangStaticAnalyzerCore
   Store.cpp
   SubEngine.cpp
   SymbolManager.cpp
+  Z3ConstraintManager.cpp
 
   LINK_LIBS
   clangAST
   clangAnalysis
   clangBasic
   clangLex
   clangRewrite
+  ${Z3_LINK_FILES}
   )
+
+if(CLANG_ANALYZER_WITH_Z3)
+  target_include_directories(clangStaticAnalyzerCore SYSTEM
+    PRIVATE
+    ${Z3_INCLUDE_DIR}
+    )
+endif()