[PATCH] D106852: [SCEV] Fix getAddExpr for adding loop invariants into start of some AddRec

[Eli Friedman via Phabricator via llvm-commits]

efriedma added a comment.

In D106852#2924428 <https://reviews.llvm.org/D106852#2924428>, @mkazantsev wrote:

>> The problem here is that we're splitting the add into pieces. a+b+1 being nsw doesn't necessarily imply that a+1 is nsw in all contexts; the nsw only applies in contexts where b is defined. This is a little subtle, but it's the only interpretation that's consistent with some of the ways we try to prove nsw flags.
>
> I think this is a self-contradictory interpretation. What if we instead computed `a+b+1-b <nsw>` and then decided to simplify `b` away, getting `a+1<nsw>`

a+1 wouldn't be nsw?  And in fact, that's what getAddExpr currently does.  I don't see how that's a contradiction.

If we say that `a+b+1-b <nsw>` implies `a+1<nsw>`, and similarly say `({a,+,1} + b)<nsw>` implies `(a+b)<nsw>`, that leads to a consistent system, I think.  But that would imply the bug here isn't in getAddExpr at all; instead, getNoWrapFlagsFromUB() is fundamentally broken.


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

https://reviews.llvm.org/D106852