[llvm] [DA] Add initial support for monotonicity check (PR #162280)

[Ryotaro Kasuga via llvm-commits]

kasuga-fj wrote:

> I think it all started with #148435 and the observation that and an access with `i%2` results in SCEV `i1 {false,+,true}<%loop>` that toggles between values 0 and 1. I.e, it iterates through all points in its space, then wraps around. So, just for clarity and completeness, we are thus not necessarily talking about signed/unsigned wrapping behaviour from say the C/C++ language point of view, but just the SCEV wrapping behaviour to capture an access pattern like toggling between values 0 and 1 (and of course other similar patterns). I believe the sign extension of this i1 SCEV to i64 is problematic too, but maybe that is separate?

Yeah, we are talking about the SCEV wrapping behavior here, not C/C++ (or other languages) specific behavior. As for the sign extension, I'm not entirely sure if it's problematic, but it's certain that there are some issues in DA with handling of sign/zero extensions. I think at least `DependenceInfo::removeMatchingExtensions` needs to be fixed.

> > The idea of monoticity to capture the behaviour that we are not iterating through the whole iteration space again and again makes perfect sense. At this point, the following is also unclear to me:
> 
> > Notably, it is still unclear whether we should also have a category for unsigned monotonicity.
> 
> I.e., I do not see how unsigned monotonicity is going to be different, but I need to think a bit more about this. Related to this, I am also not in love with the name `MultiSignedMonotonic`, but I see how "Signed" was suggested in the earlier review, and I see how the different components capture the different aspects here. If we don't need to distinguish between signed/unsigned we could drop Signed but guess this is to be determined. At a minimum, at this point, I would like to see a more crisp definition of the 3 components `Multi`, `Signed`, and `Monotonicity`. It's kind of there, but spread out, and I would like to see it all captured just before the point where `MultiSignedMonotonic` is defined. Maybe we can just drop `Multi` if we define this property to hold for all SCEVs? I know this is a little bit bikeshedding, but if these terms are going to stick, it is worth discussing a bit. :-)

The fundamental problem is a bit more serious. We need to pay attention to wrappings, even if a value doesn't iterate through the *entire* space. For instance, `symbolicRDIVtest` assumes that `a*i + c` takes its minimum value when `i = 0` and its maximum value when `i = N-1` (`N-1` is the BTC) when `a > 0`. This assumption is valid only when `a*i + c` doesn't wrap. For example, consider the following conditions:

- `a = 2^61`
- `c = 0`
- `N = 6`
- The bitwidth of the integer type is 64
- All integers are interpreted as signed

Then the minimum value of `a*i + c` is `-2^63` (when `i = 4`) and the maximum value is `2^62 + 2^61` (when `i = 3`) so that `symbolicRDIVtest` can produce an incorrect result. I think this also answers your question about the necessity of distinguishing between signed and unsigned. If the integers are interpreted as unsigned, the minimum value is `0` (when `i = 0`) and the maximum value is `2^63 + 2^61` (when `i = 5`). So in this case using unsigned interpretation might be better, but it would make difficult to handle negative values.

As for the naming, I believe I wrote the intention of the name `MultiSignedMonotonic` in [the comment of the code](https://github.com/llvm/llvm-project/blob/da8859cb562b4887f1c5d28cfc2b7b3dc8d7062f/llvm/lib/Analysis/DependenceAnalysis.cpp#L208-L238). I'm not confident it’s written clearly, so I’d appreciate any feedback.

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