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

[Ryotaro Kasuga via llvm-commits]

kasuga-fj wrote:

First of all, there are roughly two types of overflow issues in DA:

- Overflows of addrecs.
    - i.e., nowrap properties (nuw/nsw) of addrecs
- Overflows of intermediate calculations in dependence tests.
    - These happen when calling SCEV operations `getAddExpr`, `getMulExpr`, etc.

I believe we can address these two issues separately. Monotonicity is an abstraction to address the former, and it's not closely related to the latter. On the other hand, the domain of monotonicity, which this PR will introduce, is a concept that can affect both issues. Because of this, the two issues have often been conflated in the past. It would be helpful if we (myself included, of course) could keep this in mind.

---

> Therefore, for me, the preference would be to avoid adding new concepts if we can, i.e. the first test for me is "do we need this at all?".

> This seems to answer the question where we need monotonicity, i.e. we don't need it for the ZIV, SIV and RDIV tests which is the set of tests that we try to get correct for default enablement of DA.

Yes. If we only want to fix the existing DA bugs (including the MIV tests), **monotonicity is not needed at all**. I also agree that adding such a new concept is not free. However, I'd prefer to introduce it before enabling DA by default due to the following reasons:

- **Clarify the pass behavior**: The assumptions underlying DA have been vague, which makes it difficult to determine whether certain changes to DA are correct. I think this is a good opportunity to provide a formal definition of those assumptions, which I believe will help us maintain DA in the future.
- **Reduce risk of future bugs**: By separating `SCEVMonotonicityChecker` from DA itself, we can now test and verify the monotonicity checker independently. I've added several regression tests for it. These tests  may help prevent incorrect changes from being introduced in the future in the systematic way.

Resolving the existing DA bugs would be the minimum requirement for enabling DA by default. I believe that making DA more robust is also important, and introducing an abstraction layer would help achieve that. In light of this, I think it is reasonable to introduce monotonicity at this stage as well.

Some side notes:
- Current monotonicity checker is somewhat excessive. It's possible to simplify it and reduce LoC.
- My main concern is the possibility of making incorrect changes in an attempt to enable the MIV tests in the future. The motivation for adding an abstraction layer is to reduce that risk. Completely removing those tests would be another option.
- Even if we don't introduce monotonicity, we still need to consider something like "a domain of nuw/nsw" specifically for the MIV tests.

---

The suggestion I mentioned in Approach 1 in my previous reply is not closely related to monotonicity. It is about rewriting certain parts of the dependence tests into mathematically equivalent forms so that we can avoid having to account for most overflows in intermediate calculations (though not all of them). 

> * The proof is for the Strong SIV test. What about the other tests? Can they be salvaged too by adding extra checks/assumptions/constraints? I get the impression that this is the case, but is that right?
> * About the additional checks mentioned in that proof, they look minor. It only involves a BTC>=0 check and a NSW flag check. If this is the only thing, the fix looks very minor, is that right?

I'm strongly disagree with this direction because:

- This proof is tightly coupled with the implementation details. If the proof is written as a comment in the code, we must keep the code and the comment consistent. That is, every time we change the code, we also need to update the proof accordingly and re‑verify it. This is a maintenance burden, or maybe practically impossible. Notably, there are already several places in DA where the implementation is not consistent with the comments.
- Verifying the correctness of the proof itself is also not easy. It is noteworthy that @amehsan did not notice that the condition `0 <=s BTC` is being missed in the current implementation even while writing the proof. This is not meant as criticism, but I do not think human‑written proofs of implementation correctness are particularly reliable.
- The Strong SIV test is a somewhat special case because the necessary overflow checks are already in place. Other dependence tests are not so fortunate. To apply this approach to those tests, we would need to add overflow checks for every intermediate calculation. Adding many overflow checks throughout the codebase seems a bit risky to me.

My proposal in Approach 1 provides a solution that does not require writing such proofs. This is independent of monotonicity. It also doesn't require additional constraints such as `0 <=s BTC`. Since this approach avoids the risks mentioned above, I believe it is a better direction.

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