[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

[Manas Gupta via Phabricator via cfe-commits]

manas added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1411
+    if ((LHS.From() < 0 && RHS.From() < 0)) {
+      llvm::APSInt CrucialPoint = Tmin - LHS.From();
+      if (RHS.Includes(CrucialPoint)) {
----------------
vsavchenko wrote:
> What if `LHS.From()` is `Tmin` for signed `T`?
> What if `T` is unsigned?  Does `Tmin - LHS.From()` (aka `0 - LHS.From()`) make sense?
Even if `LHS.From()` is `Tmin` for signed `T` the reasoning would be correct. As, CrucialPoint will be `Zero` and hence RHS will be divided into two parts: BeforeZero (`[RHS.From, Zero]`) and AfterAndIncludingZero (`[Zero, RHS.To]`).

And if the BeforeZero subrange (which will be responsible for overflowing, contains `Tmin + Tmax` then we can ensure that the final range will be `[Tmin, Tmax]`. And if it does not, (and assuming there is no overflow on the right side), then `1432:1434` will reason the range to be `[Tmin, Max] U [Min, Tmax]`.

For unsigned types, actually we are asking the wrong question because an addition of unsigned integers can never overflow from the left side. So in that case, the code deducing the overflows from left-side will not be applicable. And therefore, `0 - LHS.From()` will never give us anything. I was thinking to checked T before applying these rules.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1448-1451
+  if ((LHS.From() > 0 && RHS.From() > 0 && Min < 0) ||
+      (LHS.From() < 0 && RHS.From() < 0 && Min > 0) ||
+      (LHS.To() > 0 && RHS.To() > 0 && Max < 0) ||
+      (LHS.To() < 0 && RHS.To() < 0 && Max > 0)) {
----------------
vsavchenko wrote:
> Speaking of unsigned `T`, does it work for unsigned overflows?  Do we have tests for that?
This was not going to make into the patch as it does not solve the case mentioned in FIXME(:1437).

An idea which I had in the previous post was this:

> 1. If one of Min/Max overflows while the other doesn't then the resulting range should be [Tmin, Tmax] as Min <= Max even after overflowing.
> 2. If both of them overflows, then: a. If both overflows on the same side, that is, both wrapped around Tmax, or both wrapped around Tmin, then the range should be [Min, Max] only. b. But if both overflowed in different sides, supposedly Min overflowed on left and Max on right, or vice versa, then the range will be [Tmin, Tmax].



Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103440