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

NagyDonat · 2025-06-25T15:59:29Z

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

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).

llvmbot · 2025-06-25T16:00:10Z

@llvm/pr-subscribers-testing-tools

@llvm/pr-subscribers-clang-static-analyzer-1

Author: Donát Nagy (NagyDonat)

Changes

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).

Full diff: https://github.com/llvm/llvm-project/pull/145731.diff

19 Files Affected:

(modified) clang/docs/analyzer/developer-docs/DebugChecks.rst (+4-9)
(removed) clang/test/Analysis/analyzer_test.py (-53)
(modified) clang/test/Analysis/bool-assignment.c (-4)
(modified) clang/test/Analysis/cstring-addrspace.c (+1-2)
(modified) clang/test/Analysis/lit.local.cfg (+2-10)
(modified) clang/test/Analysis/ptr-arith.c (-17)
(modified) clang/test/Analysis/reference.cpp (-16)
(modified) clang/test/Analysis/unary-sym-expr-z3-refutation.c (+1-1)
(modified) clang/test/Analysis/z3-crosscheck-max-attempts.cpp (+1-1)
(modified) clang/test/Analysis/z3-crosscheck.c (+2-2)
(modified) clang/test/Analysis/z3/D83660.c (+2-2)
(modified) clang/test/Analysis/z3/crosscheck-statistics.c (-2)
(removed) clang/test/Analysis/z3/enabled.c (-3)
(modified) clang/test/CMakeLists.txt (-6)
(modified) clang/test/lit.cfg.py (+6)
(modified) clang/test/lit.site.cfg.py.in (+1-1)
(modified) llvm/cmake/modules/FindZ3.cmake (+1-1)
(modified) llvm/utils/gn/secondary/clang/test/BUILD.gn (-1)
(modified) llvm/utils/lit/lit/llvm/config.py (+2-1)

diff --git a/clang/docs/analyzer/developer-docs/DebugChecks.rst b/clang/docs/analyzer/developer-docs/DebugChecks.rst
index f03a6ecf2683f..767ef6565d335 100644
--- a/clang/docs/analyzer/developer-docs/DebugChecks.rst
+++ b/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::
 
diff --git a/clang/test/Analysis/analyzer_test.py b/clang/test/Analysis/analyzer_test.py
deleted file mode 100644
index c476ceea9a59e..0000000000000
--- a/clang/test/Analysis/analyzer_test.py
+++ /dev/null
@@ -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
diff --git a/clang/test/Analysis/bool-assignment.c b/clang/test/Analysis/bool-assignment.c
index 3a104cf627ffa..f0942cc4d3499 100644
--- a/clang/test/Analysis/bool-assignment.c
+++ b/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) {
diff --git a/clang/test/Analysis/cstring-addrspace.c b/clang/test/Analysis/cstring-addrspace.c
index d6b455510e36e..fc00a78026573 100644
--- a/clang/test/Analysis/cstring-addrspace.c
+++ b/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
diff --git a/clang/test/Analysis/lit.local.cfg b/clang/test/Analysis/lit.local.cfg
index e2946cf345cb9..f08ff8d6cce63 100644
--- a/clang/test/Analysis/lit.local.cfg
+++ b/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)
diff --git a/clang/test/Analysis/ptr-arith.c b/clang/test/Analysis/ptr-arith.c
index b5ccd2c207ead..79ca190b25a0f 100644
--- a/clang/test/Analysis/ptr-arith.c
+++ b/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}}
 }
 
diff --git a/clang/test/Analysis/reference.cpp b/clang/test/Analysis/reference.cpp
index 91ba3cd23249a..e6986fb8e7058 100644
--- a/clang/test/Analysis/reference.cpp
+++ b/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
 }
 }
 
diff --git a/clang/test/Analysis/unary-sym-expr-z3-refutation.c b/clang/test/Analysis/unary-sym-expr-z3-refutation.c
index 33585236232ad..f103fdbd285b0 100644
--- a/clang/test/Analysis/unary-sym-expr-z3-refutation.c
+++ b/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]}}
 }
diff --git a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
index 7951d26546473..572e452fdcac2 100644
--- a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
+++ b/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
 
diff --git a/clang/test/Analysis/z3-crosscheck.c b/clang/test/Analysis/z3-crosscheck.c
index 13f38f43e6974..5cceaf4115db0 100644
--- a/clang/test/Analysis/z3-crosscheck.c
+++ b/clang/test/Analysis/z3-crosscheck.c
@@ -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]}}
   }
 }
 
diff --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c
index b42d934bcc9e7..048746c8e673d 100644
--- a/clang/test/Analysis/z3/D83660.c
+++ b/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
 //
@@ -9,7 +9,7 @@
 // RUN:   -analyzer-checker=core %s -verify
 //
 // REQUIRES: z3, asserts, shell, system-linux
-//
+
 // Works only with the z3 constraint manager.
 // expected-no-diagnostics
 
diff --git a/clang/test/Analysis/z3/crosscheck-statistics.c b/clang/test/Analysis/z3/crosscheck-statistics.c
index 8db3df169f246..cab31b18f50ef 100644
--- a/clang/test/Analysis/z3/crosscheck-statistics.c
+++ b/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}}
diff --git a/clang/test/Analysis/z3/enabled.c b/clang/test/Analysis/z3/enabled.c
deleted file mode 100644
index 9f44233b266c0..0000000000000
--- a/clang/test/Analysis/z3/enabled.c
+++ /dev/null
@@ -1,3 +0,0 @@
-// REQUIRES: z3
-// RUN: echo %clang_analyze_cc1 | FileCheck %s
-// CHECK: -analyzer-constraints=z3
diff --git a/clang/test/CMakeLists.txt b/clang/test/CMakeLists.txt
index 35a8042ac0e0a..e5b4a3bb84645 100644
--- a/clang/test/CMakeLists.txt
+++ b/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"
 )
diff --git a/clang/test/lit.cfg.py b/clang/test/lit.cfg.py
index 2b35bb5dcbdaf..bfdb008c5fab9 100644
--- a/clang/test/lit.cfg.py
+++ b/clang/test/lit.cfg.py
@@ -175,6 +175,12 @@ 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")
 
diff --git a/clang/test/lit.site.cfg.py.in b/clang/test/lit.site.cfg.py.in
index 77c5f27f47c92..00480d34852da 100644
--- a/clang/test/lit.site.cfg.py.in
+++ b/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@")
diff --git a/llvm/cmake/modules/FindZ3.cmake b/llvm/cmake/modules/FindZ3.cmake
index 2981753c84fe1..954a058fe6131 100644
--- a/llvm/cmake/modules/FindZ3.cmake
+++ b/llvm/cmake/modules/FindZ3.cmake
@@ -83,7 +83,7 @@ endif()
 
 # If the dynamic check fails, we might be cross compiling: if that's the case,
 # check the version in the headers, otherwise, fail with a message
-if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND
+if(NOT Z3_VERSION_STRING AND (
                               Z3_INCLUDE_DIR AND
                               EXISTS "${Z3_INCLUDE_DIR}/z3_version.h"))
   # TODO: print message warning that we couldn't find a compatible lib?
diff --git a/llvm/utils/gn/secondary/clang/test/BUILD.gn b/llvm/utils/gn/secondary/clang/test/BUILD.gn
index d8581650f1cb0..c3dce0a7d07e5 100644
--- a/llvm/utils/gn/secondary/clang/test/BUILD.gn
+++ b/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",
   ]
 
diff --git a/llvm/utils/lit/lit/llvm/config.py b/llvm/utils/lit/lit/llvm/config.py
index c134cda90e2ee..5459d431d696b 100644
--- a/llvm/utils/lit/lit/llvm/config.py
+++ b/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(

github-actions · 2025-06-25T16:02:03Z

✅ With the latest revision this PR passed the Python code formatter.

NagyDonat · 2025-06-25T16:04:44Z

For background information see also some of the later comments on the discourse thread https://discourse.llvm.org/t/taking-ownership-of-clang-test-analysis/84689/6

steakhal · 2025-06-25T16:06:14Z

For background information see also some of the later comments on the discourse thread https://discourse.llvm.org/t/taking-ownership-of-clang-test-analysis/84689/6

Move this link into the PR summary please.

NagyDonat · 2025-06-25T16:10:20Z

For background information see also some of the later comments on the discourse thread https://discourse.llvm.org/t/taking-ownership-of-clang-test-analysis/84689/6

Move this link into the PR summary please.

Done. (Originally I didn't put this into the PR summary because I felt that the information on this thread is not so valuable / important.)

steakhal

LGTM

clang/test/Analysis/reference.cpp

necto

I have no experience with this part, but the change looks reasonable, and I support getting rid of unused code

NagyDonat · 2025-06-26T12:15:58Z

I showed the contents of this commit to @gamesh411 and we decided to mark the two "expected to fail" tests with XFAIL to ensure that we don't introduce new failures (he clarified that before my commit by default they were in an UNSUPPORTED state, and not a crashing/failing state).

mgorny · 2025-06-26T18:40:42Z

This change broke standalone clang builds:

FAIL: Clang :: Analysis/z3/D83660.c (1480 of 21630)
******************** TEST 'Clang :: Analysis/z3/D83660.c' FAILED ********************
Exit Code: 1

Command Output (stderr):
--
rm -rf /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/z3/Output/D83660.c.tmp && mkdir /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/z3/Output/D83660.c.tmp # RUN: at line 1
+ rm -rf /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/z3/Output/D83660.c.tmp
+ mkdir /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/z3/Output/D83660.c.tmp
/usr/lib/ccache/bin/x86_64-pc-linux-gnu-g++ -shared -fPIC -I     /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp    -o /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/z3/Output/D83660.c.tmp/MockZ3_solver_check.so # RUN: at line 2
+ /usr/lib/ccache/bin/x86_64-pc-linux-gnu-g++ -shared -fPIC -I /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp -o /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/z3/Output/D83660.c.tmp/MockZ3_solver_check.so
x86_64-pc-linux-gnu-g++: fatal error: no input files
compilation terminated.

--

********************
******************** TEST 'Clang :: Analysis/z3-crosscheck-max-attempts.cpp' FAILED ********************                               
Exit Code: 1                                                                                                                           
                                                                                                                                       
Command Output (stderr):                                                                                                               
--                                                                                                                                     
/var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/clang -cc1 -internal-isystem /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/../../../../lib/clang/21/include -nostdsysteminc -analyze -setup-static-analyzer -analyzer-checker=debug.ConfigDumper 2>&1  | /usr/lib/llvm/21/bin/FileCheck /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3-crosscheck-max-attempts.cpp --match-full-lines # RUN: at line 2                                                            
+ /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/clang -cc1 -internal-isystem /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/../../../../lib/clang/21/include -nostdsysteminc -analyze -setup-static-analyzer -analyzer-checker=debug.ConfigDumper                                                                                                   
+ /usr/lib/llvm/21/bin/FileCheck /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3-crosscheck-max-attempts.cpp --match-full-lines                                                                                                                      
rm -rf /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.tmp && mkdir /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.tmp # RUN: at line 6                                                                                                               
+ rm -rf /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.tmp                                                                                                                                   
+ mkdir /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.tmp                                                                                                                                    
/usr/lib/ccache/bin/x86_64-pc-linux-gnu-g++ -shared -fPIC -I            /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp               -o /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.tmp/MockZ3_solver_check.so # RUN: at line 7                                          
+ /usr/lib/ccache/bin/x86_64-pc-linux-gnu-g++ -shared -fPIC -I /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp -o /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.tmp/MockZ3_solver_check.so                                                                                  
x86_64-pc-linux-gnu-g++: fatal error: no input files                                                                                   
compilation terminated.                                                                                                                
                                                                                                                                       
--                                                                                                                                     
                                                                                                                                       
********************

FWICS the problem is that Z3_INCLUDE_DIR is not set in clang.

…ode (llvm#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

steakhal · 2025-06-26T19:56:44Z

@mgorny I'm no longer available. Could you or anyone revert this or disable the failing tests using an "UNSPUPPORTED: *"?

steakhal · 2025-06-27T08:46:45Z

@NagyDonat Can you look into this reported failure?
@mgorny Could you give a link to the build bot that failed?

NagyDonat · 2025-06-27T09:08:09Z

Sorry for the failures -- I'll try to troubleshoot them ASAP.

NagyDonat · 2025-06-27T09:26:21Z

I created PR #146042 which should hopefully fix this issue. (Right now I'm rebuilding clang to ensure that it is indeed working.)

NagyDonat · 2025-06-27T09:50:11Z

@mgorny I was unable to reproduce the failure that you observed -- based on the error message that you posted, you're in a situation where Z3_INCLUDE_DIR is not set by the clang build system but these two tests which are marked with REQUIRES: z3 are still executed somehow. (Perhaps you have Z3 installed in a standard system include directory?)

Nevertheless, my fix #146042 should work even in this case.

mgorny · 2025-06-27T11:20:53Z

As I've said, my issue is specific to the standalone build. You install LLVM first, then build clang against installed LLVM. Installed LLVM configs indicate whether LLVM was built against Z3, but they don't include internal Z3 lookup variables.

mgorny · 2025-06-27T12:43:03Z

I'm probably going to spend the whole day today bisecting another issue, then I can look into providing a quick patch.

NagyDonat · 2025-06-27T12:52:47Z

Thank you, that would be very helpful! I'm not familiar with the cmake implementation details of the standalone build (until now I didn't even know about its existence), so finding a solution would've taken lots of time for me.

mgorny · 2025-06-27T15:40:16Z

No problem. I would have submitted a patch earlier but this bisect is literally taking all my resources.

NagyDonat · 2025-06-27T15:42:55Z

I'll be on vacation during the weekend and on Monday, so feel free to merge the fix without me if you have it.

steakhal · 2025-06-27T15:45:07Z

No problem. I would have submitted a patch earlier but this bisect is literally taking all my resources.

@mgorny I'm pretty sure you have heard of manyclangs. If you bisect clang builds, that should come handy. Saved me many hours already - and counting.

mgorny · 2025-06-27T15:50:01Z

@mgorny I'm pretty sure you have heard of manyclangs. If you bisect clang builds, that should come handy. Saved me many hours already - and counting.

I haven't but I doubt they'll help me — this issue seems to surface only with our specific build of Flang somehow.

Fix running tests that require Z3 headers in standalone build. They were wrongly relying on `Z3_INCLUDE_DIR` being passed through from LLVM, which is not the case for a standalone build. Instead, perform `find_package(Z3)` again to find Z3 development files and set `Z3_INCLUDE_DIR`. While at it, handle the possibility that Z3 development package is no longer installed -- run the tests only if both LLVM has been built against Z3, and the headers are still available. llvm#145731 (comment) Signed-off-by: Michał Górny <mgorny@gentoo.org>

Fix running tests that require Z3 headers in standalone build. They were wrongly relying on `Z3_INCLUDE_DIR` being passed through from LLVM, which is not the case for a standalone build. Instead, perform `find_package(Z3)` again to find Z3 development files and set `Z3_INCLUDE_DIR`. While at it, handle the possibility that Z3 development package is no longer installed -- run the tests only if both LLVM has been built against Z3, and the headers are still available. #145731 (comment) Signed-off-by: Michał Górny <mgorny@gentoo.org>

…s (#146200) Fix running tests that require Z3 headers in standalone build. They were wrongly relying on `Z3_INCLUDE_DIR` being passed through from LLVM, which is not the case for a standalone build. Instead, perform `find_package(Z3)` again to find Z3 development files and set `Z3_INCLUDE_DIR`. While at it, handle the possibility that Z3 development package is no longer installed -- run the tests only if both LLVM has been built against Z3, and the headers are still available. llvm/llvm-project#145731 (comment) Signed-off-by: Michał Górny <mgorny@gentoo.org>

mgorny · 2025-06-28T11:35:05Z

Unfortunately, after fixing the immediate issue I'm hitting another issue: %host_cxx is compiling a 64-bit library when doing -m32 build for x86 — meaning the test run now fails due to ABI mismatch:

FAIL: Clang :: Analysis/z3-crosscheck-max-attempts.cpp (1537 of 21645)
******************** TEST 'Clang :: Analysis/z3-crosscheck-max-attempts.cpp' FAILED ********************
Exit Code: 1

Command Output (stderr):
--
/var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/clang -cc1 -internal-isystem /var/tmp/portage/llvm-core/
clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/../../../../lib/clang/21/include -nostdsysteminc -analyze -setup-static-analyzer -a
nalyzer-checker=debug.ConfigDumper 2>&1  | /usr/lib/llvm/21/bin/FileCheck /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/
Analysis/z3-crosscheck-max-attempts.cpp --match-full-lines # RUN: at line 2
+ /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/clang -cc1 -internal-isystem /var/tmp/portage/llvm-cor
e/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/../../../../lib/clang/21/include -nostdsysteminc -analyze -setup-static-analyzer 
-analyzer-checker=debug.ConfigDumper
+ /usr/lib/llvm/21/bin/FileCheck /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3-crosscheck-max-attempts.cpp -
-match-full-lines
rm -rf /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.t
mp && mkdir /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.
cpp.tmp # RUN: at line 6
+ rm -rf /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp
.tmp
+ mkdir /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.
tmp
/usr/lib/ccache/bin/x86_64-pc-linux-gnu-g++ -shared -fPIC -I /usr/include           /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/c
lang/test/Analysis/z3/Inputs/MockZ3_solver_check.cpp               -o /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x
86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.tmp/MockZ3_solver_check.so # RUN: at line 7
+ /usr/lib/ccache/bin/x86_64-pc-linux-gnu-g++ -shared -fPIC -I /usr/include /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/tes
t/Analysis/z3/Inputs/MockZ3_solver_check.cpp -o /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysi
s/Output/z3-crosscheck-max-attempts.cpp.tmp/MockZ3_solver_check.so
not /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/clang -cc1 -internal-isystem /var/tmp/portage/llvm-c
ore/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/../../../../lib/clang/21/include -nostdsysteminc -analyze -setup-static-analyze
r -analyzer-config crosscheck-with-z3-max-attempts-per-query=0 2>&1 | /usr/lib/llvm/21/bin/FileCheck /var/tmp/portage/llvm-core/clang-2
1.0.0.9999/work/clang/test/Analysis/z3-crosscheck-max-attempts.cpp --check-prefix=VERIFY-INVALID # RUN: at line 19
+ not /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/clang -cc1 -internal-isystem /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/../../../../lib/clang/21/include -nostdsysteminc -analyze -setup-static-analyzer -analyzer-config crosscheck-with-z3-max-attempts-per-query=0                                                                       
+ /usr/lib/llvm/21/bin/FileCheck /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3-crosscheck-max-attempts.cpp --check-prefix=VERIFY-INVALID                                                                                                           
Z3_SOLVER_RESULTS="UNDEF"             LD_PRELOAD="/var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.tmp/MockZ3_solver_check.so" /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/clang -cc1 -internal-isystem /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/../../../../lib/clang/21/include -nostdsysteminc /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3-crosscheck-max-attempts.cpp -analyze -setup-static-analyzer -analyzer-config crosscheck-with-z3=true -analyzer-checker=core -analyzer-config crosscheck-with-z3-max-attempts-per-query=1 -verify=refuted # RUN: at line 22                                                                              
+ Z3_SOLVER_RESULTS=UNDEF                                                                                                              
+ LD_PRELOAD=/var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.tmp/MockZ3_solver_check.so                                                                                                        
+ /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/clang -cc1 -internal-isystem /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/bin/../../../../lib/clang/21/include -nostdsysteminc /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3-crosscheck-max-attempts.cpp -analyze -setup-static-analyzer -analyzer-config crosscheck-with-z3=true -analyzer-checker=core -analyzer-config crosscheck-with-z3-max-attempts-per-query=1 -verify=refuted                             
ERROR: ld.so: object '/var/tmp/portage/llvm-core/clang-21.0.0.9999/work/x/y/clang-abi_x86_32.x86/test/Analysis/Output/z3-crosscheck-max-attempts.cpp.tmp/MockZ3_solver_check.so' from LD_PRELOAD cannot be preloaded (wrong ELF class: ELFCLASS64): ignored.                  
error: 'refuted-warning' diagnostics seen but not expected:                                                                            
  File /var/tmp/portage/llvm-core/clang-21.0.0.9999/work/clang/test/Analysis/z3-crosscheck-max-attempts.cpp Line 41: Division by zero [core.DivideZero]
1 error generated.

--

********************

mgorny · 2025-06-28T11:38:13Z

I'm going to try moving the shared object build into CMake.

steakhal · 2025-06-28T11:44:30Z

I dont think we should (or you) invest too much. We can just mark this special case with UNSUPPORTED and move on.

Is this issue caused by the standalone builds? We could detect and ignore the test in that case. Or we can do the opposite and allow the test only on a specific setup that is tested in the CI.

Note that in the past these tests were disabled before we recently enabled then. So i dont think it would count as regression if its unconditionally disabled.

mgorny · 2025-06-28T11:48:21Z

It's rather caused by doing a multilib build — in general you can't really use CMAKE_CXX_COMPILER outside CMake, since CMake is doing some toolchain magic on that, and you can't reproduce it right in lit. Unfortunately, I can't think of a good way of determining whether to run that, and I think actually switching to compile the library via CMake is easier — I'm already almost done, just need to wait for some free resources to start testing.

Apply a workaround to prevent non-native builds from detecting the Z3 development files, in order to skip the relevant tests. These tests attempt to compile a shared library using `CMAKE_CXX_COMPILER` passed down to lit, and they do not respect multilib flags, effectively causing an ABI mismatch. Bug: llvm/llvm-project#145731 (comment) Signed-off-by: Michał Górny <mgorny@gentoo.org>

Build the Z3 mock module via CMake rather than compiling it directly in tests. This ensures that the toolchain file is exported, and therefore fixes testing for Gentoo multilib. Also, it ensures that the module is compiled only once for the two tests using it. While at it, remove the related Z3 include directory and host compiler substitutions -- they are not used anymore, and the latter can't be reliably used in tests. The code is based on the existing bits for CTTestTidyModule. See llvm#145731 (comment)

mgorny · 2025-06-29T18:50:48Z

Okay, figured it out after all and filed #146284.

Build the Z3 mock module via CMake rather than compiling it directly in tests. This ensures that the toolchain file is exported, and therefore fixes testing for Gentoo multilib. Also, it ensures that the module is compiled only once for the two tests using it. While at it, remove the related Z3 include directory and host compiler substitutions -- they are not used anymore, and the latter can't be reliably used in tests. The code is based on the existing bits for CTTestTidyModule. See #145731 (comment)

Build the Z3 mock module via CMake rather than compiling it directly in tests. This ensures that the toolchain file is exported, and therefore fixes testing for Gentoo multilib. Also, it ensures that the module is compiled only once for the two tests using it. While at it, remove the related Z3 include directory and host compiler substitutions -- they are not used anymore, and the latter can't be reliably used in tests. The code is based on the existing bits for CTTestTidyModule. See llvm/llvm-project#145731 (comment)

…ode (llvm#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

) Fix running tests that require Z3 headers in standalone build. They were wrongly relying on `Z3_INCLUDE_DIR` being passed through from LLVM, which is not the case for a standalone build. Instead, perform `find_package(Z3)` again to find Z3 development files and set `Z3_INCLUDE_DIR`. While at it, handle the possibility that Z3 development package is no longer installed -- run the tests only if both LLVM has been built against Z3, and the headers are still available. llvm#145731 (comment) Signed-off-by: Michał Górny <mgorny@gentoo.org>

Build the Z3 mock module via CMake rather than compiling it directly in tests. This ensures that the toolchain file is exported, and therefore fixes testing for Gentoo multilib. Also, it ensures that the module is compiled only once for the two tests using it. While at it, remove the related Z3 include directory and host compiler substitutions -- they are not used anymore, and the latter can't be reliably used in tests. The code is based on the existing bits for CTTestTidyModule. See llvm#145731 (comment)

) Fix running tests that require Z3 headers in standalone build. They were wrongly relying on `Z3_INCLUDE_DIR` being passed through from LLVM, which is not the case for a standalone build. Instead, perform `find_package(Z3)` again to find Z3 development files and set `Z3_INCLUDE_DIR`. While at it, handle the possibility that Z3 development package is no longer installed -- run the tests only if both LLVM has been built against Z3, and the headers are still available. llvm#145731 (comment) Signed-off-by: Michał Górny <mgorny@gentoo.org>

Build the Z3 mock module via CMake rather than compiling it directly in tests. This ensures that the toolchain file is exported, and therefore fixes testing for Gentoo multilib. Also, it ensures that the module is compiled only once for the two tests using it. While at it, remove the related Z3 include directory and host compiler substitutions -- they are not used anymore, and the latter can't be reliably used in tests. The code is based on the existing bits for CTTestTidyModule. See llvm#145731 (comment)

NagyDonat requested review from necto, Xazax-hun, haoNoQ, gamesh411 and steakhal June 25, 2025 15:59

llvmbot added cmake Build system in general and CMake in particular clang Clang issues not falling into any other category clang:static analyzer llvm-lit testing-tools labels Jun 25, 2025

Revert accidentally pushed private tweak

a1df5dd

Satisfy darker code formatter

6e523ad

steakhal approved these changes Jun 25, 2025

View reviewed changes

clang/test/Analysis/reference.cpp Show resolved Hide resolved

clang/test/Analysis/reference.cpp Show resolved Hide resolved

necto approved these changes Jun 26, 2025

View reviewed changes

NagyDonat added 2 commits June 26, 2025 13:48

Put XFAIL on two badly broken tests

de69f78

Undo superfluous irrelevant change

8f6abb3

NagyDonat merged commit 40cc437 into llvm:main Jun 26, 2025
6 of 8 checks passed

NagyDonat mentioned this pull request Jun 27, 2025

[analyzer] Fix tests broken by empty %z3_include_dir #146042

Closed

mgorny mentioned this pull request Jun 28, 2025

[clang] Fix tests requiring Z3 headers in standalone builds #146200

Merged

mgorny mentioned this pull request Jun 29, 2025

[clang] Build the Z3 mock module via CMake #146284

Merged

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

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

Uh oh!

Conversation

NagyDonat commented Jun 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

llvmbot commented Jun 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

NagyDonat commented Jun 25, 2025

Uh oh!

steakhal commented Jun 25, 2025

Uh oh!

NagyDonat commented Jun 25, 2025

Uh oh!

steakhal left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

necto left a comment

Choose a reason for hiding this comment

Uh oh!

NagyDonat commented Jun 26, 2025

Uh oh!

Uh oh!

mgorny commented Jun 26, 2025

Uh oh!

steakhal commented Jun 26, 2025

Uh oh!

steakhal commented Jun 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

NagyDonat commented Jun 27, 2025

Uh oh!

NagyDonat commented Jun 27, 2025

Uh oh!

NagyDonat commented Jun 27, 2025

Uh oh!

mgorny commented Jun 27, 2025

Uh oh!

mgorny commented Jun 27, 2025

Uh oh!

NagyDonat commented Jun 27, 2025

Uh oh!

mgorny commented Jun 27, 2025

Uh oh!

NagyDonat commented Jun 27, 2025

Uh oh!

steakhal commented Jun 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mgorny commented Jun 27, 2025

Uh oh!

mgorny commented Jun 28, 2025

Uh oh!

mgorny commented Jun 28, 2025

Uh oh!

steakhal commented Jun 28, 2025

Uh oh!

mgorny commented Jun 28, 2025

Uh oh!

mgorny commented Jun 29, 2025

Uh oh!

Uh oh!

NagyDonat commented Jun 25, 2025 •

edited

Loading

llvmbot commented Jun 25, 2025 •

edited

Loading

github-actions bot commented Jun 25, 2025 •

edited

Loading

steakhal commented Jun 27, 2025 •

edited

Loading

steakhal commented Jun 27, 2025 •

edited

Loading