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

[Ehsan Amiri via llvm-commits]

amehsan wrote:

I haven't read the full comment yet, but a point that I am going to mention in the issue that I have opened is this:

What we need to focus on is "no wrapping" property which can be divided to signed and unsigned categories. monotonicity is not a fundamental property that we need to care about. It just happens that the two are related (probably equivalent, but I am not sure yet) for linear functions.

When we want to prove that control-flow is irrelevant for the correctness of dependency test, all that we need is proving "no wrapping" property. To demonstrate this assume  we have a non-monotonic function; for example: assume we are checking the dependences between `A[i*i - 1]` and `A[0]` (all numbers interpreted as signed).  Also assume that  it is guaranteed that both operations, multiply and subtraction,  are `nsw` for values of `i` that the instruction is **executed** (not the entire domain).

The question that we need to answer is this: are there two values 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.

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.



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