[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference

Balogh, Ádám via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Wed May 2 06:56:49 PDT 2018


baloghadamsoftware added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276
+      const llvm::APSInt &from = i->From(), &to = i->To();
+      const llvm::APSInt &newFrom = (to.isMinSignedValue() ?
+                                     BV.getMaxValue(to) :
+                                     (to.isMaxSignedValue() ?
+                                      BV.getMinValue(to) :
+                                      BV.getValue(- to)));
+      const llvm::APSInt &newTo = (from.isMinSignedValue() ?
----------------
NoQ wrote:
> Hmm, wait a minute, is this actually correct?
> 
> For the range [-2³¹, -2³¹ + 1] over a 32-bit integer, the negated range will be [-2³¹, -2³¹] U [2³¹ - 1, 2³¹ - 1].
> 
> So there must be a place in the code where we take one range and add two ranges.
The two ends of the range of the type usually stands for +/- infinity. If we add the minimum of the type when negating a negative range, then we lose the whole point of this transformation.

Example: If `A - B < 0`, then the range of `A - B` is `[-2³¹, -1]`, If we negate this, and keep the `-2³¹` range end, then we get `[-2³¹, -2³¹]U[1, 2³¹-1]`. However, this does not mean `B - A > 0`. If we make assumption about this, we get two states instead of one, in the true state `A - B`'s range is `[1, 2³¹-1]` and in the false state it is `[-2³¹, -2³¹]`. This is surely not what we want.


https://reviews.llvm.org/D35110





More information about the cfe-commits mailing list