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

[Ehsan Amiri via llvm-commits]

amehsan wrote:

> For the remaining parts, I'd strongly recommend you to read the code. I think Symbolic RDIV is a good one. It assumes that an addrec takes its minimum value at the first iteration and maximum value at the last iteration if the coefficient is non-negative. I think it's clear that "an addrec doesn't wrap when it's executed" is insufficient

OK. I give you a proof for the case that you mentioned. Note that we are talking about a mathematical problem. If you believe my proof is incorrect, I would be more than happy to see a counterexample and learn from it.

Note that in addition to “an addrec doesn’t wrap when it’s executed” we also need computations inside DA code to not overflow. We have already fixed a couple of bugs related to that. So that should not be a controversial assumption.

Now let’s focus on the  case of non-negative coefficients in Symbolic RDIV.

Assume we have `a1 * i + c1` and `a2 * j + c2`. Note that Symbolic RDIV calculates both `c1 – c2` and  `c2-c1` so let’s interpret the numbers as signed, otherwise one of the two subtractions will overflow (Unless `c1 == c2`). (There are probably ways to make it work for unsigned numbers but I don’t think that is a concern here).

Also Note that `a1 * N1` and `a2 * N2` are two multiplications performed in DA code. If we cannot prove they do not overflow DA cannot be correct. (Similar to the bugfix for StrongSIV that Alireza contributed and you reviewed). So it is safe to assume that these two multiplications do not overflow. Also the test assumes starting value of `i` and `j` is zero.

Now let’s proceed the proof by contradiction. Let’s say there are two executed values of `x` (for `i`) and `y` (for `j`) such that `a1 *x + c1 == a2 *y + c2` but Symbolic RDIV proved independence. There are two possible scenarios:

Case 1:  `a1 * N1 < c2 – c1` and so we (supposedly incorrectly) proved independence. Note that from our assumptions about non-overflowing computations we can conclude `a1 * x + c1 <= a1 * N1 + c1 ` (`x` cannot be more than `N1`)  So we have `a1 * N1 + c1 < c2`  it is ok to move `c1` because we know there is no overflow in the left hand side computations. But since `a1, N1, and x` are non-negative numbers we have `a1 * x + c1 < c2`. And since `a2 and y` are non-negative numbers we conclude `a1 * x + c1 < a2  * y+  c2`. 

I haven’t written down the proof for Case 2 but I believe it will work out similarly. The key point is this: All the computations used in the proof are either computations of executed subscript or computations inside the DA. Everything else is irrelevant.

If this is incorrect, please give me a counterexmple. 


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