[PATCH] D106331: [ScalarEvolution] Try harder to prove overflow in howManyLessThans.

[Philip Reames via Phabricator via llvm-commits]

reames requested changes to this revision.
reames added a comment.
This revision now requires changes to proceed.

Not really a fan of the structure of this change.  Bear with me as I talk through a couple of approaches (only the last of which may work.)

Let me throw out an approach for this in terms of SCEVs.  I'm going to use the variable names from foo1 in trip-count-unknown-stride.ll to make this understandable.
%i.05 = {0, +, %s}
%add = {0 + %s, +, %s}

The condition we need to prove is that (0 + %s - %s < 0 + %s.  (Remember that the start here is in terms of %add, not %i.05.)

One tactic would be to prove (0 - %s) < 0.  (i.e. cancel %s on either side - we don't care whether the addition of %s would wrap in that step.)  This reduces to proving %s > 0.  This is interesting as we already have a framework for proving strides positive.  Maybe we can extend that?

Interestingly, we can do that with SCEV.  Consider the following code:

  if (!PositiveStride) {
    if (IsSigned && NoWrap &&
        isLoopInvariant(RHS, L) && IV->getStart() == Stride &&
        isLoopEntryGuardedByCond(L, Cond, getZero(RHS->getType()), RHS) && 
        loopIsFiniteByAssumption(L))
      PositiveStride = true;
  }

I'd written this for another purpose which didn't work out, but I think the structure is valid.  This is maybe too specific for a zero start on i.05 - though maybe we can generalize?

Anyways, that isn't a fully solution, but I'd strongly prefer you try to use a SCEV proof here over mixing IR and SCEV proofs.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D106331