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

[Gábor Horváth via cfe-dev]

As far as I remember, the tests using Z3 are behind a flag due to testing
time concerns. That being said I think none of the build bots are using the
Z3 configuration which is bad (hopefully someone will correct me if I am
wrong).
Moreover, I think to expect all the tests to give the same results
regardless of the constraint solver used might be wishful thinking, and
rerunning the whole test suite with multiple solvers would result in
surprising build bot failures for analyzer devs.

I think it would be great to have at least some z3 specific tests in the
test suite even when USE_Z3_SOLVER is set to false. Is this not the case at
the moment?

Maybe USE_Z3_SOLVER should be renamed to RECHECK_WITH_Z3_SOLVER and mean
that every RUN line will be invoked twice with all the constraint manager
and let the tests use Z3 when this option is false.
We should decide if we want the test suite to be independent of the solver
used and either set up a build bot to enforce this or maybe even make
RECHECK_WITH_Z3_SOLVER a debugging tool and document it as such.

What do you think?

Cheers,
Gabor

On Thu, 9 Jul 2020 at 18:55, Balázs Benics via cfe-dev <
cfe-dev at lists.llvm.org> wrote:

> 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
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200709/d9836061/attachment-0001.html>