[all-commits] [llvm/llvm-project] 40cc43: [NFC][analyzer] Remove Z3-as-constraint-manager ha...

[Donát Nagy via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 40cc4379cda6e0d6efe72c55d1968f9cf427a16a
      https://github.com/llvm/llvm-project/commit/40cc4379cda6e0d6efe72c55d1968f9cf427a16a
  Author: Donát Nagy <donat.nagy at ericsson.com>
  Date:   2025-06-26 (Thu, 26 Jun 2025)

  Changed paths:
    M clang/docs/analyzer/developer-docs/DebugChecks.rst
    M clang/test/Analysis/PR37855.c
    R clang/test/Analysis/analyzer_test.py
    M clang/test/Analysis/bool-assignment.c
    M clang/test/Analysis/cstring-addrspace.c
    M clang/test/Analysis/lit.local.cfg
    M clang/test/Analysis/ptr-arith.c
    M clang/test/Analysis/reference.cpp
    M clang/test/Analysis/unary-sym-expr-z3-refutation.c
    M clang/test/Analysis/z3-crosscheck-max-attempts.cpp
    M clang/test/Analysis/z3-crosscheck.c
    M clang/test/Analysis/z3/D83660.c
    M clang/test/Analysis/z3/crosscheck-statistics.c
    R clang/test/Analysis/z3/enabled.c
    M clang/test/CMakeLists.txt
    M clang/test/lit.cfg.py
    M clang/test/lit.site.cfg.py.in
    M llvm/utils/gn/secondary/clang/test/BUILD.gn
    M llvm/utils/lit/lit/llvm/config.py

  Log Message:
  -----------
  [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



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications