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

[llvmlistbot at llvm.org]

llvmorg-github-actions[bot] wrote:


<!--LLVM PR SUMMARY COMMENT-->

@llvm/pr-subscribers-mlir

Author: Reinhard Stahn (rainij)

<details>
<summary>Changes</summary>

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.

---
Full diff: https://github.com/llvm/llvm-project/pull/203713.diff


1 Files Affected:

- (modified) mlir/include/mlir/Dialect/SCF/IR/SCFOps.td (+21-13) 


``````````diff
diff --git a/mlir/include/mlir/Dialect/SCF/IR/SCFOps.td b/mlir/include/mlir/Dialect/SCF/IR/SCFOps.td
index 0b33ecb48b7f2..c0d1ac501cc77 100644
--- a/mlir/include/mlir/Dialect/SCF/IR/SCFOps.td
+++ b/mlir/include/mlir/Dialect/SCF/IR/SCFOps.td
@@ -168,19 +168,27 @@ 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:
+
+    1. 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.
+    2. No-overflow condition: `LB + n*Step` must be representable in the type of
+       the induction variable. Otherwise the behavior is undefined. Leaving this
+       case undefined lets the loop be lowered to a plain increment-and-compare
+       on a single induction register without having to account for wraparound.
 
     The body region must contain exactly one block that terminates with
     `scf.yield`. Calling ForOp::build will create such a region and insert

``````````

</details>


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