[clang] 40cc437 - [NFC][analyzer] Remove Z3-as-constraint-manager hacks from lit test code (#145731)
via cfe-commits
cfe-commits at lists.llvm.org
Thu Jun 26 05:19:34 PDT 2025
Author: Donát Nagy
Date: 2025-06-26T14:19:30+02:00
New Revision: 40cc4379cda6e0d6efe72c55d1968f9cf427a16a
URL: https://github.com/llvm/llvm-project/commit/40cc4379cda6e0d6efe72c55d1968f9cf427a16a
DIFF: https://github.com/llvm/llvm-project/commit/40cc4379cda6e0d6efe72c55d1968f9cf427a16a.diff
LOG: [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
Added:
Modified:
clang/docs/analyzer/developer-docs/DebugChecks.rst
clang/test/Analysis/PR37855.c
clang/test/Analysis/bool-assignment.c
clang/test/Analysis/cstring-addrspace.c
clang/test/Analysis/lit.local.cfg
clang/test/Analysis/ptr-arith.c
clang/test/Analysis/reference.cpp
clang/test/Analysis/unary-sym-expr-z3-refutation.c
clang/test/Analysis/z3-crosscheck-max-attempts.cpp
clang/test/Analysis/z3-crosscheck.c
clang/test/Analysis/z3/D83660.c
clang/test/Analysis/z3/crosscheck-statistics.c
clang/test/CMakeLists.txt
clang/test/lit.cfg.py
clang/test/lit.site.cfg.py.in
llvm/utils/gn/secondary/clang/test/BUILD.gn
llvm/utils/lit/lit/llvm/config.py
Removed:
clang/test/Analysis/analyzer_test.py
clang/test/Analysis/z3/enabled.c
################################################################################
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/PR37855.c b/clang/test/Analysis/PR37855.c
index e9c2564ba008a..e08ce8f250f86 100644
--- a/clang/test/Analysis/PR37855.c
+++ b/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 {
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, ptr
diff _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 at -1{{garbage}}
+ // expected-warning at -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..bd447d33f8c5d 100644
--- a/clang/test/Analysis/z3-crosscheck.c
+++ b/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 at -1{{garbage}}
+ // expected-warning at -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 at -1{{garbage}}
+ // expected-warning at -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..0a7c8bab8e345 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
//
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 at 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..24bcdb5b668fc 100644
--- a/clang/test/lit.cfg.py
+++ b/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")
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/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(
More information about the cfe-commits
mailing list