[NFC][analyzer] Remove Z3-as-constraint-manager hacks from lit test code

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, 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 non-functional 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 script was non-functional implied that tests with
`REQUIRES: z3` were not executed during normal testing, so they were
also affected by bitrot. Unfortunately this also affected the tests of
the `z3-crosscheck` (aka Z3 refutation) mode which also require Z3 (they
don't work if clang is compiled without Z3 support) but use 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 left them
in a failing state; they should be fixed by follow-up commits. Note that
these two tests use `REQUIRES: z3`, so they are not executed in the
automatic buildbots (because before this commit if somebody tried to run
the tests on a clang built with Z3 supports, `analyzer_test.py` would
have ran into an assertion failure).

Author: NagyDonat

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/analyzer_test.py

@@ -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/bool-assignment.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/cstring-addrspace.c

@@ -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/lit.local.cfg

@@ -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/ptr-arith.c

@@ -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/reference.cpp

@@ -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/unary-sym-expr-z3-refutation.c

@@ -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-max-attempts.cpp

@@ -64,7 +64,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 +74,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]}}
   }
 }