[ScalarEvolution] Fix overflow in computeBECount.

[efriedma]

Summary

The current implementation of computeBECount doesn't account for the possibility that adding "Stride - 1" to Delta might overflow. For almost all loops, it doesn't, but it's not actually proven anywhere.

To deal with this, use a variety of tricks to try to prove that the addition doesn't overflow. If the proof is impossible, use an alternate sequence which never overflows.

[reames]

I'm working on a very similar patch as we speak, so you found a knowledgeable reviewer. Your test diff is a lot smaller than my current one, so maybe you're on to something. Unfortunately, I'm about to leave for the day, so I won't be able to get you detailed feedback until at least tomorrow.

A couple of quick comments.

The code does disallow stride == 0 on the howManyLessThans path. The logic is explained in the !PositiveStride path, but the comments are really confusing, so let me explain again. For a non-positive exit, we require that this be the sole exit and the current condition control that exit. (Indirectly through NoWrap) As a result, if the stride was zero, then the loop must either a) be infinite, or b) exit on the first iteration. The !loopIsFiniteByAssumption check requires a zero stride to exit on the first iteration. (Ah, I think I see the issue you did now. The stride can be zero iff the exit is taken on first iteration. If this was your chain of thought, can you clarify submission comment?)

llvm/lib/Analysis/ScalarEvolution.cpp

11600

Style comment: I'd suggest pulling out a function getUDivCeiling(Delta,Stride,MayOverflow). I found (in my WIP patch) that this really helps readability. Once you have that, you can use early return via tail call to helper for most of the above.

[reames]

llvm/lib/Analysis/ScalarEvolution.cpp

11609

While true, this is the same set of facts which allowed you to avoid the max for the start expression. As such, you've already gotten most of the benefit.

11711

This check needs removed. The problem is that this isn't doing what the comment says it is.

The actual condition to prove the backedge is taken on the first iteration is OrigStart Cond OrigRHS.

I have a test case which this check causes us to generate wrong code because Start-Stride < RHS, but Start < RHS does not hold. (Actually, what happened to that test case? I thought I'd committed that, but I don't see it in my commit history. Need to find that.)

When I tried removing this without also fixing the overflow issue, I got bad results. I don't fully remember why atm, will try to reconstruct that and share it.

[efriedma]

In D105216#2851010, @reames wrote:

Your test diff is a lot smaller than my current one, so maybe you're on to something.

I found that I needed a wide variety of heuristics to handle various cases in the regression tests. This is the source of most of the complexity in this patch.

(Ah, I think I see the issue you did now. The stride can be zero iff the exit is taken on first iteration. If this was your chain of thought, can you clarify submission comment?)

I'll clarify the commit message, sure.

llvm/lib/Analysis/ScalarEvolution.cpp

11600

Hmm...

Maybe I'll just make the computation of MayOverflow a lambda.

11711

Okay. We can deal with this separately, I think?

[efriedma]

Address review comments.

[mkazantsev]

How much worse does it become if we simply check that start <= MAX_INT - step and bail if we can't prove it?

llvm/include/llvm/Analysis/ScalarEvolution.h

2045

I feel it a bit confusing to pass end before start. Reverse order maybe?

[efriedma]

In D105216#2858946, @mkazantsev wrote:

How much worse does it become if we simply check that start <= MAX_INT - step and bail if we can't prove it?

I assume that isn't the expression you meant to write?

Practically, I expect the most important cases to recognize are:

1. Power-of-two stride.
2. Post-increment loops: Start == Stride. (This is a special case of Start >= Stride - 1).

I'm not sure how well isLoopEntryGuardedByCond/isKnownViaNonRecursiveReasoning would do if I just throw Start >= Stride - 1 for unsigned, or the signed equivalent, at it. I can try, I guess.

[reames]

Detailed comments inline. The two common issues running through are:

• The use of IsSigned confuses me. We should be computing an unsigned expression at this point, so why does the signedness of the end max expression matter? I think I finally figured it out but a change to the code structure and comments would really help. My current understanding is that IsSigned == true implies (End >=s Start) and !IsSigned implies (End >=u Start) as preconditions of the method. I'd just state that explicitly in comment form.
• We can have an exit which is dynamically dead, produces poison, and overflows in the computation. See the long explanation in the first comment. As far as I can tell, this only applies to the first case.

Sorry this took so long.

llvm/include/llvm/Analysis/ScalarEvolution.h

2033

... if *this* exit is taken

llvm/lib/Analysis/ScalarEvolution.cpp

11518

I'm not sure this holds, let me walk you through why.

There is no guarantee that this exit must be taken. Instead, some other exit could be taken.

The cornercase here is when we have an exit (which won't be taken) whose no-wrap IV does in fact wrap on the last iteration (producing poison), but whose value we don't branch on (e.g. no UB) because an earlier exit is taken instead.

I believe this means the minimum BTC we can report for the (untaken) exit is 2^BW/Stride. (e.g. so it must be >= the exit count of the taken exit)

I believe that invalidates your inequality, and thus your result.

We can patch this in a couple of ways:

• If ControlsExit is true, then we know this condition is branched on by the sole exit. Thus, no other exit, and logic holds.
• If we know this condition is branched on by any latch dominating exit, then we know that the execution of iteration 2^BW/Stride must execute UB if no earlier exit is taken. Thus, either this exit is taken on a previous iteration, or another exit is taken up to that iteration. (I got stuck here, but it really seems like we should be able to do case analysis?)

Aside: If we already know the other exit count is small, it's a real shame we can't use that here... Maybe we can do a two step analysis and simplify using min approach? Just a thought.

11533

Aside: None of the logic below appears to rely on no-wrap facts on the IV. Note sure if it's worth it, but should we reflect that in code structure somehow?

11538

Code structure wise, I request you pass in the BaseStart explicitly. This parsing of expressions is confusing.

11552

The last line of this comment confuses me. Why is this relevant?

Otherwise, the reasoning in this case does appear to hold.

11556

According to my brute force program, your reasoning does hold. I find the isSigned usage very very confusing. Please write out the implied predicates.

11571

This appears to hold, though I didn't follow the logic TBH. I resorted to writing a small program to brute force the i8 space. :)

Please state the !IsSigned precondition in the comment in End >=u Start form.

11577

Again, please state the precondition that IsSigned implies. Your code is correct, but the comment is very hard to follow.

[efriedma]

llvm/lib/Analysis/ScalarEvolution.cpp

11518

If ControlsExit is false, and stride isn't one, it's hard to get here. I think the only way is if canIVOverflowOnLT returns false, which I think is enough to prevent any trouble here? Maybe worth going into in the comment, though.

11571

It's basically just proving "end + (stride-1)" doesn't overflow. I'll try to clarify the comment.

[efriedma]

Spent some more time on this.

I discovered that some of the checks were not really necessary. I think I must have added a check, then didn't realize it became unnecessary as I added other checks. So it's down to three relatively straightforward checks. We can re-add the other checks if we discover practical cases where they're necessary.

I rewrote the power-of-two proof; hopefully makes it more clear that it's actually correct. And I clarified the signed vs. unsigned on the other checks.

Separated out getUDivCeilSCEV() as a separate function. Makes this patch a little easier to read, and hopefully the general utility is useful for other cases in the future.

[reames]

llvm/lib/Analysis/ScalarEvolution.cpp

11518

I believe you are correct, though I'll note I really dislike code whose correctness depends on understanding a non-trivial invariant through a large batch of complicated code. Please try to comment this clearly!

[reames]

LGTM

Thank you for pushing this through.

I'll have a couple of small followups for review to tweak comments and code structure, but what you've got is a huge improvement and I want to get this in. It unblocks several other changes which improve opt quality.

[mstorsjo]

I’ve bisected a miscompilation on aarch64 down to this commit. I’ll follow up with a repro later…

[shchenz]

Yeah, we also found issue on PowerPC target. Reducing a small case:

__attribute__((noinline))int foo(int *arr)
{
  int prime = 0, k = 0;

  for(int i = 0; i < 8191; i++) {
    prime = i + i + 1; 
    k = i + prime;
    for (int j = k; j < 8191; j += prime)
      arr[j] = 0;
  }
  return 0;
}
int main(void)
{
  int arr[8191];

  foo (arr);
  return 0;
}

$ clang -O2 t.cpp ; ./a.out
Segmentation fault (core dumped)

-fno-vectorize can make above case pass. Initial investigation shows that after this patch, the loop execution count for the vectorized loop now can be wrap, so generate unexpected behaviour.

[uabelho]

Hi,

We see a miscompile as well.
It goes wrong for my out of tree target so I don't have a reproducer for an in tree target but maybe some info may help anyway.
I have a function containing the following two nested loops:

void foo()
{
    #define MAX 2048

    static unsigned a[MAX];

    unsigned count = 2;

    for (unsigned i = 0; i < MAX; ++i)
    {
        if (a[i] == 0)
        {
            unsigned p = i + i + 3;
            count++;
            for (unsigned j = i; j < MAX; j += p)
            {
                a[j] = 1;
            }
        }
    }
    assert(count == 565);
}

With some debug printouts from the compiler I see that before we got the following from SCEV for the inner loop:

Exit count: ({2047,+,-1}<%for.body> /u {3,+,2}<nuw><nsw><%for.body>)
Trip count: (1 + ({2047,+,-1}<%for.body> /u {3,+,2}<nuw><nsw><%for.body>))<nuw><nsw>
Trip count bound: 16 bits, [1,684)

and with the patch we get

Exit count: ((((-1 * (1 umin {2045,+,-3}<%for.body>))<nuw><nsw> + {2045,+,-3}<%for.body>) /u {3,+,2}<nuw><nsw><%for.body>) + (1 umin {2045,+,-3}<%for.body>))
Trip count: (1 + (((-1 * (1 umin {2045,+,-3}<%for.body>))<nuw><nsw> + {2045,+,-3}<%for.body>) /u {3,+,2}<nuw><nsw><%for.body>) + (1 umin {2045,+,-3}<%for.body>))
Trip count bound: 16 bits, [1,21848)

With some printouts in the outer and inner loop I also see that when i is 682, then something goes wrong for the inner loop and it executes for the following (way too many) j values:

outer. i: 682
  inner. j: 682
  inner. j: 2049
  inner. j: 3416
  inner. j: 4783
  inner. j: 6150
  [...]
  inner. j: 63564
  inner. j: 64931
  inner. j: 762
outer. i: 683

[mstorsjo]

The case I'm observing is within this translation unit: https://martin.st/temp/gsmdec-preproc.c

There's some difference visible in the assembly generated by clang -target aarch64-linux-gnu -c -O3 gsmdec-preproc.c, I haven't exactly pinpointed what part of it is that breaks.

If you have access to aarch64 linux, the issue can be reproduced at runtime with these commands:

git clone git://source.ffmpeg.org/ffmpeg
cd ffmpeg
./configure --cc=clang --samples=/path/to/empty/dir
make fate-rsync # sync data samples for running tests, into the path specified above
make -j$(nproc) fate-g723_1-dec-1

The error in this case is in libavformat/gsmdec.o. There's also a couple other miscompilations in there, visible in make fate-sub-vplayer and make fate-wmavoice-7k, but I haven't pinpointed which translation unit those errors stem from.

[efriedma]

I think the miscompile is the isLoopEntryGuardedByCond issue noted in https://reviews.llvm.org/D105216#2851010 . Looking.

[efriedma]

Updated to fix the miscompile. This unfortunately involves yet another complicated proof...

[efriedma]

More refactoring. Unbreak howManyGreaterThans.

[efriedma]

@reames Please take another look before I merge; I ended up substantially refactoring the patch to deal with the miscompile.

[reames]

I've glanced at this, and the refactor/new code seems very complicated to me. My LGTM no longer applies. I will try to take a closer look at the reasoning in the newly added parts, but I *strongly* request you look for ways to factor the code so that the reasoning is modular. If we can split this into two or more patches, that would be my strong preference.

[efriedma]

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.

If we can split this into two or more patches, that would be my strong preference.

I can split off the introduction of getUDivCeilSCEV() into a separate patch, and I can introduce the new isLoopEntryGuardedByCond(L, CondGT, Start, StartMinusStride) check in a separate patch. I'm not sure the result is easier to review, but I guess it would make it easier to figure out regressions.

[efriedma]

Posted D105865 with just cleanup. Then I'll post a followup with the missing isLoopEntryGuardedByCond() checks. Then I'll rebase this (so at that point, we'll just be adding the MayAddOverflow checks). Let me know if that makes sense.

[reames]

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

If we can split this into two or more patches, that would be my strong preference.

I can split off the introduction of getUDivCeilSCEV() into a separate patch, and I can introduce the new isLoopEntryGuardedByCond(L, CondGT, Start, StartMinusStride) check in a separate patch. I'm not sure the result is easier to review, but I guess it would make it easier to figure out regressions.

Splitting patches to isolate regressions is good!

I went ahead and landed e4b43973. This handles only the constant bounds cases using the new ceiling operation. This is an easy sub-case because a) stride is known positive, b) it'll constant fold thus not changing the result at all, and c) it doesn't appear to be influenced by your most recent proof. If you rebase over that, it should help a bit to reduce complexity.

[efriedma]

In D105216#2874452, @reames wrote:

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

[reames]

In D105216#2874703, @efriedma wrote:

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.

It's this last bit which is non-obvious from the patch. You're using an entirely different formula for the BTC in this case, you should say so in the comments!

[reames]

Eli, I think I just had an "aha!" moment. Check my reasoning here, but I think we can greatly simplify the patch structure.

The most recent case you added, appears to simply be a specialization of ceiling(max(A,B)-A, C) where max(A,B) > A - C is known. I don't think we actually need to know anything about where A, B, and C come from for your lowering to be valid. I think we can also generalize this slightly into two pieces:

1. A general ceiling lowering when ceiling(X-A, C) where X > A - C
2. A pushdown rule for max(X,Y) > Z as X > Z && Y > Z ==> max(X,Y) > Z

This really tempts me to go back to the first version of your patch, and add another specialization of how to generate a faster ceiling.

What do you think?

llvm/lib/Analysis/ScalarEvolution.cpp

11849

I split off this part of the change into 087310c71e with a bit of restructuring.

[efriedma]

The general formula for the backedge-taken count can be written, in arbitrary-precision arithmetic, as something like floor(max(End - Start + Stride - 1, 0) / Stride), I think. We could define a function to compute that, I guess, separate from howManyLessThans, and optimize based on that.

Granted, that's basically just taking this patch, and shoving the code into a different function. But it might be easier to reason about future changes.

[reames]

Eli,

I went ahead and posted https://reviews.llvm.org/D105942 which splits this one step further, but in the process, I also convinced myself of the correctness of your revised patch. I'd be fine either landing the one I posted, then rebasing this into a smaller patch, or simply landing this one after rebase, and then posting a cleanup or two afterwards. Up to you.

I still like the idea of having all of this inside getUDivCeiling if possible, but doing that as cleanup once this lands seems reasonable.

[reames]

Eli, I think we're out of things which can be reasonable split here. If you want to rebase your patch - preferably the form close to what you committed before - I think we're ready for the last big piece to go in. We probably should wait a day or two to make sure the previous bits stick, but assuming they do, I don't see any reason to delay this further.

[efriedma]

Rebased.

[reames]

LGTM

And thank you!

llvm/include/llvm/Analysis/ScalarEvolution.h

private:
   /// PredicatedSCEVRewrites.
   /// If the analysis is not successful, a mapping from the \p SymbolicPHI to
   /// itself (with no predicates) is recorded, and a nullptr with an empty
   /// predicates vector is returned as a pair.
   Optional<std::pair<const SCEV *, SmallVector<const SCEVPredicate *, 3>>>
   createAddRecFromPHIWithCastsImpl(const SCEVUnknown *SymbolicPHI);
 
   /// Compute the backedge taken count knowing the interval difference, and
-  /// the stride for an inequality.  Result takes the form:
-  /// (Delta + (Stride - 1)) udiv Stride.
-  /// Caller must ensure that this expression either does not overflow or
-  /// that the result is undefined if it does.
-  const SCEV *computeBECount(const SCEV *Delta, const SCEV *Stride);
+  /// the stride for an inequality.
+  ///
+  /// Caller must ensure that non-negative N exists such that
+  /// (Start + Stride * N) >= End, and that computing "(Start + Stride * N)"
+  /// doesn't overflow. In other words:
+  /// 1. If IsSigned is true, Start <=s End. Otherwise, Start <=u End.
+  /// 2. If End is not equal to start and IsSigned is true, Stride >s 0. If
+  ///    End is not equal to start and IsSigned is false, Stride >u 0.
+  /// 3. The index variable doesn't overflow.
+  ///
+  /// If the preconditions hold, the backedge taken count is N.
+  ///
+  /// IsSigned determines whether End, Start, and Stride are treated as
+  /// signed values, for the purpose of optimizing the form of the result.
+  ///
+  /// This function tries to use an optimized form:
+  /// ((End - Start) + (Stride - 1)) /u Stride
+  ///
+  /// If it can't prove the addition doesn't overflow in that form, it uses
+  /// getUDivCeilSCEV.
+  const SCEV *computeBECount(bool IsSigned, const SCEV *Start, const SCEV *End,
+                             const SCEV *Stride);
+
+  /// Compute ceil(N / D). N and D are treated as unsigned values.
+  ///
+  /// Since SCEV doesn't have native ceiling division, this generates a
+  /// SCEV expression of the following form:
+  ///
+  /// umin(N, 1) + floor((N - umin(N, 1)) / D)
+  ///
+  /// A denominator of zero or poison is handled the same way as getUDivExpr().
+  const SCEV *getUDivCeilSCEV(const SCEV *N, const SCEV *D);
 
   /// Compute the maximum backedge count based on the range of values
   /// permitted by Start, End, and Stride. This is for loops of the form
   /// {Start, +, Stride} LT End.
   ///
   /// Precondition: the induction variable is known to be positive.  We *don't*
   /// assert these preconditions so please be careful.
   const SCEV *computeMaxBECountForLT(const SCEV *Start, const SCEV *Stride,

llvm/lib/Analysis/ScalarEvolution.cpp

bool ScalarEvolution::canIVOverflowOnGT(const SCEV *RHS, const SCEV *Stride,
   APInt MinRHS = getUnsignedRangeMin(RHS);
   APInt MinValue = APInt::getMinValue(BitWidth);
   APInt MaxStrideMinusOne = getUnsignedRangeMax(getMinusSCEV(Stride, One));
 
   // UMinRHS - UMaxStrideMinusOne < UMinValue => overflow!
   return (std::move(MinValue) + MaxStrideMinusOne).ugt(MinRHS);
 }
 
-const SCEV *ScalarEvolution::computeBECount(const SCEV *Delta,
-                                            const SCEV *Step) {
-  const SCEV *One = getOne(Step->getType());
-  Delta = getAddExpr(Delta, getMinusSCEV(Step, One));
-  return getUDivExpr(Delta, Step);
+const SCEV *ScalarEvolution::computeBECount(bool IsSigned, const SCEV *Start,
+                                            const SCEV *End,
+                                            const SCEV *Stride) {
+  // The basic formula here is ceil((End - Start) / Stride).  Since SCEV
+  // doesn't natively have division that rounds up, we need to convert to
+  // floor division.
+  //
+  // MayOverflow is whether adding (End - Start) + (Stride - 1)
+  // can overflow if Stride is positive. It's a precondition of the
+  // function that "End - Start" doesn't overflow. We handle the case where
+  // Stride isn't positive later.
+  //
+  // In practice, the arithmetic almost never overflows, but we have to prove
+  // it.  We have a variety of ways to come up with a proof.
+  const SCEV *One = getOne(Stride->getType());
+  bool MayOverflow = [&] {
+    if (auto *StrideC = dyn_cast<SCEVConstant>(Stride)) {
+      if (StrideC->getAPInt().isPowerOf2()) {
+        // Suppose Stride is a power of two, and Start/End are unsigned
+        // integers.  Let UMAX be the largest representable unsigned
+        // integer.
+        //
+        // By the preconditions of this function (see comment in header), we
+        // know "(Start + Stride * N)" >= End, and this doesn't overflow.
+        // As a formula:
+        //
+        //   End <= (Start + Stride * N) <= UMAX
+        //
+        // Subtracting Start from all the terms:
+        //
+        //   End - Start <= Stride * N <= UMAX - Start
+        //
+        // Since Start is unsigned, UMAX - Start <= UMAX.  Therefore:
+        //
+        //   End - Start <= Stride * N <= UMAX
+        //
+        // Stride * N is a multiple of Stride. Therefore,
+        //
+        //   End - Start <= Stride * N <= UMAX - (UMAX mod Stride)
+        //
+        // Since Stride is a power of two, UMAX + 1 is divisible by Stride.
+        // Therefore, UMAX mod Stride == Stride - 1.  So we can write:
+        //
+        //   End - Start <= Stride * N <= UMAX - Stride - 1
+        //
+        // Dropping the middle term:
+        //
+        //   End - Start <= UMAX - Stride - 1
+        //
+        // Adding Stride - 1 to both sides:
+        //
+        //   (End - Start) + (Stride - 1) <= UMAX
+        //
+        // In other words, the addition doesn't have unsigned overflow.
+        //
+        // A similar proof works if we treat Start/End as signed values.
+        // Just rewrite steps before "End - Start <= Stride * N <= UMAX" to
+        // use signed max instead of unsigned max. Note that we're trying
+        // to prove a lack of unsigned overflow in either case.
+        return false;
+      }
+    }
+    if (Start == Stride || Start == getMinusSCEV(Stride, One)) {
+      // If Start is equal to Stride, (End - Start) + (Stride - 1) == End - 1.
+      // If !IsSigned, 0 <u Stride == Start <=u End; so 0 <u End - 1 <u End.
+      // If IsSigned, 0 <s Stride == Start <=s End; so 0 <s End - 1 <s End.
+      //
+      // If Start is equal to Stride - 1, (End - Start) + Stride - 1 == End.
+      return false;
+    }
+    if (IsSigned && isKnownNonNegative(Start)) {
+      // IsSigned implies "Start <=s End <=s INT_MAX".
+      // "isKnownNonNegative(Start)" implies "Start >=s 0".
+      // Therefore, "0 <=s End - Start <=s INT_MAX - Start <= INT_MAX".
+      // IsSigned also implies "0 <=s Stride - 1 <s INT_MAX". Therefore,
+      // "(End - Start) + (Stride - 1) <u INT_MAX * 2 <u UINT_MAX".
+      return false;
+    }
+    return true;
+  }();
+
+  // Force the stride to at least one, so we don't divide by zero. The stride
+  // can be zero if Delta is zero. We don't actually care what value we use
+  // for Stride in this case, as long as it isn't zero.
+  Stride = getUMaxExpr(Stride, One);
+
+  const SCEV *Delta = getMinusSCEV(End, Start);
+  if (!MayOverflow) {
+    // floor((D + (S - 1)) / S)
+    // We prefer this formulation if it's legal because it's fewer operations.
+    return getUDivExpr(getAddExpr(Delta, getMinusSCEV(Stride, One)), Stride);
+  }
+  return getUDivCeilSCEV(Delta, Stride);
+}
+
+const SCEV *ScalarEvolution::getUDivCeilSCEV(const SCEV *N, const SCEV *D) {
+  // umin(N, 1) + floor((N - umin(N, 1)) / D)
+  // This is equivalent to "1 + floor((N - 1) / D)" for N != 0. The umin
+  // expression fixes the case of N=0.
+  const SCEV *MinNOne = getUMinExpr(N, getOne(N->getType()));
+  const SCEV *NMinusOne = getMinusSCEV(N, MinNOne);
+  return getAddExpr(MinNOne, getUDivExpr(NMinusOne, D));
 }
 
 const SCEV *ScalarEvolution::computeMaxBECountForLT(const SCEV *Start,
                                                     const SCEV *Stride,
                                                     const SCEV *End,
                                                     unsigned BitWidth,
                                                     bool IsSigned) {
 
   assert(!isKnownNonPositive(Stride) &&
          "Stride is expected strictly positive!");
   // Calculate the maximum backedge count based on the range of values
   // permitted by Start, End, and Stride.
   const SCEV *MaxBECount;
   APInt MinStart =
       IsSigned ? getSignedRangeMin(Start) : getUnsignedRangeMin(Start);
 
const SCEV *ScalarEvolution::computeMaxBECountForLT(const SCEV *Start,
 
   // Although End can be a MAX expression we estimate MaxEnd considering only
   // the case End = RHS of the loop termination condition. This is safe because
   // in the other case (End - Start) is zero, leading to a zero maximum backedge
   // taken count.
   APInt MaxEnd = IsSigned ? APIntOps::smin(getSignedRangeMax(End), Limit)
                           : APIntOps::umin(getUnsignedRangeMax(End), Limit);
 
-  MaxBECount = computeBECount(getConstant(MaxEnd - MinStart) /* Delta */,
+  MaxBECount = getUDivCeilSCEV(getConstant(MaxEnd - MinStart) /* Delta */,
                                getConstant(StrideForMaxBECount) /* Step */);
 
   return MaxBECount;
 }
 
 ScalarEvolution::ExitLimit
 ScalarEvolution::howManyLessThans(const SCEV *LHS, const SCEV *RHS,
                                   const Loop *L, bool IsSigned,
                                   bool ControlsExit, bool AllowPredicates) {
if (!isLoopInvariant(RHS, L)) {
     return ExitLimit(getCouldNotCompute() /* ExactNotTaken */, MaxBECount,
                      false /*MaxOrZero*/, Predicates);
   }
   // If the backedge is taken at least once, then it will be taken
   // (End-Start)/Stride times (rounded up to a multiple of Stride), where Start
   // is the LHS value of the less-than comparison the first time it is evaluated
   // and End is the RHS.
   const SCEV *BECountIfBackedgeTaken =
-    computeBECount(getMinusSCEV(End, Start), Stride);
+      computeBECount(IsSigned, Start, End, Stride);
   // If the loop entry is guarded by the result of the backedge test of the
   // first loop iteration, then we know the backedge will be taken at least
   // once and so the backedge taken count is as above. If not then we use the
   // expression (max(End,Start)-Start)/Stride to describe the backedge count,
   // as if the backedge is taken at least once max(End,Start) is End and so the
   // result is as above, and if not max(End,Start) is Start so we get a backedge
   // count of zero.
   const SCEV *BECount;
   if (isLoopEntryGuardedByCond(L, Cond, getMinusSCEV(OrigStart, Stride), OrigRHS))
     BECount = BECountIfBackedgeTaken;
   else {
     // If we know that RHS >= Start in the context of loop, then we know that
     // max(RHS, Start) = RHS at this point.
     if (isLoopEntryGuardedByCond(
             L, IsSigned ? ICmpInst::ICMP_SGE : ICmpInst::ICMP_UGE, OrigRHS, OrigStart))
       End = RHS;
     else
       End = IsSigned ? getSMaxExpr(RHS, Start) : getUMaxExpr(RHS, Start);
-    BECount = computeBECount(getMinusSCEV(End, Start), Stride);
+    BECount = computeBECount(IsSigned, Start, End, Stride);
   }
 
   const SCEV *MaxBECount;
   bool MaxOrZero = false;
   if (isa<SCEVConstant>(BECount))
     MaxBECount = BECount;
   else if (isa<SCEVConstant>(BECountIfBackedgeTaken)) {
     // If we know exactly how many times the backedge will be taken if it's

 }
 
 ScalarEvolution::ExitLimit
 ScalarEvolution::howManyGreaterThans(const SCEV *LHS, const SCEV *RHS,
                                      const Loop *L, bool IsSigned,
                                      bool ControlsExit, bool AllowPredicates) {
   SmallPtrSet<const SCEVPredicate *, 4> Predicates;
   // We handle only IV > Invariant
   if (!isLoopInvariant(RHS, L))
     return getCouldNotCompute();
 
   const SCEVAddRecExpr *IV = dyn_cast<SCEVAddRecExpr>(LHS);
   if (!IV && AllowPredicates)
     // Try to make this an AddRec using runtime tests, in the first X
     // iterations of this loop, where X is the SCEV expression found by the
     // algorithm below.
     IV = convertSCEVToAddRecWithPredicates(LHS, L, Predicates);
if (isa<SCEVCouldNotCompute>(Start))
       return Start;
   }
   if (End->getType()->isPointerTy()) {
     End = getLosslessPtrToIntExpr(End);
     if (isa<SCEVCouldNotCompute>(End))
       return End;
   }
 
-  const SCEV *BECount = computeBECount(getMinusSCEV(Start, End), Stride);
+  const SCEV *BECount = computeBECount(IsSigned, End, Start, Stride);
 
   APInt MaxStart = IsSigned ? getSignedRangeMax(Start)
                             : getUnsignedRangeMax(Start);
 
   APInt MinStride = IsSigned ? getSignedRangeMin(Stride)
                              : getUnsignedRangeMin(Stride);
 
   unsigned BitWidth = getTypeSizeInBits(LHS->getType());
   APInt Limit = IsSigned ? APInt::getSignedMinValue(BitWidth) + (MinStride - 1)
                          : APInt::getMinValue(BitWidth) + (MinStride - 1);
 
   // Although End can be a MIN expression we estimate MinEnd considering only
   // the case End = RHS. This is safe because in the other case (Start - End)
   // is zero, leading to a zero maximum backedge taken count.
   APInt MinEnd =
     IsSigned ? APIntOps::smax(getSignedRangeMin(RHS), Limit)
              : APIntOps::umax(getUnsignedRangeMin(RHS), Limit);
 
   const SCEV *MaxBECount = isa<SCEVConstant>(BECount)
                                ? BECount
-                               : computeBECount(getConstant(MaxStart - MinEnd),
+                               : getUDivCeilSCEV(getConstant(MaxStart - MinEnd),
                                                  getConstant(MinStride));
 
-  if (isa<SCEVCouldNotCompute>(MaxBECount))
-    MaxBECount = BECount;
-
   return ExitLimit(BECount, MaxBECount, false, Predicates);
 }
 
 const SCEV *SCEVAddRecExpr::getNumIterationsInRange(const ConstantRange &Range,
                                                     ScalarEvolution &SE) const {
   if (Range.isFullSet())  // Infinite loop.
     return SE.getCouldNotCompute();
 

llvm/test/Analysis/ScalarEvolution/2008-11-18-Stride1.ll

 ; RUN: opt < %s -analyze -enable-new-pm=0 -scalar-evolution | FileCheck %s
 ; RUN: opt < %s -disable-output "-passes=print<scalar-evolution>" 2>&1 | FileCheck %s
 
-; CHECK: Loop %bb: backedge-taken count is ((-5 + %x) /u 3)
+; CHECK: Loop %bb: backedge-taken count is (((-7 + (-1 * (1 umin (-7 + %x)))<nuw><nsw> + %x) /u 3) + (1 umin (-7 + %x)))
 ; CHECK: Loop %bb: max backedge-taken count is 1431655764
 
-
-; ScalarEvolution can't compute a trip count because it doesn't know if
-; dividing by the stride will have a remainder. This could theoretically
-; be teaching it how to use a more elaborate trip count computation.
-
 define i32 @f(i32 %x) nounwind readnone {
 entry:
   %0 = icmp ugt i32 %x, 4    ; <i1> [#uses=1]
   br i1 %0, label %bb.nph, label %bb2
 
 bb.nph:   ; preds = %entry
   br label %bb
 

llvm/test/Analysis/ScalarEvolution/2008-11-18-Stride2.ll

 ; RUN: opt < %s -analyze -enable-new-pm=0 -scalar-evolution 2>&1 | FileCheck %s
 ; RUN: opt < %s -disable-output "-passes=print<scalar-evolution>" 2>&1 2>&1 | FileCheck %s
 
-; CHECK: Loop %bb: backedge-taken count is ((999 + (-1 * %x)) /u 3)
+; CHECK: Loop %bb: backedge-taken count is (((997 + (-1 * (1 umin (997 + (-1 * %x))))<nuw><nsw> + (-1 * %x)) /u 3) + (1 umin (997 + (-1 * %x))))
 ; CHECK: Loop %bb: max backedge-taken count is 334
 
-
-; This is a tricky testcase for unsigned wrap detection which ScalarEvolution
-; doesn't yet know how to do.
+; This is a tricky testcase for unsigned wrap detection.
 
 define i32 @f(i32 %x) nounwind readnone {
 entry:
   %0 = icmp ugt i32 %x, 999    ; <i1> [#uses=1]
   br i1 %0, label %bb2, label %bb.nph
 
 bb.nph:   ; preds = %entry
   br label %bb

llvm/test/Analysis/ScalarEvolution/trip-count-unknown-stride.ll

 ; RUN: opt < %s -analyze -enable-new-pm=0 -scalar-evolution | FileCheck %s
 ; RUN: opt < %s -disable-output "-passes=print<scalar-evolution>" 2>&1 | FileCheck %s
 
 ; ScalarEvolution should be able to compute trip count of the loop by proving
 ; that this is not an infinite loop with side effects.
 
-; CHECK: Determining loop execution counts for: @foo1
-; CHECK: backedge-taken count is ((-1 + %n) /u %s)
+; CHECK-LABEL: Determining loop execution counts for: @foo1
+; CHECK: backedge-taken count is ((-1 + (-1 * %s) + (1 umax %s) + %n) /u (1 umax %s))
 
 ; We should have a conservative estimate for the max backedge taken count for
 ; loops with unknown stride.
 ; CHECK: max backedge-taken count is -1
 
 target datalayout = "e-m:e-p:32:32-f64:32:64-f80:32-n8:16:32-S128"
 
 define void @foo1(i32* nocapture %A, i32 %n, i32 %s) mustprogress {
for.body:                                         ; preds = %entry, %for.body
   br i1 %cmp, label %for.body, label %for.end
 
 for.end:                                          ; preds = %for.body, %entry
   ret void
 }
 
 
 ; Check that we are able to compute trip count of a loop without an entry guard.
-; CHECK: Determining loop execution counts for: @foo2
-; CHECK: backedge-taken count is ((-1 + (%n smax %s)) /u %s)
+; CHECK-LABEL: Determining loop execution counts for: @foo2
+; CHECK: backedge-taken count is ((-1 + (-1 * %s) + (1 umax %s) + (%n smax %s)) /u (1 umax %s))
 
 ; We should have a conservative estimate for the max backedge taken count for
 ; loops with unknown stride.
 ; CHECK: max backedge-taken count is -1
 
 define void @foo2(i32* nocapture %A, i32 %n, i32 %s) mustprogress {
 entry:
   br label %for.body
for.body:                                         ; preds = %entry, %for.body
   br i1 %cmp, label %for.body, label %for.end
 
 for.end:                                          ; preds = %for.body, %entry
   ret void
 }
 
 ; Check that without mustprogress we don't make assumptions about infinite
 ; loops being UB.
-; CHECK: Determining loop execution counts for: @foo3
+; CHECK-LABEL: Determining loop execution counts for: @foo3
 ; CHECK: Loop %for.body: Unpredictable backedge-taken count.
 ; CHECK: Loop %for.body: Unpredictable max backedge-taken count.
 
 define void @foo3(i32* nocapture %A, i32 %n, i32 %s) {
 entry:
   br label %for.body
 
 for.body:                                         ; preds = %entry, %for.body
   %i.05 = phi i32 [ %add, %for.body ], [ 0, %entry ]
   %arrayidx = getelementptr inbounds i32, i32* %A, i32 %i.05
   %0 = load i32, i32* %arrayidx, align 4
   %inc = add nsw i32 %0, 1
   store i32 %inc, i32* %arrayidx, align 4
   %add = add nsw i32 %i.05, %s
   %cmp = icmp slt i32 %add, %n
   br i1 %cmp, label %for.body, label %for.end
 
 for.end:                                          ; preds = %for.body, %entry
   ret void
 }
 
 ; Same as foo2, but with mustprogress on loop, not function
-; CHECK: Determining loop execution counts for: @foo4
-; CHECK: backedge-taken count is ((-1 + (%n smax %s)) /u %s)
+; CHECK-LABEL: Determining loop execution counts for: @foo4
+; CHECK: backedge-taken count is ((-1 + (-1 * %s) + (1 umax %s) + (%n smax %s)) /u (1 umax %s))
 ; CHECK: max backedge-taken count is -1
 
 define void @foo4(i32* nocapture %A, i32 %n, i32 %s) {
 entry:
   br label %for.body
 
 for.body:                                         ; preds = %entry, %for.body
   %i.05 = phi i32 [ %add, %for.body ], [ 0, %entry ]
   %arrayidx = getelementptr inbounds i32, i32* %A, i32 %i.05
   %0 = load i32, i32* %arrayidx, align 4
   %inc = add nsw i32 %0, 1
   store i32 %inc, i32* %arrayidx, align 4
   %add = add nsw i32 %i.05, %s
   %cmp = icmp slt i32 %add, %n
   br i1 %cmp, label %for.body, label %for.end, !llvm.loop !8
 
 for.end:                                          ; preds = %for.body, %entry
   ret void
 }
 
+; A more complex case with pre-increment compare instead of post-increment.
+; CHECK-LABEL: Determining loop execution counts for: @foo5
+; CHECK: Loop %for.body: backedge-taken count is ((((-1 * (1 umin ((-1 * %start) + (%n smax %start))))<nuw><nsw> + (-1 * %start) + (%n smax %start)) /u (1 umax %s)) + (1 umin ((-1 * %start) + (%n smax %start))))
+
+; We should have a conservative estimate for the max backedge taken count for
+; loops with unknown stride.
+; CHECK: max backedge-taken count is -1
+
+define void @foo5(i32* nocapture %A, i32 %n, i32 %s, i32 %start) mustprogress {
+entry:
+  br label %for.body
+
+for.body:                                         ; preds = %entry, %for.body
+  %i.05 = phi i32 [ %add, %for.body ], [ %start, %entry ]
+  %arrayidx = getelementptr inbounds i32, i32* %A, i32 %i.05
+  %0 = load i32, i32* %arrayidx, align 4
+  %inc = add nsw i32 %0, 1
+  store i32 %inc, i32* %arrayidx, align 4
+  %add = add nsw i32 %i.05, %s
+  %cmp = icmp slt i32 %i.05, %n
+  br i1 %cmp, label %for.body, label %for.end
+
+for.end:                                          ; preds = %for.body, %entry
+  ret void
+}
+
 !8 = distinct !{!8, !9}
 !9 = !{!"llvm.loop.mustprogress"}