[Mlir-commits] [mlir] [mlir][scf] Fix the scf.while result reconstructed by upliftWhileToForLoop (PR #219617)

[Alessandro Potenza]

https://github.com/alepot55 commented:

I built this on `11e915f2b75d` and checked the arithmetic by folding it, which makes the bug show up as three wrong constants. Input shape, with the bounds constant so `canonicalize` collapses the reconstructed expression:

```mlir
func.func @uplift_const() -> index {
  %lb = arith.constant 5 : index
  %ub = arith.constant 5 : index
  %st = arith.constant 1 : index
  %0 = scf.while (%i = %lb) : (index) -> (index) {
    %c = arith.cmpi slt, %i, %ub : index
    scf.condition(%c) %i : index
  } do {
  ^bb0(%i: index):
    "test.test1"(%i) : (index) -> ()
    %n = arith.addi %i, %st : index
    scf.yield %n : index
  }
  return %0 : index
}
```

`mlir-opt -pass-pipeline='builtin.module(func.func(test-scf-uplift-while-to-for,canonicalize))'`:

| lb, ub, step | `scf.while` returns | main | with this PR |
| --- | --- | --- | --- |
| 5, 5, 1 | 5, the loop never runs | 4 | 5 |
| 5, 3, 1 | 5, the loop never runs | 2 | 5 |
| 0, 10, 3 | 12, the first index that fails `slt` | 9 | 12 |

So both halves of the change are load-bearing, and separately: dropping the `- 1` fixes the third row, and the `maxsi` is what fixes the second, where the signed division truncates to `-2` and the old expression walked the result backwards past `lb`. `mlir/test/Dialect/SCF` is green with the patch (45 passed, 1 expectedly failed).

Two remarks, neither blocking.

The description is right that the result is `lb + tripCount * step`, but it is worth saying in the code comment *why* that differs from the last executed index, since the `- 1` presumably looked correct to whoever wrote it: `scf.condition` forwards to the results on the iteration that fails, and that iteration has already incremented. The comment you added says the first half; the second half is the part that was misread.

The clamp is on the trip count rather than on the result. Those differ when `step` is negative, where `(ub - lb + step - 1) / step` is not a ceiling division at all. I could not find a guard in `upliftWhileToForLoop` that rejects a non-positive step, so if one can reach this code the expression was already wrong before your change and stays wrong after it, just differently. Worth a look, and if a negative step really is impossible here an assert or a comment saying so would save the next reader the same trip.

No reviewers are requested on this. @Hardcode84 wrote `UpliftWhileToFor.cpp` in #76108 and is the obvious person to ask.

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