[Mlir-commits] [mlir] [mlir][SCF] Tighten description of scf.for (PR #203713)

[Reinhard Stahn]

https://github.com/rainij updated https://github.com/llvm/llvm-project/pull/203713

>From f88e0617f19adf0e843c230b71c85f4deb54437a Mon Sep 17 00:00:00 2001
From: Reinhard Stahn <rainij36 at proton.me>
Date: Sat, 13 Jun 2026 16:14:36 +0000
Subject: [PATCH] [mlir][scf] Tighten description of scf.for

The previous description was vague in the case that the
one-past-the-last value for the induction variable is not representable
in the used integer type. Current passes implicitly exploit this by
implementing non-equivalent semantics (e.g. terminating vs
non-terminating loops).

We tighten the specification of `scf.for` by first stating the desired
ideal semantics, but deeming overflow undefined behavior. This fixes all
inconsistencies I am aware of.

Documentation only; no behavioral change.
---
 mlir/include/mlir/Dialect/SCF/IR/SCFOps.td | 33 +++++++++++++---------
 1 file changed, 20 insertions(+), 13 deletions(-)

diff --git a/mlir/include/mlir/Dialect/SCF/IR/SCFOps.td b/mlir/include/mlir/Dialect/SCF/IR/SCFOps.td
index 0b33ecb48b7f2..a455ae5a94e47 100644
--- a/mlir/include/mlir/Dialect/SCF/IR/SCFOps.td
+++ b/mlir/include/mlir/Dialect/SCF/IR/SCFOps.td
@@ -168,19 +168,26 @@ def ForOp : SCF_Op<"for",
        RecursiveMemoryEffects]> {
   let summary = "for operation";
   let description = [{
-    The `scf.for` operation represents a loop taking 3 SSA value as operands
-    that represent the lower bound, upper bound and step respectively. The
-    operation defines an SSA value for its induction variable. It has one
-    region capturing the loop body. The induction variable is represented as an
-    argument of this region. This SSA value is a signless integer or index.
-    The step is a value of same type but required to be positive, the lower and
-    upper bounds can be also negative or zero. The lower and upper bounds
-    specify a half-open range: the iteration is executed iff the comparison of
-    induction variable value is less than the upper bound and bigger or equal
-    to the lower bound.
-
-    By default, the integer comparison is signed. If the `unsignedCmp` unit
-    attribute is specified, the integer comparison is unsigned.
+    The `scf.for` operation represents a loop whose first three operands are the
+    lower bound, upper bound and step respectively. The operation has one region
+    capturing the loop body. The induction variable is represented as an
+    argument of this region.
+
+    Lower bound, upper bound, and step are interpreted as signed integers by
+    default, or as unsigned integers if the `unsignedCmp` unit attribute is
+    present. The step is required to be strictly positive.
+
+    The lower and upper bounds specify a half-open range, including the lower
+    bound but excluding the upper bound. More precisely, the semantics is
+    governed by the following two rules, where arithmetic is performed with
+    arbitrary precision:
+
+    The trip count `n` is `max(0, ceil((UB - LB) / Step))` and the induction
+    variable takes the values `LB + j·Step` for `j = 0, ..., n - 1` in that
+    order.
+
+    No-overflow condition: `LB + n·Step` must be representable in the type of
+    the induction variable. Otherwise the behavior is undefined.
 
     The body region must contain exactly one block that terminates with
     `scf.yield`. Calling ForOp::build will create such a region and insert