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
===============================
lit - A Software Testing Tool
===============================
About
=====
*lit* is a portable tool for executing LLVM and Clang style test suites,
summarizing their results, and providing indication of failures. *lit* is
designed to be a lightweight testing tool with as simple a user interface as
possible.
Features
========
* Portable!
* Flexible test discovery.
* Parallel test execution.
* Support for multiple test formats and test suite designs.
Documentation
=============
The official *lit* documentation is in the man page, available online at the LLVM
Command Guide: http://llvm.org/cmds/lit.html.
Source
======
The *lit* source is available as part of LLVM, in the LLVM source repository:
https://github.com/llvm/llvm-project/tree/main/llvm/utils/lit
Contributing to lit
===================
Please browse the issues labeled *tools:llvm-lit* in LLVM's issue tracker for
ideas on what to work on:
https://github.com/llvm/llvm-project/labels/tools%3Allvm-lit
Before submitting patches, run the test suite to ensure nothing has regressed::
# From within your LLVM source directory.
utils/lit/lit.py \
--path /path/to/your/llvm/build/bin \
utils/lit/tests
Note that lit's tests depend on ``not`` and ``FileCheck``, LLVM utilities.
You will need to have built LLVM tools in order to run lit's test suite
successfully.
You'll also want to confirm that lit continues to work when testing LLVM.
Follow the instructions in http://llvm.org/docs/TestingGuide.html to run the
regression test suite:
make check-llvm
And be sure to run the llvm-lit wrapper script as well:
/path/to/your/llvm/build/bin/llvm-lit utils/lit/tests
Finally, make sure lit works when installed via setuptools:
python utils/lit/setup.py install
lit --path /path/to/your/llvm/build/bin utils/lit/tests