[Mlir-commits] [mlir] [mlir][scf]: Add value bound for the computed upper bound of for loop (PR #126426)

[Matthias Springer]

================
@@ -93,9 +99,14 @@ struct ForOpInterface
     auto forOp = cast<ForOp>(op);
 
     if (value == forOp.getInductionVar()) {
-      // TODO: Take into account step size.
       cstr.bound(value) >= forOp.getLowerBound();
       cstr.bound(value) < forOp.getUpperBound();
+      AffineExpr tripCountMinusOne =
----------------
matthias-springer wrote:

Can you put a comment before this new block of code:
```
// iv <= lb + ((ub-lb)/step - 1)*step
```

Also add a comment that this bound does not render the above `iv < ub` obsolete because bounds where two constraint set dimensions are multiplied are not supported.

I'd also add an additional test case with a few extra index bbargs instead of all constants. You should be able to construct an example, where the value bounds analysis is unable to compute an UB (or prove an "LE" relation) because of the multiplication/division of two bbargs (which is not supported). Put a TODO as a comment to make clear that this is a known limitation.


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