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

[Ehsan Amiri via llvm-commits]

amehsan wrote:

Thanks @sjoerdmeijer . This is what I can say in response to your remarks:

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

Yes, I wrote a proof for Symbolic RDIV once. I can rewrite it. I have looked at two weak SIV tests and it seems doable. In general for anything linear, I expect this to be doable.

> 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?

That is my impression too. I can try to prepare a patch this Friday.


>If I am reading that right, my proposal would be to delay the introduction of monotonicity until we actually we need it, and focus on getting these tests correct without monotonicity. Does that make sense?

This makes sense to me. We can introduce monotonicity when needed. The plan is to enable the tests one by one, so for each test we can check what is the best approach.

That aside, even when using  monotonicity domain we need proofs of correctness. Let's look at the Strong SIV: for the case that we rely on monotonicity in the entire domain, the proof should be simpler than mine. But the other case, we need essentially the same proof (part 1 of my proof).

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