[PATCH] D35109: [Analyzer] SValBuilder Comparison Rearrangement

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In https://reviews.llvm.org/D35109#837673, @zaks.anna wrote:

> > What do you suggest? Should we widen the type of the difference, or abandon this patch and revert back to the local solution I originally used in the iterator checker?
>
> Does the local solution you used in the iterator checker not have the same problem?


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.


https://reviews.llvm.org/D35109