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

[Sjoerd Meijer via llvm-commits]

================
@@ -177,13 +189,192 @@ void DependenceAnalysisWrapperPass::getAnalysisUsage(AnalysisUsage &AU) const {
   AU.addRequiredTransitive<LoopInfoWrapperPass>();
 }
 
+namespace {
+
+/// The property of monotonicity of a SCEV. To define the monotonicity, assume
+/// a SCEV defined within N-nested loops. Let i_k denote the iteration number
+/// of the k-th loop. Then we can regard the SCEV as an N-ary function:
+///
+///   F(i_1, i_2, ..., i_N)
+///
+/// The domain of i_k is the closed range [0, BTC_k], where BTC_k is the
+/// backedge-taken count of the k-th loop.
+///
+/// A function F is said to be "monotonically increasing with respect to the
+/// k-th loop" if x <= y implies the following condition:
+///
+///   F(i_1, ..., i_{k-1}, x, i_{k+1}, ..., i_N) <=
+///   F(i_1, ..., i_{k-1}, y, i_{k+1}, ..., i_N)
+///
+/// where i_1, ..., i_{k-1}, i_{k+1}, ..., i_N, x, y in their domains.
+///
+/// Likewise F is "monotonically decreasing with respect to the k-th loop"
+/// if x <= y implies
+///
+///   F(i_1, ..., i_{k-1}, x, i_{k+1}, ..., i_N) >=
+///   F(i_1, ..., i_{k-1}, y, i_{k+1}, ..., i_N)
+///
+/// A function F with either monotonically increasing or decreasing with
+/// respect to the k-th loop is simply called
+/// "monotonic with respect to k-th loop".
+///
+/// A function F is said to be "multimonotonic" when it is monotonic with
+/// respect to all of the N loops.
+///
+/// Since integer comparison can be either signed or unsigned, we need to
+/// distinguish monotonicity in the signed sense from that in the unsigned
+/// sense. Note that the inequality "x <= y" merely indicates loop progression
+/// and is not affected by the difference between signed and unsigned order.
+///
+/// Currently we only consider monotonicity in a signed sense.
----------------
sjoerdmeijer wrote:

A lot of things have been discussed in the comments. I need to catch up on some, but that is my problem. What I was going to ask is this. I really like the clear descriptions so far, but can we add, or is it worth explaining a little bit more, the algorithm that determines monotonicity? That will be a high level description of course, but I feel explaining the concepts of looking at AddRec and the nowrap flags etc. is missing a little bit. 

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