[PATCH] D103096: [analyzer] Implement cast for ranges of symbolic integers.

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In D103096#2789439 <https://reviews.llvm.org/D103096#2789439>, @ASDenysPetrov wrote:

> @NoQ
> This solution only intends to make correct calculations whenever cast occures. We can mark this as //alpha// or add an argument flag to turn cast reasoning on/off, or we can even disable any part of this patch with argument settings.

That would be awesome. I think we should land this patch under an `-analyzer-config` flag. This will allow us to experiment with viability of enabling cast symbols at any time as we improve the constraint solver. Additionally, presence of cast symbols is extremely valuable for z3 runs in which our concerns for increased complexity are eliminated.

>> But this still requires //massive// testing, a lot more than a typical constraint solver patch; extraordinary claims require extraordinary evidence.
>
> What kind of tests do you think we need?

Test on a lot of real-world code. Like, seriously, *A LOT* of real-world code. Say, 20x the amount of code we have in docker and csa-testbench, from a large variety of projects. Investigate newly appeared reports carefully to understand the impact. I'll be happy to help with this at some point.

>> With `SymbolCast`s in place our equations become much more complicated and therefore the constraint solver becomes much more likely to produce false positives in cases where it previously erred on the side of false negatives.
>>
>> Another thing to test is our ability to explain bug paths.
>
> My proposition is to design and describe a paper of:
>
> - what cases shall be considered as erroneous and be reported;
> - what cases shall be ignored or considered as exceptions (i.e. static_cast);
> - what wordings shall we use in reports;
> - how paths of those reports shall look like;
> - //your options;//

I think we should start from examples. While testing on real-world code, find poorly explained reports and see what piece of information is missing and preventing the user from understanding the warning. Then add that piece of information.

>> But in practice there may be other reasons to use a larger integer type, such as API requirements (eg., how `isascii()` accepts an `int` but only uses 266 values).
>
> IMO this is great when we tell user that he/she should make sure of the value bounds before passing the arguments to such APIs.

I'm thinking about warnings inside the //implementations// of such APIs.

>> There's also the usual problem of overflow being impossible specifically on the current path; in this case we have to make sure that an appropriate `assert()` would actually suppress the warning (i.e., the constraint solver would be able to correctly solve the assert condition as well).
>
> For example, this test easily passes.
>
>   void test(int x) {
>     assert(0 < x && x < 42);
>     char c = x;
>     clang_analyzer_eval(c <= 0); // expected-warning {{FALSE}}
>     clang_analyzer_eval(c >= 42); // expected-warning {{FALSE}}
>   }
>
> Or you meant some other cases?

I meant real-world examples. We should see if it works on real-world code where constraints are significantly more complex.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103096