[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,6 +50,7 @@ add_clang_library(clangStaticAnalyzerCore
   Store.cpp
   SubEngine.cpp
   SymbolManager.cpp
+  Z3ConstraintManager.cpp
 
   LINK_LIBS
   clangAST
@@ -50,4 +58,12 @@ add_clang_library(clangStaticAnalyzerCore
   clangBasic
   clangLex
   clangRewrite
+  ${Z3_LINK_FILES}
   )
+
+if(CLANG_ANALYZER_WITH_Z3)
+  target_include_directories(clangStaticAnalyzerCore SYSTEM
+    PRIVATE
+    ${Z3_INCLUDE_DIR}
+    )
+endif()

clang/test/Analysis/expr-inspection.c

@@ -19,4 +19,4 @@ void foo(int x) {
 
 // CHECK: Expressions:
 // CHECK-NEXT: clang_analyzer_printState : &code{clang_analyzer_printState}
-// CHECK-NEXT: Ranges are empty.
+// CHECK-NEXT: {{(Ranges are empty.)|(Constraints:[[:space:]]*$)}}

clang/test/Analysis/lit.local.cfg

@@ -10,6 +10,10 @@ class AnalyzerTest(lit.formats.ShTest, object):
         if result.code == lit.Test.FAIL:
             return result
 
+        # If z3 backend available, add an additional run line for it
+        if test.config.clang_staticanalyzer_z3 == '1':
+            result = self.executeWithAnalyzeSubstitution(test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3')
+
         return result
 
     def executeWithAnalyzeSubstitution(self, test, litConfig, substitution):

clang/test/Analysis/unsupported-types.c

@@ -0,0 +1,31 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -triple x86_64-unknown-linux -verify %s
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -triple powerpc64-linux-gnu -verify %s
+
+#define _Complex_I      (__extension__ 1.0iF)
+
+void clang_analyzer_eval(int);
+
+void complex_float(double _Complex x, double _Complex y) {
+  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
+  if (x != 1.0 + 3.0 * _Complex_I && y != 1.0 - 4.0 * _Complex_I)
+    return
+  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(x + y == 2.0 - 1.0 * _Complex_I); // expected-warning{{UNKNOWN}}
+}
+
+void complex_int(int _Complex x, int _Complex y) {
+  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
+  if (x != 1.0 + 3.0 * _Complex_I && y != 1.0 - 4.0 * _Complex_I)
+    return
+  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(x + y == 2.0 - 1.0 * _Complex_I); // expected-warning{{UNKNOWN}}
+}
+
+void longdouble_float(long double x, long double y) {
+  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
+  if (x != 0.0L && y != 1.0L)
+    return
+  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(x + y == 1.0L); // expected-warning{{UNKNOWN}}
+}

clang/test/lit.cfg

@@ -361,6 +361,9 @@ if config.clang_default_cxx_stdlib != '':
 if config.clang_staticanalyzer:
     config.available_features.add("staticanalyzer")
 
+    if config.clang_staticanalyzer_z3 == '1':
+        config.available_features.add("z3")
+
 # As of 2011.08, crash-recovery tests still do not pass on FreeBSD.
 if platform.system() not in ['FreeBSD']:
     config.available_features.add('crash-recovery')

clang/test/lit.site.cfg.in

@@ -18,6 +18,7 @@ config.have_zlib = @HAVE_LIBZ@
 config.clang_arcmt = @CLANG_ENABLE_ARCMT@
 config.clang_default_cxx_stdlib = "@CLANG_DEFAULT_CXX_STDLIB@"
 config.clang_staticanalyzer = @CLANG_ENABLE_STATIC_ANALYZER@
+config.clang_staticanalyzer_z3 = "@CLANG_ANALYZER_WITH_Z3@"
 config.clang_examples = @CLANG_BUILD_EXAMPLES@
 config.enable_shared = @ENABLE_SHARED@
 config.enable_backtrace = @ENABLE_BACKTRACES@