NoQ 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() ? ---------------- baloghadamsoftware wrote: > 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. Well, we can't turn math into something we want, it is what it is. Iterator-related symbols are all planned to be within range [-2²⁹, -2²⁹], right? So if we subtract one such symbol from another, it's going to be in range [-2³⁰, 2³⁰]. Can we currently infer that? Or maybe we should make the iterator checker to enforce that separately? Because this range doesn't include -2³¹, so we won't have any problems with doing negation correctly. So as usual i propose to get this code mathematically correct and then see if we can ensure correct behavior by enforcing reasonable constraints on our symbols. https://reviews.llvm.org/D35110 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
