[llvm] [DA] Add tests for nsw doesn't hold on entier iteration (PR #162281)

[Michael Kruse via llvm-commits]

Meinersbur wrote:

> The question that we need to answer is this: are there values for `i` such that `i * i -1 = 0`. **_When there is no overflow in computation, the calculation of `i*i - 1` will have the same bitwise representation whether it is calculated in the ring of integers modulo `2^64` or it is calculated as integers._** and this tells us we can just solve the equation as integer and we are fine.

Are you suggesting using arbitrary-precision integers for solving dependency equations? Because this is why Integer Set Library and https://github.com/llvm/llvm-project/tree/main/mlir/include/mlir/Analysis/Presburger use arbitrary-precision integers.



> This is the basic idea of the proofs that we need to show control flow is irrelevant. But monotonicity is not the issue here. What is important here is "no wrapping" property as long as it is used in a consistent way (signed or unsigned) for each proof.

Monotonicity is supposed to give the additional guarantee that expression evaluations stay between the what it evaluates to in the first and last loop iterations, since otherwise to get the range of an arbitrary expression one would need to evaluate it for every in-between value. Everytime I see `getBackedgeTakenCount`, some monotonicity assumption probably went in. Two subscript expressions having non-intersecting ranges is the basic non-dependence test. The even stronger guarantee would be *linear*, but this would would also rule out SCEVExpr such as integer-division-by-constant and min/max. Indeed, ZIV, SIV, MIV classified subscripts don't contain them but are linear by defintion, but there are ther cases we might want to dependence-analyse.

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