There are multiple problems with the relevant code:
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'))
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.
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.
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.
‘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.