This is an archive of the discontinued LLVM Phabricator instance.

Return "[SCEV] Prove implicaitons via AddRec start"
ClosedPublic

Authored by mkazantsev on Sep 24 2020, 3:23 AM.

Details

Summary

If we know that some predicate is true for AddRec and an invariant
(w.r.t. this AddRec's loop), this fact is, in particular, true on the first
iteration. We can try to prove the facts we need using the start value.

The motivating example is proving things like

isImpliedCondOperands(>=, X, 0, {X,+,-1}, 0}

The initial version of the patch was reverted because it missed the check that
the predicate being proved is actually guarded by this check on 1st iteration.
If it was not executed on 1st iteration (but possibly executes after that), then
it is incorrect to use reasoning about IV start to prove it.

Added the test where the miscompile was seen. Unfortunately, my attempts
to reduce it with bugpoint did not succeed; it can further be reduced when
we understand how to do it without losing the initial bug's notion.

Diff Detail

Event Timeline

mkazantsev created this revision.Sep 24 2020, 3:23 AM
Herald added a project: Restricted Project. · View Herald TranscriptSep 24 2020, 3:23 AM
mkazantsev requested review of this revision.Sep 24 2020, 3:23 AM
mkazantsev added a reviewer: sanjoy.
reames requested changes to this revision.Sep 24 2020, 9:57 AM
reames added inline comments.
llvm/lib/Analysis/ScalarEvolution.cpp
9901

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.

This revision now requires changes to proceed.Sep 24 2020, 9:57 AM
mkazantsev added inline comments.Sep 24 2020, 9:02 PM
llvm/lib/Analysis/ScalarEvolution.cpp
9901

Do we need this for varying Y case?

mkazantsev planned changes to this revision.Sep 24 2020, 10:33 PM
mkazantsev added inline comments.
llvm/lib/Analysis/ScalarEvolution.cpp
9901

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

Ruled out "known after loop" case because it is something we do not want to deal with.

reames accepted this revision.Sep 28 2020, 9:31 AM

LGTM

I'd missed the subtlety with the context. I'm glad you caught that!

This revision is now accepted and ready to land.Sep 28 2020, 9:31 AM
This revision was automatically updated to reflect the committed changes.
mkazantsev reopened this revision.Oct 6 2020, 3:54 AM
This revision is now accepted and ready to land.Oct 6 2020, 3:54 AM
mkazantsev requested review of this revision.Oct 6 2020, 3:57 AM
mkazantsev updated this revision to Diff 296407.
mkazantsev retitled this revision from [SCEV] Prove implicaitons via AddRec start to Return "[SCEV] Prove implicaitons via AddRec start".
mkazantsev edited the summary of this revision. (Show Details)
mkazantsev added a reviewer: bkramer.
This revision was not accepted when it landed; it landed in state Needs Review.Oct 7 2020, 9:17 PM
This revision was automatically updated to reflect the committed changes.