[PATCH] D37569: Rework loop predication pass

[Sanjoy Das via Phabricator via llvm-commits]

sanjoy accepted this revision.
sanjoy added a comment.
This revision is now accepted and ready to land.

I did not check the actual code changes carefully -- I've assumed they're in sync with the comments -- but let me know if you want me to take a look.  The comments and the math bits LGTM.



================
Comment at: lib/Transforms/Scalar/LoopPredication.cpp:38
+// It's tempting to rely on SCEV here, but it has proven to be problematic.
+// Generally the facts SCEV provides are true if the backedge of the loop is
+// taken, which implicitly assumes that the guard doesn't fail. Using these
----------------
I think we should be clearer here:  the facts that SCEV proves about the *increment step* of add recurrences are true if the backedge of the loop is taken


================
Comment at: lib/Transforms/Scalar/LoopPredication.cpp:75
+//
+// One solution for M is M = forall X . (G(X) && B(X + S)) => G(X + S)
+//
----------------
Can you please add a short inductive informal proof on why this is sufficient?  You should also state that `M` or anything "stronger" (i.e. any condition that implies `M`) will do.


================
Comment at: lib/Transforms/Scalar/LoopPredication.cpp:110
+//   latchLimit s<= guardLimit.
+//
+// So the widened condition is:
----------------
I would append this to make things 100% clear:

"""
In other words, if latchLimit s<= guardLimit then (the ranges below are written in ConstantRange notation, where `[A, B)` is the set `for (I = A; I != B; I++ /*maywrap*/) yield(I);`):

```
   forall X . X u< guardLimit && (X + 1) s< latchLimit =>  (X + 1) u< guardLimit
== forall X . X u< guardLimit && (X + 1) s< guardLimit =>  (X + 1) u< guardLimit
== forall X . X in [0, guardLimit) && (X + 1) in [INT_MIN, guardLimit) =>  (X + 1) in [0, guardLimit)
== forall X . X in [0, guardLimit) && X in [INT_MAX, guardLimit-1) =>  X in [-1, guardLimit-1)
== forall X . X in [0, guardLimit-1) => X in [-1, guardLimit-1)
== true
```
"""



================
Comment at: lib/Transforms/Scalar/LoopPredication.cpp:397
+  }
+  assert(((TrueDest == L->getHeader()) || (FalseDest == L->getHeader())) &&
+         "One of the latch's destinations must be the header");
----------------
I don't think you need parens around `A == B`.


Repository:
  rL LLVM

https://reviews.llvm.org/D37569