[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.

A SCEV add being marked nsw means, essentially, that at any point in the IR where all the operands are defined, the add doesn't wrap.

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.

(The definition point for a SCEV is either the point of definition for a SCEVUnknown, or the beginning of the loop header of an AddRec.)

But we can extend the logic a little.  If a+1 is nsw in contexts where b is defined, it's also nsw in any context that must eventually flow to the definition of b.  If the definition of a is such a context, a+1 is always nsw.

So, for example, if "a" is an addrec for a loop, and "b" is an addrec for a loop nested inside the first loop, and the control flow is simple, nsw on "a+b+1" implies nsw for "a+1".  Abnormal exits break this sort of proof, though: we assumed control must eventually flow to b's loop header.


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

https://reviews.llvm.org/D106852