[cfe-dev] [analyzer] ClangSA tests that 'REQUIRES: z3' won't run even if you have z3 installed

[Balázs Benics via cfe-dev]

There are multiple problems with the relevant code:
clang/test/Analysis/analyzer_test.py
<https://github.com/llvm/llvm-project/blob/master/clang/test/Analysis/analyzer_test.py#L18-L29>
```
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'))
```

1) If you watch closely, tests that 'REQUIRES: z3' won't run unless you
specify the undocumented USE_Z3_SOLVER=1 llvm-lit parameter.
So even if I have z3 installed, the corresponding test would still not run
- which is somewhat counter-intuitive.

2) Even if you additionally specify the magic flag, your tests would run,
except with the z3 based constraint manager (z3-CM) - so strictly speaking
- not your test configuration would run.
This is problematic if your test depends on the simplified (flawed)
behavior of the range-CM in certain situations.

3) If the test file does not require z3 but the USE_Z3_SOLVER is enabled.
First, the test file would be checked using the range-CM, and (assuming it
passed) checked again using the z3-CM.
There is some chance, that on a given test file, that the generated
exploded graph will be significantly different.
Due to these differences, we should not assume that the bugreports that are
expected in the test file would match with the actual reports in both cases.
This is especially problematic since this additional run was added by the
test suite rather than the test author.


Conclusion:
'REQUIRES: z3' should really mean whether you have clang built with z3 or
not. (in other words, you have z3 installed or not)
We should have some way (eg. another keyword?) specifying that this test
file can be run with z3-CM. (something like: ALSO_RUN_WITH_Z3_SOLVER)
In such files, all RUN commands should be executed normally, but also with
the z3-CM if z3 is available.

Since the z3-CM is really slow, it is reasonable to have some way to skip
such tests, but no more than necessary.
I assume, that USE_Z3_SOLVER tried to serve exactly this purpose.
Probably 'ALLOW_Z3_CONSTRAINT_MANAGER' would be a better name and we should
have some sort of documentation about this parameter.

If the test file requires z3 and contains run commands using only the
z3-CM, then that test should be categorized as UNSUPPORTED if
ALLOW_Z3_CONSTRAINT_MANAGER was not enabled.
Tests that require z3 but only for crosscheck, should run regardless of the
ALLOW_Z3_CONSTRAINT_MANAGER param.


By the same token, do we even have build bots using this USE_Z3_SOLVER lit
param?
Or even having z3 installed?

What are your thoughts about this?
Is this approach reasonable to you?


Let me know if I missed something.

Regards, Balazs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200709/af4248e3/attachment.html>