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

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/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/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 @@ def have_host_clang_repl_cuda():
 
     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 @@ def use_clang(
                 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(