[llvm] [SCEV] Update comment for check BE formula in howManyLT (NFC) (PR #219170)

[Nikita Popov via llvm-commits]

================
@@ -13560,35 +13560,34 @@ ScalarEvolution::howManyLessThans(const SCEV *LHS, const SCEV *RHS,
                        MaxBECount, false /*MaxOrZero*/, Predicates);
     }
   } else {
-    // 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.
+    // Let End = max(RHS,Start).  We use the expression (End-Start)/Stride to
+    // describe the backedge count: if the backedge is taken at least once then
+    // End is RHS, and if not End is Start so we get a backedge count of zero.
     auto *OrigStartMinusStride = getMinusSCEV(OrigStart, Stride);
     assert(isAvailableAtLoopEntry(OrigStartMinusStride, L) && "Must be!");
     assert(isAvailableAtLoopEntry(OrigStart, L) && "Must be!");
     assert(isAvailableAtLoopEntry(OrigRHS, L) && "Must be!");
-    // Can we prove (max(RHS,Start) > Start - Stride?
+    // Can we prove Start - Stride < Start and Start - Stride < RHS?
     if (isLoopEntryGuardedByCond(L, Cond, OrigStartMinusStride, OrigStart) &&
         isLoopEntryGuardedByCond(L, Cond, OrigStartMinusStride, OrigRHS)) {
       // In this case, we can use a refined formula for computing backedge
       // taken count.  The general formula remains:
-      //   "End-Start /uceiling Stride" where "End = max(RHS,Start)"
+      //   "End-Start /uceiling Stride"
       // We want to use the alternate formula:
-      //   "((End - 1) - (Start - Stride)) /u Stride"
+      //   "((RHS - 1) - (Start - Stride)) /u Stride"
       // Let's do a quick case analysis to show these are equivalent under
-      // our precondition that max(RHS,Start) > Start - Stride.
-      // * For RHS <= Start, the backedge-taken count must be zero.
-      //   "((End - 1) - (Start - Stride)) /u Stride" reduces to
+      // our preconditions that Start - Stride is below both Start and RHS.
+      // * For RHS <= Start (End is Start), the backedge-taken count must be
+      //   zero.
+      //   "((End - 1) - (Start - Stride)) /u Stride" is <=
----------------
nikic wrote:

```suggestion
      //   "((RHS - 1) - (Start - Stride)) /u Stride" is <=
```
Should be the starting point here. And it's not clear how the rest follows from that starting point.

https://github.com/llvm/llvm-project/pull/219170