<div dir="ltr"><div>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).</div><div>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.</div><div><br></div><div>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?</div><div><br></div><div>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.</div><div>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.</div><div><br></div><div>What do you think?<br></div><div><br></div><div>Cheers,</div><div>Gabor<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 9 Jul 2020 at 18:55, Balázs Benics via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">There are multiple problems with the relevant code:<br><a href="https://github.com/llvm/llvm-project/blob/master/clang/test/Analysis/analyzer_test.py#L18-L29" target="_blank">clang/test/Analysis/analyzer_test.py</a><br><span style="font-family:monospace">```<br>if 'z3' not in test.requires:<br> results.append(self.executeWithAnalyzeSubstitution(<br> saved_test, litConfig, '-analyzer-constraints=range'))<br><br> if results[-1].code == lit.Test.FAIL:<br> return results[-1]<br><br># If z3 backend available, add an additional run line for it<br>if self.use_z3_solver == '1':<br> assert(test.config.clang_staticanalyzer_z3 == '1')<br> results.append(self.executeWithAnalyzeSubstitution(<br> saved_test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3'))<br>```</span><br><br>1) If you watch closely, tests that 'REQUIRES: z3' won't run unless you specify the undocumented USE_Z3_SOLVER=1 llvm-lit parameter.<br>So even if I have z3 installed, the corresponding test would still not run - which is somewhat counter-intuitive.<br><br>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.<br>This is problematic if your test depends on the simplified (flawed) behavior of the range-CM in certain situations.<br><br>3) If the test file does not require z3 but the USE_Z3_SOLVER is enabled.<br>First, the test file would be checked using the range-CM, and (assuming it passed) checked again using the z3-CM.<br>There is some chance, that on a given test file, that the generated exploded graph will be significantly different.<br>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.<br>This is especially problematic since this additional run was added by the test suite rather than the test author.<br><br><br>Conclusion:<br>'REQUIRES: z3' should really mean whether you have clang built with z3 or not. (in other words, you have z3 installed or not)<br>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)<br>In such files, all RUN commands should be executed normally, but also with the z3-CM if z3 is available.<br><br>Since the z3-CM is really slow, it is reasonable to have some way to skip such tests, but no more than necessary.<br>I assume, that USE_Z3_SOLVER tried to serve exactly this purpose.<br>Probably 'ALLOW_Z3_CONSTRAINT_MANAGER' would be a better name and we should have some sort of documentation about this parameter.<br><br>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.<br>Tests that require z3 but only for crosscheck, should run regardless of the ALLOW_Z3_CONSTRAINT_MANAGER param.<br><br><br>By the same token, do we even have build bots using this USE_Z3_SOLVER lit param?<br>Or even having z3 installed?<br><br>What are your thoughts about this?<br>Is this approach reasonable to you?<br><br><br>Let me know if I missed something.<br><br>Regards, Balazs<br></div>
_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
</blockquote></div></div>