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

[Ryotaro Kasuga via llvm-commits]

kasuga-fj wrote:

> The way I see it now is that there are two angles here for monotonicity: 1) required to fix correctness issues, 2) a nice abstractions to check some (pre)conditions. We also asked the "why monotonicity?" question because there was a proposal to fix up correctness issues in a different way, i.e. addressing 1). After some more discussions, and Michael pointing out [this](https://github.com/llvm/llvm-project/issues/168823#issuecomment-3612636989) comment, my reasoning / understanding in a nutshell was, and I am quoting some parts:
> 
>  * "SIV is by definition is an expression of the form a*i+c"
>
>  * "Affine obviously also implies monotonic."
>
>  * you can check "whether it is no-wrap (for all values of a, i, and c)".

Maybe I'm also repeating myself: I also think that monotonicity is unnecessary to fix correctness issues in the ZIV / SIV / RDIV tests, and the quote above matches my understanding as well.

My (probably too pessimistic) concern is that the incorrect test (i.e., the Banerjee MIV test) will remain in the codebase merely disabled by default. This could cause confusion in the future, and in the worst case, the context discussed here might be lost and someone might enable it without knowing why it was disabled in the first place. Maybe writing some comments in the code would help mitigate this risk. Introducing an abstraction and clarifying the preconditions may be another way. Completely removing the incorrect test is also an option. In any case, I feel that simply disabling the test is a bit risky. That said, it would be fair to say that I'm being too pessimistic here.

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