[llvm] [DA] Introduce domain for monotonicity (PR #176367)

[Ryotaro Kasuga via llvm-commits]

kasuga-fj wrote:

> `%N` and `%N` can be `INT64_MAX` and `INT64_MAX - 1000` respectively, leading to an overflow in the expression `i + j` at `BTC` (even much earlier). In what sense is it "safe"? Is it because overflowing `i + j` would be undefined behavior? That is the case for the second example as well, even when ignoring the `i < 1000` guard, which as you mentioned have the same SCEVExpr.

Yeah, I'm referring to "safe" in the sense that the expression `i + j` will not overflow for all iterations of the loops. If I understand correctly, it's safe to assume that `%N` and `%M` are enough small to satisfy `%N + %M` doesn't overflow, since otherwise the program is UB. This property should hold because it doesn't have any guard like `i < 1000`.

> > In the latter case, it is obviously not safe, as it means `INT64_MAX + (INT64_MAX - 1000)`. Thus, DA needs more information than nowrap properties of addrecs.
> 
> As mentioned in my explanation, DA can just bail-out (return [confused](https://github.com/llvm/llvm-project/blob/114f3b530bae5a195234e3bd1c1328b38b39a000/llvm/include/llvm/Analysis/DependenceAnalysis.h#L143-L145)). Bailing out is necessarily correct.
> 
> I am not convinced about the practical relevance of this example -- in the sense that we should work hard on not bailing out in this case: loops with actual bounds close to `INT64_MAX` do not occur often in-the-wild. Unknown loop bounds such as `%N` which could be equal `INT64_MAX` are. To make this a problem we do not need nested loops or conditions:
> 
> ```c
> for (i = 0; i < N; ++i)
>   A[2 + i] = 0;
> ```
> 
> with `N = INT64_MAX`, the expression `2 + i` will overflow at the last iteration (same sample already discussed [here](https://discourse.llvm.org/t/rfc-a-new-pass-as-an-alternative-to-dependenceanalysis/88403/28?u=meinersbur)). IMHO the only way out here is adding a runtime check/assumption combined with LoopVersioning, so we only execute the optimized code with values of `N` that we know do not cause overflow.
> 
> If `N` is replaced with a constant `INT64_MAX`, I have not concern with bailing out in such cases: That execution would always cause an overflow of the `2 + i` expression. Even when adding a guard `if (i < INT64_MAX-1)` for the overflow to not occur, my original statement applies: I don't think this pattern occurs sufficiently often in-the-wild to be concerned about bailing out.

What I've been concerned about all along is the Banerjee MIV test. Roughly speaking, it computes the lower and upper bounds of a nested addrec by recursively evaluating it at 0 or `BTC`. My question is whether this is actually sound. If the addrec is not nested, then the situation should be simple -- just checking `nsw` (or `nuw`) of the addrec is enough. However, as the name "MIV" (Multiple Index Variable) suggests, the Banerjee MIV test is intended for nested addrecs. What I tried to point out with my previous examples is that, in the former case, applying the Banerjee MIV test appears to be sound, whereas in the latter case it is clearly not, even though the information carried by both addrecs is exactly the same. If we determined to bail out in such unclear cases, then this test would almost always return `confused`, which makes it less useful.

I don't think your example is particularly relevant to my concern, and in general I agree with you about loop-versioning. In practice, "we know `N` is small enough that `2 + i` does not overflow" should be more or less equivalent to saying that "the addrec `{2,+,1}` has `nsw`." If we cannot prove no-wrap, we can simply bail out or add runtime checks, as you suggested. If I understand correctly, LoopAccessAnalysis performs similar reasoning.

So, again, my main concern is about the soundness of the Banerjee MIV test for nested addrecs. What `nsw`/`nuw` mean for nested addrecs is not very clear to me. That said, I'm not sure whether it's worth putting effort into this. IMHO this test is too risky to use in practice.

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