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

[Ryotaro Kasuga via llvm-commits]

================

----------------
kasuga-fj wrote:

The test cases themselves simply show that the current monotonicity check is not along with its definition. This PR doesn't say anything about how to fix the problem (while I have some thoughts as mentioned). I'm really not sure what you are requesting here.

---

I've read your proof and found several issues:

- You are conflating signed comparisons with unsigned comparisons. A backedge-taken count can be larger than `2^63 - 1`. So `a * (y - x)`, or even `y - x` may overflow in a signed sense.
- Therefore `|a| (y - x) = |c - d|` is non-trivial.
- You are implicitly assuming `|a| * BTC` doesn't overflow.

So I don't think your proof is correct. Also this is why I don't bother writing out the proof, and I don't trust such proofs written by humans. Mistakes like this can easily occur, and it's also difficult to continually maintain consistency between the implementation and the proof. At the very least, I think this type of proof should be checked by a proof assistant.

---

It seems that you want to use the term "no-wrap", but it's not clear to me what arithmetic is guaranteed not to wrap. Note that both "monotonicity in execution space" and `nsw` don't imply `a*i` doesn't overflow. Monotonicity only means `a*i + c < a*(i + 1) + c < ...`. I don't really understand what is improved by changing the terminology.


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