[SCEV] Further clarify comments regarding UB and zero stride

[reames]

Summary

Follow on to D109029. I realized we had no mention of mustprogrress in the comment (as it prexisted mustprogress in the codebase). In the process of adding it, I tweaked the preconditions into something I think is more clear. Note that mustprogress is checked in the code.

[nikic]

LG

llvm/lib/Analysis/ScalarEvolution.cpp

if (!PositiveStride) {
     // The backedge taken count for such loops is evaluated as -
     // (max(end, start + stride) - start - 1) /u stride
     //
     // The additional preconditions that we need to check to prove correctness
     // of the above formula is as follows -
     //
     // a) IV is either nuw or nsw depending upon signedness (indicated by the
     //    NoWrap flag).
-    // b) loop is single exit with no side effects.
-    // c) loop has no abnormal exits
-    //
+    // 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.
     //