[PATCH] D105216: [ScalarEvolution] Fix overflow in computeBECount.

[Eli Friedman via Phabricator via llvm-commits]

efriedma added a comment.

In D105216#2874452 <https://reviews.llvm.org/D105216#2874452>, @reames wrote:

> In D105216#2872827 <https://reviews.llvm.org/D105216#2872827>, @efriedma wrote:
>
>>> but I *strongly* request you look for ways to factor the code so that the reasoning is modular
>>
>> I really don't see any way to unify the two different proof strategies.  The proofs are trying to reason about overflow on completely different operations.
>
> So, I think this might be part of our problem.  The code and comments to date have not made your last sentence here obvious to me as the reviewer.
>
> To be clear, I have not seen a concise description of what the bug in the original patch *was*.  That makes it hard to review a patch which is supposed to fix it.

Oh, sorry, I thought you understood the issue since you sort of pointed it out originally.  The issue is the case where `End < Start`.

If we prove `RHS >= Start`, this is impossible.  If we use `End = max(RHS, Start)`, this is also impossible.  If we only proved `RHS > Start - Stride`, it's possible that `Start - Stride < End < Start`.  In this case, the backedge-taken count should be zero.  But `RHS - Start` overflows, so getUDivCeilSCEV treats it as a very large positive number.

So we never want to use getUDivCeilSCEV if we're optimizing an expression by proving `RHS > Start - Stride`.  As I outline in the proof in this patch, in this case, we can show that the backedge-taken count is actually `((RHS - 1) - (Start - Stride)) /u Stride`, which is equivalent to the expression we would produce without this patch.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D105216