[SCEV] Allow negative steps for LT exit count computation for unsigned comparisons

[reames]

Summary

This bit of code is incredibly suspicious. It allows fully unknown (but potentially negative) steps, but not steps known to be negative. The comment about scev flag inference is worrying, but also not correct to my knowledge.

At best, this might be covering up some related miscompile. However, there's no test in tree for it, the review history doesn't include obvious motivation, and the C++ example doesn't appear to give wrong results when hand translated to IR. I think it's time to remove this and see what falls out.

[efriedma]

llvm/lib/Analysis/ScalarEvolution.cpp

11710–11718

Does the logic here actually work correctly for step=0? It looks like we end up dividing by zero.

If we can prove the step is non-zero, loopIsFiniteByAssumption seems too aggressive; a lack of abnormal exits should be enough. We'll hit UB after a finite number of steps.

Using isKnownPositive doesn't really make sense in the unsigned case; an unsigned number can't be negative.

[reames]

llvm/lib/Analysis/ScalarEvolution.cpp

11710–11718

Step can't be zero, or the loop would be infinite. Though, actually, writing that, I see a latent bug here. The loop could be finite *because we took another exit*, the step of this IV could still be zero, and we could still have a divide by zero along this path.

I don't think that has anything to do with this change though.

p.s. Yes, we can infer non-zero other ways. I even have one patch out to do that right now. :)

[efriedma]

llvm/lib/Analysis/ScalarEvolution.cpp

11710–11718

I agree this patch makes sense, just saying it might expose other issues.

*because we took another exit*

Even if we take this exit. If the backedge-taken count is zero, the step doesn't matter.

[reames]

llvm/lib/Analysis/ScalarEvolution.cpp

11710–11718

Eli, I think you're missing the point slightly. For the induction step to be zero, and for this to be the sole exit, then the loop must be infinite. Since mustprogress infinite loops are undefined, any result from this function is allowed. If there's a divide by zero which causes a compiler crash, that would be bad, but literally any result is legal at that point.

[efriedma]

llvm/lib/Analysis/ScalarEvolution.cpp

11710–11718

If the induction step is zero, and this is the sole exit, the loop is either infinite, or has a backedge-taken count of zero. See, for example, https://godbolt.org/z/9djfj1Ycq .

[reames]

llvm/lib/Analysis/ScalarEvolution.cpp

11710–11718

Gah, yeah, you're correct. No idea why I didn't see that the first time.

[reames]

Rebase over tests which actually exercise code and show difference.

The zero stride issue was fixed separately. This still depends on Eli's patch for overflow correctness. Once that's fixed, I think this will be safe.

It's worth noting that given a condition which dominates the latch, an IV which has either nsw or nuw, and a negative step, the exit backedge taken must be either 0 or 1. For it to be more than that, we must perform at least two adds of negative value which must by definition wrap. As a result, we could do much better in terms of formulas specific for negative strides, but I'm not really interested in bothering. The main value of this patch is in making it easier to exercise the general path via tests.

[efriedma]

llvm/lib/Analysis/ScalarEvolution.cpp

11556–11560

Is the unconditional use of "smax" here going to cause issues?

11571

Instead of computing min(End, Limit) - Start, should we be using max(End, Start) - Start like we do elsewhere?

11704

This is inductive logic, right? If the first iteration doesn't the loop, the following iterations also can't exit the loop.

I think this logic requires that RHS is invariant? Not that we would compute BECount anyway in that case, but I think we might underestimate MaxBECount.

[efriedma]

llvm/lib/Analysis/ScalarEvolution.cpp

11556–11560

Oh, also, if BitWidth is one, "One" is a negative number. isKnownNonPositive(Stride) guards against this, since it's always true for an i1 value. :)

[efriedma]

llvm/lib/Analysis/ScalarEvolution.cpp

11556–11560

I'll write a patch for computeMaxBECountForLT.

[efriedma]

Posted D106197. That addresses all my review comments here except the one about the RHS being invariant.

[reames]

Address Eli's review comment which isn't covered by D106197.

I'm going to land some tests for this case and probably split this patch since this appears to be a flaw in the existing logic for potentially zero strides.

[efriedma]

llvm/lib/Analysis/ScalarEvolution.cpp

11701

I think this needs to be "if the stride is negative and rhs is invariant".

[reames]

Needs to be rebased over D106327 once landed.

[reames]

llvm/lib/Analysis/ScalarEvolution.cpp

11701

I've given this a lot of thought and I don't believe this is true. Let me explain why I think the code is correct, and you can poke holes in my reasoning. :)

A negative stride must be greater than half of the addressable space. Thus, we can only add a negative stride once without producing poison.

We check that if IV becomes poison that the loop must execute UB. (This is the purpose of the ControlsExit check combined with the flag check.) Thus, we don't have to worry about IV being poison, but another exit being taken before the one we're analyzing. (This is important as it cuts off a *lot* of subtle edge case reasoning.)

As a result, we can infer that IV must add the step at most once. Given we must increment IV on each iteration, this implies the backedge is not taken.

Note that the value of RHS did not appear in any of that logic.

Chasing through the code for computeMaxBECountForLT, we appear to produce a correct/conservative result for a negative stride.

Do you have a particular counter example in mind?

p.s. The means by which we prove poison triggers immediate UB could be generalized easily here. Maybe something to explore in the future if we want to expand support for multiple exit loops.

[efriedma]

llvm/lib/Analysis/ScalarEvolution.cpp

11701

I was thinking of something like this:

int a(int *x) {
  int i = 0;
  do {
    i -= 2;
  } while (i < x[i]);
  return i;
}
int main() {
    int z[] = {-100000,0,0,0,};
    __builtin_printf("%d\n", a(z+4));
}

Am I missing some condition that excludes this?

[reames]

llvm/lib/Analysis/ScalarEvolution.cpp

11701

Quick answer: I'd gotten myself confused on nsw semantics of add w/negative RHS again. Long answer to follow once I've given it a bit more thought.

[reames]

Narrowing focus to unsigned comparisons.

The reasoning about signed cases makes my head hurt, and even after staring at it for a while, I'm neither sure the code is correct or incorrect for signed comparisons. Give my actual interest is unsigned IVs, I propose we just defer the signed cases until someone else has time, interest, and the ability to reason through it.

@efriedma Sorry for the silence on this for so long.

p.s. I'm going to mark this as dependent on D109029 as the diff is built on top of that patch and might be confusing otherwise, but there's no semantic connection between the two.

[reames]

@efriedma ping?

[efriedma]

LGTM

llvm/lib/Analysis/ScalarEvolution.cpp

const SCEV *ScalarEvolution::computeMaxBECountForLT(const SCEV *Start,
                                                     const SCEV *End,
                                                     unsigned BitWidth,
                                                     bool IsSigned) {
   // The logic in this function assumes we can represent a positive stride.
   // If we can't, the backedge-taken count must be zero.
   if (IsSigned && BitWidth == 1)
     return getZero(Stride->getType());
 
+  // This code has only been closely audited for negative strides in the
+  // unsigned comparison case, it may be correct for signed comparison, but
+  // that needs to be established.
+  assert((!IsSigned || !isKnownNonPositive(Stride)) &&
+         "Stride is expected strictly positive for signed case!");
+
   // Calculate the maximum backedge count based on the range of values
   // permitted by Start, End, and Stride.
   APInt MinStart =
       IsSigned ? getSignedRangeMin(Start) : getUnsignedRangeMin(Start);
 
   APInt MinStride =
       IsSigned ? getSignedRangeMin(Stride) : getUnsignedRangeMin(Stride);
 
   // We assume either the stride is positive, or the backedge-taken count
   // is zero. So force StrideForMaxBECount to be at least one.
   APInt One(BitWidth, 1);
   APInt StrideForMaxBECount = IsSigned ? APIntOps::smax(One, MinStride)
                                        : APIntOps::umax(One, MinStride);
 
   APInt MaxValue = IsSigned ? APInt::getSignedMaxValue(BitWidth)
                             : APInt::getMaxValue(BitWidth);
   APInt Limit = MaxValue - (StrideForMaxBECount - 1);
 
   // 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 = ceil((max(MaxEnd, MinStart) - MinStart) / Stride)
   MaxEnd = IsSigned ? APIntOps::smax(MaxEnd, MinStart)
                     : APIntOps::umax(MaxEnd, MinStart);
 
   return getUDivCeilSCEV(getConstant(MaxEnd - MinStart) /* Delta */,
                          getConstant(StrideForMaxBECount) /* Step */);
 }
if (!PositiveStride) {
     //
     // a) IV is either nuw or nsw depending upon signedness (indicated by the
     //    NoWrap flag).
     // b) the loop is guaranteed to be finite (e.g. is mustprogress and has
     //    no side effects within the loop)
     // c) loop has a single static exit (with no abnormal exits)
     //
     // Precondition a) implies that if the stride is negative, this is a single
     // trip loop. The backedge taken count formula reduces to zero in this case.
     //
     // Precondition b) and c) combine to imply that if rhs is invariant in L,
     // then a zero stride means the backedge can't be taken without executing
     // undefined behavior.
     //
     // The positive stride case is the same as isKnownPositive(Stride) returning
     // true (original behavior of the function).
     //
-    // We want to make sure that the stride is truly unknown as there are edge
-    // cases where ScalarEvolution propagates no wrap flags to the
-    // post-increment/decrement IV even though the increment/decrement operation
-    // itself is wrapping. The computed backedge taken count may be wrong in
-    // such cases. This is prevented by checking that the stride is not known to
-    // be either positive or non-positive. For example, no wrap flags are
-    // propagated to the post-increment IV of this loop with a trip count of 2 -
-    //
-    // unsigned char i;
-    // for(i=127; i<128; i+=129)
-    //   A[i] = i;
-    //
-    if (PredicatedIV || !NoWrap || isKnownNonPositive(Stride) ||
-        !loopIsFiniteByAssumption(L) || !loopHasNoAbnormalExits(L))
+    if (PredicatedIV || !NoWrap || !loopIsFiniteByAssumption(L) ||
+        !loopHasNoAbnormalExits(L))
+      return getCouldNotCompute();
+
+    // This bailout is protecting the logic in computeMaxBECountForLT which
+    // has not yet been sufficiently auditted or tested with negative strides.
+    // We used to filter out all known-non-positive cases here, we're in the
+    // process of being less restrictive bit by bit.
+    if (IsSigned && isKnownNonPositive(Stride))
       return getCouldNotCompute();
 
     if (!isKnownNonZero(Stride)) {
       // If we have a step of zero, and RHS isn't invariant in L, we don't know
       // if it might eventually be greater than start and if so, on which
       // iteration.  We can't even produce a useful upper bound.
       if (!isLoopInvariant(RHS, L))
         return getCouldNotCompute();

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

for.body:                                         ; preds = %entry, %for.body
   %cmp = icmp ult i8 %add, 128
   br i1 %cmp, label %for.body, label %for.end
 
 for.end:                                          ; preds = %for.body, %entry
   ret void
 }
 
 ; CHECK-LABEL: Determining loop execution counts for: @ult_129_unknown_start
-; CHECK: Loop %for.body: Unpredictable backedge-taken count
-; CHECK: Loop %for.body: Unpredictable max backedge-taken count
+; CHECK: Loop %for.body: backedge-taken count is (((127 + (-1 * (1 umin (127 + (-1 * %start) + (-128 umax (-127 + %start)))))<nuw><nsw> + (-1 * %start) + (-128 umax (-127 + %start))) /u -127) + (1 umin (127 + (-1 * %start) + (-128 umax (-127 + %start)))))
+; CHECK: Loop %for.body: max backedge-taken count is 1
 
 define void @ult_129_unknown_start(i8 %start) mustprogress {
 entry:
   br label %for.body
 
 for.body:                                         ; preds = %entry, %for.body
   %i.05 = phi i8 [ %add, %for.body ], [ %start, %entry ]
   %add = add nuw i8 %i.05, 129