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

[Ryotaro Kasuga via llvm-commits]

kasuga-fj wrote:

Let me first clear up a misunderstanding.

> The strong disagreement expressed earlier to solve this in the current framework without monotonicity evolved around:
> 
> > I'm strongly disagree with this direction because:

The disagreement is not about resolving the existing issues without monotonicity. The approach 1 and 2 I mentioned are different topic from monotonicity. What I meant is that, we can address some of the overflow issues without either monotonicity or the proof, so writing proofs is unnecessary in the first place. Additional constraints like `0 <=s BTC` are also unnecessary in that case.

My current position about monotonicity is: it's not mandatory, but I *think* it's a good property to have to make the pass more robust. The reasons for this are as described in my previous comment. I don't know whether this will be believed, but if this still doesn’t convince folks, I was actually starting to think about dropping monotonicity at this point.

---

> > Regarding the altenatives, I think emitting runtime assumptions is worth to pursue. Not sure if this will be helpful, but here is my thoughts:
> > DA already has functionality for runtime predicates, but I don’t want to enhance it, at least until the existing bugs are fixed.
> 
> That is a very strong statement, and I don't know how to read that. We don't know when all bugs are fixed, so does this now means I am blocked to make progress if I do want to progress this?

Thanks for pointing this out. To be frank, my first reaction when reading this was: "Wow, is this statement very strong?". I genuinely didn’t think I was saying anything strong at all. This is just my personal preference, and I had no intention to block anyone. Is this a matter of wording? If so, I really appreciate you pointing it out.

That said, I intended to aim for consensus. In my earlier comment, I meant to say that monotonicity is not mandatory (and thus could be dropped), though it it seems I may have caused the misunderstanding I mentined above.

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