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

[Ehsan Amiri via llvm-commits]

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

----------------
amehsan wrote:

> * 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.

Signedness interpretation should be consistent everywhere in the analysis. So we either interpret all the numbers as signed and everything must have nsw flag, or everything is interpreted as unsigned and we must have nuw flags everywhere.

If we are working with signed numbers then `BTC` cannot be larger than `2^63-1`, as it has to be interpreted as signed. How is this reflected in the proof and in the code? if you have a large BTC then `a*i` at some point will cross the bounday of `2^63` and so `a*i` cannot have nsw flag. So monotonicity check will fail.

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