[PATCH] D17174: [LVI] Greatly strengthen inductive reasoning on predicates

[Sanjoy Das via llvm-commits]

sanjoy added a comment.

In http://reviews.llvm.org/D17174#363158, @reames wrote:

> In http://reviews.llvm.org/D17174#359356, @sanjoy wrote:
>
> > The difference is in `LVI Getting edge value   %iv.next = add i32 %iv, 1 from 'loop' to 'backedge'`.  **However** I am yet to make this "regression" result in a missed transform; so it is very possible that there is an invariant on why the above difference does not matter by construction.  Is that the case?
> >
> > I think you had explained this to me in person before, but putting this in writing will both help me remember what we decided, and is also good for record.
>




> It is possible for this patch to cause a regression in result

>  quality in some rare cases.  The tradeoff is that we're able to catch

>  other cases which are much more common in practice.


What are those cases?  Is there a reason why they would be rarer in
practice?  I'm okay making a tradeoff, as long as we know what the
tradeoff is.

> Looking at your *particular* example, I think you've just found an

>  unrelated bug in LVI.  In particular, we've computed a tight bound for

>  the phi, but for some reason don't use that for the next step of the

>  unwinding analysis.  That's more than a bit strange.




> The only way I know handle the general case without regressions is

>  the double iteration scheme I mentioned in my description.  If we

>  stopped when encountering not the first node in the cycle, but the

>  last node in the cycle (i.e. before pushing any value three times).


Why would that scheme handle all cases?  IOW, why is visiting every
value in the cycle twice enough (and not weaker then pushing every
value in teh cycle thrice)?


http://reviews.llvm.org/D17174