[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

[Devin Coughlin via Phabricator via cfe-commits]

dcoughlin added a comment.

Thanks for updating the tests to be able to run both the z3 and range-constraint managers! I think this will make it much easier to ensure the z3-backed manager continues to work as as expected moving forward. I suggested an alternative approach inline to running the tests under both managers, which you may wish to consider.

In https://reviews.llvm.org/D28952#669963, @ddcc wrote:

> I added support for a callback field in lit's configuration (see https://reviews.llvm.org/D29684), which is used to execute each testcase for each supported constraint solver backends at runtime. I believe this resolves all remaining issues, except for the remaining two testcase failures:
>
> 1. The testcase Analysis/reference.cpp currently fails, because the RangeConstraintManager has an internal optimization that assumes references are known to be non-zero (see RangeConstraintManager.cpp:422). This optimization is probably in the wrong place, and should be moved into the analyzer and out of the constraint solver. Unless anyone objects, I plan to modify this testcase so that this result is fine for the z3 solver backend.


This sounds reasonable to me.

> 1. The testcase Analysis/ptr-arith.c currently fails, because handling of ptrdiff_t is somewhat tricky. This constraint manager interface maps ptrdiff_t to a signed bitvector in Z3, and pointers to unsigned bitvectors in Z3. However, since this testcase compares the pointer values both directly and indirectly via ptrdiff_t, if a < b is true using a signed comparison, the same is not necessarily true using an unsigned comparison. Likewise, unless anyone objects, I plan to whitelist this result for the z3 solver backend.

I think in both cases whitelisting is the right thing to do -- just provide a comment in the test explaining why. If you have a sense of the right way to fix the problem, please add a // FIXME: in the test with a short description.

There are some minor comments inline. Also: It is important to make sure the build still works and the tests still pass even both when Z3 is not present and when it is not enabled.



================
Comment at: CMakeLists.txt:371
 
+option(CLANG_BUILD_Z3
+  "Build the static analyzer with the Z3 constraint manager." OFF)
----------------
I think it would be good to change the name of this setting to have the prefix "CLANG_ANALYZER_...". This will help make it clear in, for example, the ccmake interface, that the option is only relevant to the analyzer.


================
Comment at: lib/StaticAnalyzer/Core/CMakeLists.txt:62
+  ${Z3_LINK_FILES}
   )
----------------
This needs something like:
```
if(CLANG_BUILD_Z3 AND CLANG_HAVE_Z3)
  target_include_directories(clangStaticAnalyzerCore SYSTEM
  PRIVATE
  ${Z3_INCLUDE_DIR}
  )
endif()
```
so that the analyzer core can find the Z3 headers when they are installed outside of the usual system include paths.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:17
+
+#if defined(CLANG_BUILD_Z3) && defined(CLANG_HAVE_Z3)
+
----------------
Is it possible to expose only one Z3-related definition here? Does the C++ need to understand the distinction between CLANG_HAVE_Z3 and CLANG_BUILD_Z3?

Could the CMake expose one master build setting that is true when other two are both true?


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:21
+
+using namespace clang;
+using namespace ento;
----------------
These 'using' declarations need to be moved outside the #if -- otherwise there is a compile error at the definition of CreateZ3ConstraintManager() when building without Z3.


================
Comment at: test/Analysis/lit.local.cfg:2
+import lit.TestRunner
+
+def callback(test, cmd):
----------------
Here is a suggestion that would avoid needing to block changes to 'lit' itself.

lit allows you to create different a different Test subclass in each test directory. You could create a custom subclass just for analyzer tests (we already do this for unit tests):

```
class AnalyzerTest(lit.formats.ShTest, object):

    def execute(self, test, litConfig):
        result = self.executeWithAnalyzeSubstitution(test, litConfig, '-analyzer-constraints=range')

        if result.code == lit.Test.FAIL:
            return result
      
        if test.config.build_z3 == 'ON' and test.config.have_z3 == '1':
            result = self.executeWithAnalyzeSubstitution(test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3')

        return result

    def executeWithAnalyzeSubstitution(self, test, litConfig, substitution):
        saved_substitutions = list(test.config.substitutions)
        test.config.substitutions.append(('%analyze', substitution))
        result = lit.TestRunner.executeShTest(test, litConfig, self.execute_external)
        test.config.substitutions = saved_substitutions

        return result


config.test_format = AnalyzerTest(config.test_format.execute_external)
```

Saving and mutating the substitutions is kind of janky, but it would avoid blocking this commit on an expanded lit interface.


https://reviews.llvm.org/D28952