[mlir][affine][Analysis] Add conservative bounds for semi-affine mods (#93576)

This patch adds support for computing bounds for semi-affine mod
expression to FlatLinearConstraints. This is then enabled within the
ScalableValueBoundsConstraintSet to allow computing the bounds of
scalable remainder loops.

E.g. computing the bound of something like:
```
// `1000 mod s0` is a semi-affine.
#remainder_start_index = affine_map<()[s0] -> (-(1000 mod s0) + 1000)>
#remaining_iterations = affine_map<(d0) -> (-d0 + 1000)>

%0 = affine.apply #remainder_start_index()[%c8_vscale]
scf.for %i = %0 to %c1000 step %c8_vscale {
  %remaining_iterations = affine.apply #remaining_iterations(%i)
  // The upper bound for the remainder loop iterations should be:
  // %c8_vscale - 1  (expressed as an affine map,
  // affine_map<()[s0] -> (s0 * 8 - 1)>, where s0 is vscale)
  %bound = "test.reify_bound"(%remaining_iterations) <{scalable, ...}>
}
```

There are caveats to this implementation. To be able to add a bound for
a `mod` we need to assume the rhs is positive (> 0). This may not be
known when adding the bounds for the `mod` expression. So to handle this
a constraint is added for `rhs > 0`, this may later be found not to hold
(in which case the constraints set becomes empty/invalid).

This is not a problem for computing scalable bounds where it's safe to
assume `s0` is vscale (or some positive multiple of it). But this may
need to be considered when enabling this feature elsewhere (to ensure
correctness).

0 files changed, 0 insertions, 0 deletions