[PATCH] D35109: [Analyzer] SValBuilder Comparison Rearrangement

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In https://reviews.llvm.org/D35109#837723, @NoQ wrote:

> It's something similar to assuming that the string length is within range [0, INT_MAX/4] in CStringChecker: we can easily assume that no overflow is happening in computations involving string lengths or iterator positions, but not on generic integers. Which lead me to believing that we could maintain a no-overflow variant of evalBinOp (questionable).
>
> Would anything go wrong if we only enable this code when both symbols are known to be within range [-max/4, max/4]? And in the checker, add the respective assumption. I believe it's a very clear way to express that no overflow is happening. In fact, in the program state we can add an API `ProgramStateRef assumeNoOverflow(SVal, QualType)`, which tries to assume that the value is within range [-max/4, max/4] for signed types or [0, max/4] for unsigned types (and fails when such assumption is known be violated), so that to avoid duplicating similar trick in every checker.


I had a quick look into actually implementing this solution, and i generally liked how it looks. Instead of the checker saying "I know that these symbols won't overflow on any operations, so let me do whatever I want", it says "I know that these symbols are small" and the core handles the rest.

I managed to get this patch and https://reviews.llvm.org/D35110 and https://reviews.llvm.org/D32642 running on top of my solution in a fairly straightforward manner. I did not see if there is any impact on performance; if there is, in the worst case we may want to expose the "unsafe" functions to the checkers to optimize out repeated checks. A bit of cleanup may be necessary after me (eg. turn static functions into methods where appropriate).

Unsigned integers are not supported, because their overflows are harder to avoid; however, as far as i understand you are only interested in signed integers. For signed integers, rearrangement only kicks in when all symbols and concrete integers are of the same type `T` and are constrained within `[-max/4, max/4]`, where `max` is the maximum value of `T`.

Here are my patches:

- On top of https://reviews.llvm.org/D35109: F5459988: Max4Rearrangements.patch <https://reviews.llvm.org/F5459988>
- On top of https://reviews.llvm.org/D35110: F5459990: Max4Negations.patch <https://reviews.llvm.org/F5459990>
- On top of https://reviews.llvm.org/D35110: F5459991: Max4Iterators.patch <https://reviews.llvm.org/F5459991>

All tests should pass when all 6 patches are applied.

Could you see if this works for you?


https://reviews.llvm.org/D35109