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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
