[PATCH] D83677: [analyzer] Rework Z3 requirements in the CSA testsuite

[Balázs Benics via Phabricator via llvm-commits]

steakhal marked 4 inline comments as done.
steakhal added a comment.

In D83677#2148435 <https://reviews.llvm.org/D83677#2148435>, @NoQ wrote:

> [...] It looks like you are planning to actively support Z3 as a //constraint manager//. [...] Did you consider my usual suggestion to only apply it to refuting non-buggy states in order to combat your false negatives similarly to how our current Z3 refutation refutes buggy states to combat false positives?


I don't plan to invest time to support Z3-CM.

Although, I highly value the refutation infrastructure. TBH this patch focused fixing the test-infra to be able to have tests //explicitly// testing refutation related warnings.
Please note that previously you could **not** `require z3` and //only// run the test using the //range-CM//. Using also the `Z3-CM` would not emit warning for that case, making the test fail.
Besides fixing this (which was my primary object), adds new `ToolSubst`s in a backward-compatible manner to let the test author specify explicitly the CM of their choice.



================
Comment at: clang/www/analyzer/checker_dev_manual.html:534
     <pre class="code">
     $ <b>bin/llvm-lit -sv ../llvm/tools/clang/test/Analysis</b>
     </pre>
----------------
NoQ wrote:
> Yeah, just delete this :)
Is the `ninja check-clang-analysis` the prefered way running the test?
I will reword the doc then.


================
Comment at: llvm/utils/lit/lit/llvm/config.py:412-413
             ToolSubst('%clang', command=self.config.clang, extra_args=additional_flags),
-            ToolSubst('%clang_analyze_cc1', command='%clang_cc1', extra_args=['-analyze', '%analyze', '-setup-static-analyzer']+additional_flags),
+            ToolSubst('%clang_analyze_cc1_range', command='%clang_cc1', extra_args=['-analyze', '-analyzer-constraints=range', '-setup-static-analyzer']+additional_flags),
+            ToolSubst('%clang_analyze_cc1_z3', command='%clang_cc1', extra_args=['-analyze', '-analyzer-constraints=z3', '-setup-static-analyzer']+additional_flags),
+            ToolSubst('%clang_analyze_cc1', command='%clang_cc1', extra_args=['-analyze', '%constraint_manager', '-setup-static-analyzer']+additional_flags),
----------------
NoQ wrote:
> I'm for longer names, "range" is too vague, "z3" is already ambiguous (does it mean as constraint manager or for refutation?).
> 
> `%clang_analyze_cc1_range_cm_only` would probably make more sense. It also looks more like a FIXME and tells that something's wrong with the test.
> I'm for longer names, "range" is too vague, "z3" is already ambiguous (does it mean as constraint manager or for refutation?).
If we don't expect the clangSA dev to be able to differentiate, why should we expect them to know what 'cm' means there?
I'm not against longer names, but kinda hard to strike the balance for finding short but descriptive names.

A lengthy `ToolSubst` would consume most of the available space in the line, rendering most of the RUN commands to span across multiple lines. 

> [...] It also looks more like a FIXME and tells that something's wrong with the test.
I don't think that should be suspicious.
I wouldn't assume that test is wrong, simply that test works only with the range-CM.


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D83677/new/

https://reviews.llvm.org/D83677