[PATCH] D88208: [SCEV] Prove implicaitons via AddRec start

[Max Kazantsev via Phabricator via llvm-commits]

mkazantsev planned changes to this revision.
mkazantsev added inline comments.


================
Comment at: llvm/lib/Analysis/ScalarEvolution.cpp:9892
+    const SCEV *FoundLHS, const SCEV *FoundRHS) {
+  // {X,+,1} < Y implies X < Y, and {X,+,-1} > Y implies X > Y.
+  // {X,+,C} != Y implies X != Y and {X,+,C} == Y implies X == Y if Y is a
----------------
mkazantsev wrote:
> reames wrote:
> > If Y is loop invariant, this obviously follows.  And the more general form of (X,+,W) < Y ==> X < Y would also hold.
> > 
> > I'm struggling to convince myself this holds when Y is an arbitrary loop varying scev.  I haven't found a counter example yet.
> > 
> > Could I ask you to split this into two patches?  One for the invariant case since that's easy to reason about, and one for the varying Y case?  I both want to think about that separately and have an easy patch to revert if needed.
> Do we need this for varying Y case?
I just realized my code for NE and EQ is wrong.

Actually, there are two conceptually different cases here I want to emphasize. 

The `isImpliedCondOperandsViaAddRecStart(Pred, X, RHS, {X,+,W}, Y)` (Y is a loop invariant) actually means two different things depending on the context.

If we query it in the loop, the known fact `{X,+,W} Pred Y` is true for IV on every iteration, in particular on the first iteration. So we can trivially make this descent.

If we query it *after* the loop, then the known fact `{X,+,W} Pred Y`  means the following: after the loop has ended and the final value of this IndVar is computed, this predicate is true for this final value.

If we know that the IndVar was strictly reducing/increasing (steps 1/-1), then we can still make this transit: `{X,+,-1} > Y` on the first iteration and went down, but even on the last iteration it is still greater than Y. The fact that it was stronger than Y on the first iteration is even a stronger fact, but if it's enough then fine.

But this does not hold for NE.

Actually I do not want to deal with "queried after loop" at all. The logic there is too flacky. What I really want is that this fact is known in loop. I think this code should be in "isKnownOnEveryIteration".


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

https://reviews.llvm.org/D88208