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

[Ehsan Amiri via llvm-commits]

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

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

> I'm not sure why you are so obsessed with your proofs. I say they are unnecessary. If you want to save your time, I'd recommend pausing it for now.

Stop this kind of comments. Let's focus on the technical reasoning about the issue at hand. Most of your comment above is irrelevant to the technical discussion. 

As for the technical issue:

If we want to assume SCEV behavior is permanent, then always monotonicity will be held for all values of the induction variable.  Sure no special proof is needed and also no code change is needed. 

I suspect the existing SCEV behavior will be a headache for loop opts in the future and also it is something that is possible to change (and if that happens we better have the required proofs of correctness). If this is correct, it is better for us to stick to the existing implementation because it won't break if SCEV changes in the future.

I am going to go a bit deeper to see is there a reason to believe this behavior in SCEV cannot change in the future or not. 



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