[llvm] [LAA] Bound non-affine monotonic pointer expressions for runtime checks. (PR #210626)

[Florian Hahn via llvm-commits]

================
@@ -328,6 +328,64 @@ static bool evaluatePtrAddRecAtMaxBTCWillNotWrap(
   return SE.isKnownPredicate(CmpInst::ICMP_ULE, MaxOffset, DerefBytesSCEV);
 }
 
+/// Return true if \p S is known to be monotonically non-decreasing
+/// (in the unsigned sense, without unsigned wrap) across iterations of \p L.
+static bool isKnownNonDecreasingInLoop(const SCEV *S, const Loop *L,
+                                       ScalarEvolution &SE) {
+  if (SE.isLoopInvariant(S, L))
+    return true;
+
+  switch (S->getSCEVType()) {
+  case scUDivExpr: {
+    // Non-decreasing in the numerator when the divisor is loop-invariant.
+    const auto *UDiv = cast<SCEVUDivExpr>(S);
+    return SE.isLoopInvariant(UDiv->getRHS(), L) &&
+           isKnownNonDecreasingInLoop(UDiv->getLHS(), L, SE);
----------------
fhahn wrote:

Here we are only handling unsigned division, so I don't think the direction flips (unsigned values are interpreated as large unsigned values, so the following should still hold: `%x + 1 /u -4 >= %x u/ -4)`: https://alive2.llvm.org/ce/z/E8EFi9 (second set of proofs shows it does not hold for signed division)

I added a new test for this case `bitset_udiv_neg_4_symbolic_tc`

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