[Mlir-commits] [mlir] [mlir][scf] Fix scf.for value bounds for empty and unsigned loops (PR #226761)

[Dhairyashil R G]

https://github.com/dhairyashilRG updated https://github.com/llvm/llvm-project/pull/226761

>From 7dcfbb4f66fe72853e58f4a1ff8e7a96a467ead5 Mon Sep 17 00:00:00 2001
From: Dhairyashil R G <dhairyashil25 at gmail.com>
Date: Sun, 27 Sep 2026 11:37:03 +0530
Subject: [PATCH] [mlir][scf] Fix scf.for value bounds for empty and unsigned
 loops

The ValueBoundsOpInterface model of scf.for adds
result == init + ceildiv(ub - lb, step) * (yield - iter_arg).
This is wrong if the loop does not run, because the trip count is
max(0, ceildiv(ub - lb, step)), and for unsigned loops, because ub - lb
is computed as a signed difference. The induction variable bounds are
also added as signed constraints for unsigned loops.

Add the result equality only for signed loops with a provable ub > lb,
and do not add induction variable bounds for unsigned loops.

Assisted-by: Claude
---
 .../SCF/IR/ValueBoundsOpInterfaceImpl.cpp     | 13 +++++
 .../SCF/value-bounds-op-interface-impl.mlir   | 54 +++++++++++++++++++
 2 files changed, 67 insertions(+)

diff --git a/mlir/lib/Dialect/SCF/IR/ValueBoundsOpInterfaceImpl.cpp b/mlir/lib/Dialect/SCF/IR/ValueBoundsOpInterfaceImpl.cpp
index 496a7b036e65d19..171ab3f19e09afe 100644
--- a/mlir/lib/Dialect/SCF/IR/ValueBoundsOpInterfaceImpl.cpp
+++ b/mlir/lib/Dialect/SCF/IR/ValueBoundsOpInterfaceImpl.cpp
@@ -101,6 +101,16 @@ struct ForOpInterface
     if (dim.has_value() || isa<BlockArgument>(value))
       return;
 
+    // The closed form below holds only if the loop runs at least once (the
+    // trip count is not clamped at 0) and the bounds are compared as signed
+    // integers.
+    if (forOp.getUnsignedCmp() ||
+        !cstr.populateAndCompare(
+            forOp.getUpperBound(),
+            ValueBoundsConstraintSet::ComparisonOperator::GT,
+            forOp.getLowerBound()))
+      return;
+
     // `value` is result of `forOp`, we can prove that:
     // %result == %init_arg + trip_count * (%yielded_value - %iter_arg).
     // Where trip_count is (ub - lb) / step.
@@ -117,6 +127,9 @@ struct ForOpInterface
     auto forOp = cast<ForOp>(op);
 
     if (value == forOp.getInductionVar()) {
+      // The IV bounds are signed; unsigned loops are not modeled.
+      if (forOp.getUnsignedCmp())
+        return;
       return populateIVBounds(forOp.getLowerBound(), forOp.getUpperBound(),
                               forOp.getStep(), value, cstr);
     }
diff --git a/mlir/test/Dialect/SCF/value-bounds-op-interface-impl.mlir b/mlir/test/Dialect/SCF/value-bounds-op-interface-impl.mlir
index 60fe96d52d20b22..ab3e0b3989cb168 100644
--- a/mlir/test/Dialect/SCF/value-bounds-op-interface-impl.mlir
+++ b/mlir/test/Dialect/SCF/value-bounds-op-interface-impl.mlir
@@ -388,3 +388,57 @@ func.func @scf_forall_computed_upper_bound(%x: index) {
   }
   return
 }
+
+// -----
+
+// The loop does not run (5 to 2), so %0 is 3. ceildiv(ub - lb, step) is
+// negative and must not be used as the trip count: %0 is not 6.
+func.func @scf_for_result_empty() {
+  %c1 = arith.constant 1 : index
+  %c2 = arith.constant 2 : index
+  %c3 = arith.constant 3 : index
+  %c5 = arith.constant 5 : index
+  %c6 = arith.constant 6 : index
+  %0 = scf.for %iv = %c5 to %c2 step %c1 iter_args(%arg = %c3) -> index {
+    %1 = arith.subi %arg, %c1 : index
+    scf.yield %1 : index
+  }
+  // expected-error @below{{unknown}}
+  "test.compare"(%0, %c6) {cmp = "EQ"} : (index, index) -> ()
+  return
+}
+
+// -----
+
+// Unsigned loop from 2^64 - 1 to 5: the loop does not run, so %0 is 3. The
+// signed difference of the bounds must not be used as the trip count: %0 is
+// not 9.
+func.func @scf_for_unsigned_result() {
+  %c1 = arith.constant 1 : index
+  %c3 = arith.constant 3 : index
+  %c5 = arith.constant 5 : index
+  %c9 = arith.constant 9 : index
+  %lb = arith.constant -1 : index
+  %0 = scf.for unsigned %iv = %lb to %c5 step %c1 iter_args(%arg = %c3) -> index {
+    %1 = arith.addi %arg, %c1 : index
+    scf.yield %1 : index
+  }
+  // expected-error @below{{unknown}}
+  "test.compare"(%0, %c9) {cmp = "EQ"} : (index, index) -> ()
+  return
+}
+
+// -----
+
+// Unsigned loop: %iv is 1, 2^62 + 1 and 2^63 + 1. Signed bounds do not hold.
+func.func @scf_for_unsigned_induction_var() {
+  %c1 = arith.constant 1 : index
+  %ub = arith.constant -4611686018427387904 : index
+  %step = arith.constant 4611686018427387904 : index
+  scf.for unsigned %iv = %c1 to %ub step %step {
+    // expected-error @below{{could not reify bound}}
+    %0 = "test.reify_bound"(%iv) {type = "UB", constant} : (index) -> (index)
+    "test.some_use"(%0) : (index) -> ()
+  }
+  return
+}