[llvm] [DA] Rewrite the formula in the Strong SIV test (PR #179665)

[Ryotaro Kasuga via llvm-commits]

kasuga-fj wrote:

Sorry, I'm really not sure your argument about SCEV. Based on your past comments (including your [Discourse post](https://discourse.llvm.org/t/scev-question-about-inferring-nsw-flags/89858)), I suspect there may be some fundamental misunderstanding about SCEV, though I’m not sure exactly what it is. The advantage you described for your approach simply doesn't make sense to me. I don't think further discussion will be productive, and I don't want to spend more time on this.

If you still believe your approach has an advantage with respect to future SCEV changes, please clarify the following points:

- What "the nowrap flags of **addrecs** under certain conditions" means.
- Why it is safe to employ context-sensitive nowrap flags in your approach.
- Under what circumstances your approach would be more beneficial than this one.

It's not directly related to this PR, but I'd also strongly recommend you to reread https://www.npopov.com/2023/10/03/LLVM-Scalar-evolution.html#nowrap-flags more carefully, at least to the extent that you can explain the points below:

- The difference between "inference" and "transformation" of the nowrap flags.
- What nowrap flags of addrecs actually mean.
    - In particular, which arithmetic operations are guaranteed not to overflow, and when.
- Why we cannot "transfer" the nowrap flags if the load/store isn't unconditionally executed.

---

> Not because I didn't know BTC must be non-negative, but because I didn't know we need the check even with the existing SCEV behavior.

This is really problematic. Most of the DA bugs we have found so far were due to misunderstandings of the behaviour of SCEV. "I didn’t know..." can be a serious issue.

> That said, the point here is that, no, this test is not a technical debt and a small code change in the future is not going to introduce another subtle corner case. That is why we need a proof. Otherwise , this kind of cocern is applicable to any implemention including the one proposed here.

As I’ve said repeatedly, the very existence of a proof is technical debt. It is extremely difficult to keep a proof up to date while preserving its correctness and consistency with the code. For example, how do we prevent a situation where the proof is accidentally modified and no longer proves the intended property? If you look at the codebase and/or its history, you can easily find several cases where the consistency between code comments and the actual code was broken.
There is no reason to adopt an approach that has so many edge cases that we cannot be confident in its correctness without a proof. We should strive to write code that is readable, maintainable, robust, and less likely to introduce defects (read [LLVM Code-Review Policy and Practices](https://llvm.org/docs/CodeReview.html)). Even the advantages of your approach, an adequate explanation has still not been provided.

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