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