[PATCH] D104066: [SCEV] Use knowledge of stride to prove loops finite for LT exit count computation

Philip Reames via Phabricator via llvm-commits llvm-commits at lists.llvm.org
Thu Jun 10 14:57:58 PDT 2021


reames created this revision.
reames added reviewers: nikic, mkazantsev, bjope.
Herald added subscribers: bollu, hiraditya, mcrosier.
reames requested review of this revision.
Herald added a project: LLVM.

This came up in the post commit review discussion of D103834 <https://reviews.llvm.org/D103834>.

The basic idea is that the general case was using a loop being finite by assumption to prove that step was non-zero.  Non-zero combined with NoWrap flags in turns proves the loop must exit before overflow occurs.  This change adds an explicit check for when the loop isn't known mustprogress, but we can directly prove that the step isn't zero.  This will mostly help non-C/C++ family languages, though it may benefit some C language test cases as well.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D104066

Files:
  llvm/lib/Analysis/ScalarEvolution.cpp
  llvm/test/Analysis/ScalarEvolution/trip-count-unknown-stride.ll


Index: llvm/test/Analysis/ScalarEvolution/trip-count-unknown-stride.ll
===================================================================
--- llvm/test/Analysis/ScalarEvolution/trip-count-unknown-stride.ll
+++ llvm/test/Analysis/ScalarEvolution/trip-count-unknown-stride.ll
@@ -106,5 +106,31 @@
   ret void
 }
 
+; Without explicit mustprogress, but the combination of nsw flags, the
+; condition being branched on, and the fact the step is known non-zero
+; is enough to prove this loop finite.
+
+; CHECK: Determining loop execution counts for: @non_zero_stride
+; CHECK: Loop %for.body4: backedge-taken count is ((-1 + (-1 * %arg) + ((%arg + %div) smax %n)) /u %div)
+; CHECK: Loop %for.body4: max backedge-taken count is -1
+
+define void @non_zero_stride(i64 %arg, i64 %div, i64 %n) {
+entry:
+  %assume = icmp sgt i64 %div, 0
+  call void @llvm.assume(i1 %assume)
+  br label %for.body4
+
+for.body4:                                        ; preds = %for.cond1.preheader, %for.body4
+  %i.020 = phi i64 [ %add5, %for.body4 ], [ %arg, %entry ]
+  %add5 = add nsw i64 %i.020, %div
+  %cmp2 = icmp slt i64 %add5, %n
+  br i1 %cmp2, label %for.body4, label %exit
+
+exit:
+  ret void
+}
+
+declare void @llvm.assume(i1)
+
 !8 = distinct !{!8, !9}
 !9 = !{!"llvm.loop.mustprogress"}
Index: llvm/lib/Analysis/ScalarEvolution.cpp
===================================================================
--- llvm/lib/Analysis/ScalarEvolution.cpp
+++ llvm/lib/Analysis/ScalarEvolution.cpp
@@ -11447,14 +11447,14 @@
     //
     // a) IV is either nuw or nsw depending upon signedness (indicated by the
     //    NoWrap flag).
-    // b) loop is single exit with no side effects.
-    //
+    // b) s is non-zero (and thus the loop is non-infinite)
     //
     // 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) implies that the unknown stride cannot be zero otherwise
-    // we have UB.
+    // Precondition b) implies that the loop can't be infinite (as a non-zero
+    // stride requires the comparison to eventually produce poison and we know
+    // this condition value reaches the branch exit)
     //
     // The positive stride case is the same as isKnownPositive(Stride) returning
     // true (original behavior of the function).
@@ -11471,8 +11471,12 @@
     // for(i=127; i<128; i+=129)
     //   A[i] = i;
     //
-    if (PredicatedIV || !NoWrap || isKnownNonPositive(Stride) ||
-        !loopIsFiniteByAssumption(L))
+
+    bool StrideNonZero = loopIsFiniteByAssumption(L) ||
+      isLoopEntryGuardedByCond(L, ICmpInst::ICMP_NE, Stride,
+                               getZero(Stride->getType()));
+
+    if (PredicatedIV || !NoWrap || isKnownNonPositive(Stride) || !StrideNonZero)
       return getCouldNotCompute();
   } else if (!Stride->isOne() && !NoWrap) {
     auto isUBOnWrap = [&]() {


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D104066.351275.patch
Type: text/x-patch
Size: 2945 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20210610/d686bc98/attachment.bin>


More information about the llvm-commits mailing list