[NFC][analyzer] Remove Z3-as-constraint-manager hacks from lit test code (#145731)

Before this commit the LIT test framework of the static analyzer had a
file called `analyzer_test.py` which implemented a tricky system for
selecting the constraint manager:
- (A) Test files without `REQUIRES: z3` were executed with the default
    range-based constraint manager.
- (B) If clang was built with Z3 support _and_ `USE_Z3_SOLVER=1` was
    passed to the test run, the test was executed with Z3 as the
    constraint manager.
(There was support for executing the same RUN line twice if both
conditions were satisfied.)

Unfortunately, using Z3 as the constraint manager does not work in
practice (very slow and causes many crashes), so the (B) pathway became
unused (or was never truly used?) and became broken due to bit rot. (In
the CI bots the analyzer is built without Z3 support, so only the
pathway (A) is used.)

This commit removes `analyzer_test.py` (+ related logic in other build
files + the test `z3/enabled.c` which just tested that
`analyzer_test.py` is active), because it tries to implement a feature
that we don't need (only one constraint manager is functional) and its
code is so complicated and buggy that it isn't useful as a starting
point for future development.

The fact that this logic was broken implied that tests with `REQUIRES:
z3` were not executed during normal testing, so they were also affected
by bit rot. Unfortunately this also affected the tests of the
`z3-crosscheck` mode (aka Z3 refutation) which also depends on Z3 but
uses Z3 in a different way which is actually stable and functional.

In this commit I'm fixing most of the `REQUIRES: z3` tests that were
broken by straightforward issues. Two test files, `PR37855.c` and
`z3-crosscheck.c` were affected by more complex issues, so I marked them
as `XFAIL` for now. We're planning to fix them with follow-up commits in
the foreseeable future.

For additional background information see also the discourse thread
https://discourse.llvm.org/t/taking-ownership-of-clang-test-analysis/84689

clang/docs/analyzer/developer-docs/DebugChecks.rst

@@ -317,15 +317,10 @@ ExprInspection checks
   The value can be represented either as a range set or as a concrete integer.
   For the rest of the types function prints ``n/a`` (aka not available).
 
-  **Note:** This function will print nothing for clang built with Z3 constraint manager.
-  This may cause crashes of your tests. To manage this use one of the test constraining
-  techniques:
-
-  * llvm-lit commands ``REQUIRES no-z3`` or ``UNSUPPORTED z3`` `See for details. <https://llvm.org/docs/TestingGuide.html#constraining-test-execution>`_
-
-  * a preprocessor directive ``#ifndef ANALYZER_CM_Z3``
-
-  * a clang command argument ``-analyzer-constraints=range``
+  **Note:** This function will print nothing when clang uses Z3 as the
+  constraint manager (which is an unsupported and badly broken analysis mode
+  that's distinct from the supported and stable "Z3 refutation" aka "Z3
+  crosscheck" mode).
 
   Example usage::
 

clang/test/Analysis/PR37855.c

@@ -2,6 +2,8 @@
 // RUN: %clang_cc1 -analyze -analyzer-checker=core -w -analyzer-config crosscheck-with-z3=true -verify %s
 // REQUIRES: z3
 
+// XFAIL: *
+
 typedef struct o p;
 struct o {
   struct {

clang/test/Analysis/analyzer_test.py

@@ -1,53 +0,0 @@
-import lit.formats
-import lit.TestRunner
-
-# Custom format class for static analyzer tests
-class AnalyzerTest(lit.formats.ShTest):
-    def __init__(self, execute_external, use_z3_solver=False):
-        super(AnalyzerTest, self).__init__(execute_external)
-        self.use_z3_solver = use_z3_solver
-
-    def execute(self, test, litConfig):
-        results = []
-
-        # Parse any test requirements ('REQUIRES: ')
-        saved_test = test
-        lit.TestRunner.parseIntegratedTestScript(test)
-
-        if "z3" not in test.requires:
-            results.append(
-                self.executeWithAnalyzeSubstitution(
-                    saved_test, litConfig, "-analyzer-constraints=range"
-                )
-            )
-
-            if results[-1].code == lit.Test.FAIL:
-                return results[-1]
-
-        # If z3 backend available, add an additional run line for it
-        if self.use_z3_solver == "1":
-            assert test.config.clang_staticanalyzer_z3 == "1"
-            results.append(
-                self.executeWithAnalyzeSubstitution(
-                    saved_test, litConfig, "-analyzer-constraints=z3 -DANALYZER_CM_Z3"
-                )
-            )
-
-        # Combine all result outputs into the last element
-        for x in results:
-            if x != results[-1]:
-                results[-1].output = x.output + results[-1].output
-
-        if results:
-            return results[-1]
-        return lit.Test.Result(
-            lit.Test.UNSUPPORTED, "Test requires the following unavailable features: z3"
-        )
-
-    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

clang/test/Analysis/bool-assignment.c

@@ -43,11 +43,7 @@ void test_BOOL_initialization(int y) {
     return;
   }
   if (y > 200 && y < 250) {
-#ifdef ANALYZER_CM_Z3
-    BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
-#else
     BOOL x = y; // no-warning
-#endif
     return;
   }
   if (y >= 127 && y < 150) {

clang/test/Analysis/cstring-addrspace.c

@@ -1,6 +1,5 @@
 // RUN: %clang_analyze_cc1 -triple amdgcn-unknown-unknown \
-// RUN: -analyze -analyzer-checker=core,alpha.unix.cstring \
-// RUN: -analyze -analyzer-checker=debug.ExprInspection \
+// RUN: -analyzer-checker=core,alpha.unix.cstring,debug.ExprInspection \
 // RUN: -analyzer-config crosscheck-with-z3=true -verify %s \
 // RUN: -Wno-incompatible-library-redeclaration
 // REQUIRES: z3

clang/test/Analysis/lit.local.cfg

@@ -1,15 +1,7 @@
 # -*- Python -*- vim: set ft=python ts=4 sw=4 expandtab tw=79:
-from lit.llvm.subst import ToolSubst
-import site
+import lit.formats
 
-# Load the custom analyzer test format, which runs the test again with Z3 if it
-# is available.
-site.addsitedir(os.path.dirname(__file__))
-import analyzer_test
-
-config.test_format = analyzer_test.AnalyzerTest(
-    config.test_format.execute_external, config.use_z3_solver
-)
+config.test_format = lit.formats.ShTest(config.test_format.execute_external)
 
 # Filtering command used by Clang Analyzer tests (when comparing .plist files
 # with reference output)

clang/test/Analysis/ptr-arith.c

@@ -221,12 +221,7 @@ void comparisons_imply_size(int *lhs, int *rhs) {
   }
 
   clang_analyzer_eval(lhs <= rhs); // expected-warning{{TRUE}}
-// FIXME: In Z3ConstraintManager, ptrdiff_t is mapped to signed bitvector. However, this does not directly imply the unsigned comparison.
-#ifdef ANALYZER_CM_Z3
-  clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{UNKNOWN}}
-#else
   clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{TRUE}}
-#endif
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
 
   if (lhs >= rhs) {
@@ -236,11 +231,7 @@ void comparisons_imply_size(int *lhs, int *rhs) {
 
   clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
   clang_analyzer_eval(lhs < rhs); // expected-warning{{TRUE}}
-#ifdef ANALYZER_CM_Z3
-  clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
-#else
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
-#endif
 }
 
 void size_implies_comparison(int *lhs, int *rhs) {
@@ -251,11 +242,7 @@ void size_implies_comparison(int *lhs, int *rhs) {
     return;
   }
 
-#ifdef ANALYZER_CM_Z3
-  clang_analyzer_eval(lhs <= rhs); // expected-warning{{UNKNOWN}}
-#else
   clang_analyzer_eval(lhs <= rhs); // expected-warning{{TRUE}}
-#endif
   clang_analyzer_eval((rhs - lhs) >= 0); // expected-warning{{TRUE}}
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{UNKNOWN}}
 
@@ -265,11 +252,7 @@ void size_implies_comparison(int *lhs, int *rhs) {
   }
 
   clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
-  clang_analyzer_eval(lhs < rhs); // expected-warning{{UNKNOWN}}
-#else
   clang_analyzer_eval(lhs < rhs); // expected-warning{{TRUE}}
-#endif
   clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
 }
 

clang/test/Analysis/reference.cpp

@@ -123,26 +123,10 @@ S getS();
 S *getSP();
 
 void testReferenceAddress(int &x) {
-// FIXME: Move non-zero reference assumption out of RangeConstraintManager.cpp:422
-#ifdef ANALYZER_CM_Z3
-  clang_analyzer_eval(&x != 0); // expected-warning{{UNKNOWN}}
-  clang_analyzer_eval(&ref() != 0); // expected-warning{{UNKNOWN}}
-#else
   clang_analyzer_eval(&x != 0); // expected-warning{{TRUE}}
   clang_analyzer_eval(&ref() != 0); // expected-warning{{TRUE}}
-#endif
-
-#ifdef ANALYZER_CM_Z3
-  clang_analyzer_eval(&getS().x != 0); // expected-warning{{UNKNOWN}}
-#else
   clang_analyzer_eval(&getS().x != 0); // expected-warning{{TRUE}}
-#endif
-
-#ifdef ANALYZER_CM_Z3
-  clang_analyzer_eval(&getSP()->x != 0); // expected-warning{{UNKNOWN}}
-#else
   clang_analyzer_eval(&getSP()->x != 0); // expected-warning{{TRUE}}
-#endif
 }
 }
 

clang/test/Analysis/unary-sym-expr-z3-refutation.c

@@ -29,5 +29,5 @@ void k(long L) {
   int h = g + 1;
   int j;
   j += -h < 0; // should not crash
-  // expected-warning@-1{{garbage}}
+  // expected-warning@-1{{The left expression of the compound assignment uses uninitialized memory [core.uninitialized.Assign]}}
 }

clang/test/Analysis/z3-crosscheck-max-attempts.cpp

@@ -4,7 +4,7 @@
 // CHECK: crosscheck-with-z3-max-attempts-per-query = 3
 
 // RUN: rm -rf %t && mkdir %t
-// RUN: %host_cxx -shared -fPIC                           \
+// RUN: %host_cxx -shared -fPIC -I %z3_include_dir        \
 // RUN:   %S/z3/Inputs/MockZ3_solver_check.cpp            \
 // RUN:   -o %t/MockZ3_solver_check.so
 

clang/test/Analysis/z3-crosscheck.c

@@ -2,6 +2,8 @@
 // RUN: %clang_cc1 -triple x86_64-pc-linux-gnu -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
 // REQUIRES: z3
 
+// XFAIL: *
+
 void clang_analyzer_dump(float);
 
 int foo(int x) 
@@ -64,7 +66,7 @@ void floatUnaryNegInEq(int h, int l) {
   clang_analyzer_dump((float)l); // expected-warning-re {{(float) (reg_${{[0-9]+}}<int l>)}}
   if (-(float)h != (float)l) {  // should not crash
     j += 10;
-    // expected-warning@-1{{garbage}}
+    // expected-warning@-1{{The left expression of the compound assignment uses uninitialized memory [core.uninitialized.Assign]}}
   }
 }
 
@@ -74,7 +76,7 @@ void floatUnaryLNotInEq(int h, int l) {
   clang_analyzer_dump((float)l); // expected-warning-re {{(float) (reg_${{[0-9]+}}<int l>)}}
   if ((!(float)h) != (float)l) {  // should not crash
     j += 10;
-    // expected-warning@-1{{garbage}}
+    // expected-warning@-1{{The left expression of the compound assignment uses uninitialized memory [core.uninitialized.Assign]}}
   }
 }
 

clang/test/Analysis/z3/D83660.c

@@ -1,5 +1,5 @@
 // RUN: rm -rf %t && mkdir %t
-// RUN: %host_cxx -shared -fPIC \
+// RUN: %host_cxx -shared -fPIC -I %z3_include_dir \
 // RUN:   %S/Inputs/MockZ3_solver_check.cpp \
 // RUN:   -o %t/MockZ3_solver_check.so
 //

clang/test/Analysis/z3/crosscheck-statistics.c

@@ -4,8 +4,6 @@
 
 // REQUIRES: z3
 
-// expected-error@1 {{Z3 refutation rate:1/2}}
-
 int accepting(int n) {
   if (n == 4) {
     n = n / (n-4); // expected-warning {{Division by zero}}

clang/test/Analysis/z3/enabled.c

@@ -1,3 +0,0 @@
-// REQUIRES: z3
-// RUN: echo %clang_analyze_cc1 | FileCheck %s
-// CHECK: -analyzer-constraints=z3

clang/test/CMakeLists.txt

@@ -124,10 +124,6 @@ if(LLVM_INCLUDE_SPIRV_TOOLS_TESTS)
     )
 endif()    
 
-set(CLANG_TEST_PARAMS
-  USE_Z3_SOLVER=0
-  )
-
 if( NOT CLANG_BUILT_STANDALONE )
   list(APPEND CLANG_TEST_DEPS
     llvm-config
@@ -195,13 +191,11 @@ set_target_properties(clang-test-depends PROPERTIES FOLDER "Clang/Tests")
 add_lit_testsuite(check-clang "Running the Clang regression tests"
   ${CMAKE_CURRENT_BINARY_DIR}
   #LIT ${LLVM_LIT}
-  PARAMS ${CLANG_TEST_PARAMS}
   DEPENDS ${CLANG_TEST_DEPS}
   ARGS ${CLANG_TEST_EXTRA_ARGS}
   )
 
 add_lit_testsuites(CLANG ${CMAKE_CURRENT_SOURCE_DIR}
-  PARAMS ${CLANG_TEST_PARAMS}
   DEPENDS ${CLANG_TEST_DEPS}
   FOLDER "Clang tests/Suites"
 )

clang/test/lit.cfg.py

@@ -175,6 +175,9 @@ if config.clang_staticanalyzer:
 
     if config.clang_staticanalyzer_z3:
         config.available_features.add("z3")
+        config.substitutions.append(
+            ("%z3_include_dir", config.clang_staticanalyzer_z3_include_dir)
+        )
     else:
         config.available_features.add("no-z3")
 

clang/test/lit.site.cfg.py.in

@@ -27,6 +27,7 @@ config.clang_default_pie_on_linux = @CLANG_DEFAULT_PIE_ON_LINUX@
 config.clang_default_cxx_stdlib = "@CLANG_DEFAULT_CXX_STDLIB@"
 config.clang_staticanalyzer = @CLANG_ENABLE_STATIC_ANALYZER@
 config.clang_staticanalyzer_z3 = @LLVM_WITH_Z3@
+config.clang_staticanalyzer_z3_include_dir = "@Z3_INCLUDE_DIR@"
 config.clang_enable_cir = @CLANG_ENABLE_CIR@
 config.clang_examples = @CLANG_BUILD_EXAMPLES@
 config.enable_shared = @ENABLE_SHARED@
@@ -39,7 +40,6 @@ config.reverse_iteration = @LLVM_ENABLE_REVERSE_ITERATION@
 config.host_arch = "@HOST_ARCH@"
 config.perl_executable = "@PERL_EXECUTABLE@"
 config.python_executable = "@Python3_EXECUTABLE@"
-config.use_z3_solver = lit_config.params.get('USE_Z3_SOLVER', "@USE_Z3_SOLVER@")
 config.has_plugins = @CLANG_PLUGIN_SUPPORT@
 config.clang_vendor_uti = "@CLANG_VENDOR_UTI@"
 config.llvm_external_lit = path(r"@LLVM_EXTERNAL_LIT@")

llvm/utils/gn/secondary/clang/test/BUILD.gn

@@ -77,7 +77,6 @@ write_lit_config("lit_site_cfg") {
     "LLVM_USE_SANITIZER=",
     "LLVM_VERSION_MAJOR=$llvm_version_major",
     "Python3_EXECUTABLE=$python_path",
-    "USE_Z3_SOLVER=",
     "PPC_LINUX_DEFAULT_IEEELONGDOUBLE=0",
   ]
 

llvm/utils/lit/lit/llvm/config.py

@@ -629,7 +629,8 @@ class LLVMConfig(object):
                 ToolSubst(
                     "%clang_analyze_cc1",
                     command="%clang_cc1",
-                    extra_args=["-analyze", "%analyze", "-setup-static-analyzer"]
+                    # -setup-static-analyzer ensures that __clang_analyzer__ is defined
+                    extra_args=["-analyze", "-setup-static-analyzer"]
                     + additional_flags,
                 ),
                 ToolSubst(