[llvm] [DA] Add tests for nsw doesn't hold on entier iteration (PR #162281)

[Ryotaro Kasuga via llvm-commits]

kasuga-fj wrote:

To move the discussion forward, I’d like to return to the original topic.

Short summary: I feel that the domain of monotonicity should be defined more clearly.

### Problems

Currently the [definition](https://github.com/llvm/llvm-project/blob/e79c7c18d675a10e03c2942960d68f02f1a54f1f/llvm/lib/Analysis/DependenceAnalysis.cpp#L232-L239) states:

```
/// 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.
```

With the current definition, when we say that a SCEV is monotonic, we must guarantee that it is monotonic over the entire iteration domain. Therefore, treating the following case (which is what this PR changes) as monotonic is indeed incorrect.

```c
for (i = 0; i < INT64_MAX - 1; i++)
  if (i < 1000)
    for (j = 0; j < 2000; j++)
      a[i + j] = 0;
```

That said, the followings would also be true:

- Properly filtering out such cases requires a fair amount of effort
- Requiring monotonicity over the entire iteration domain would be too strong for some dependence tests

### Classification of dependence tests

I think the existing dependence tests can be classified roughly into the following two categories:

- Category 1: Tests that effectively compare the minimum and maximum values of two subscripts
    - E.g., The former part of Strong SIV, Symbolic RDIV
- Category 2: Tests that analyze something based on modulo operations
    - E.g., The latter part of Strong SIV, Exact XXX (in other words, GCD test)

For Category 1, I think we still need to ensure monotonicity over the entire iteration domain. On the other hand, for Category 2, the monotonicity requirement can be relaxed.

### Approach

My proposal is to introduce a new kind of domain of monotonicity in addition to the entire iteration domain. For example, we can call it the "effective iteration domain". The entire iteration domain is:

$[0, \mathrm{BTC}_1] \times [0, \mathrm{BTC}_2] \times \cdots \times [0, \mathrm{BTC}_N]$

The effective iteration domain can be written as follows:

$[L_1, U_1] \times [L_2, U_2] \times \cdots \times [L_N, U_N]$

where $0 \leq L_k \leq U_k \leq \mathrm{BTC}_k$ for each $k$. Essentially, monotonicity over the effective iteration domain should be what current nsw-based monotonicity checks guarantee. Note that

- I don't intend to compute the values of $L_k$ and $U_k$. We only know that such values exist, but we don't know what they are.
- For each $i_k$, it's important that the range $[L_k, U_k]$ is a contiguous range.
    - To prevent case like https://github.com/llvm/llvm-project/pull/162281#issuecomment-3516217589.

For tests in Category 1, we still require monotonicity over the entire iteration domain. But for tests in Category 2, probably monotonicity over the effective iteration domain is sufficient.

Regarding the implementation, we will likely define something like the following:

```c++
enum Domain {
    EntireIteration,
    EffectiveIteration
};

enum MonotonicityType {
    Unknown,
    Invariant,  // maybe unnecessary?
    MultivariateSignedMonotonic,
    MultivariateUnsignedMonotonic,  // not yet implemented
};

struct Monotonicity {
    Domain D;
    MonotonicityType MT;
};
```

To make the implementation easier:

- Ensure that the existing nsw-based monotonicity checks guarantee monotonicity over the effective iteration domain
    - Theoretically, if the loops are perfectly nested, we can prove monotonicity over the entire iteration domain. But I don't want to implement perfect loop nest checks for now.
- If all involved values except for the induction variables are constant, we can check monotonicity without relying on nsw. If we can prove monotonicity in this way, we can say that the SCEV is monotonic over the entire iteration domain.
    - E.g., in the following case, we can prove monotonicity over the entire iteration domain, by simply checking `2*100 + 3*200 + 5` doesn't overflow.
    ```c
    for (i = 0; i < 100; i++)
      if (i < 50)
        for (j = 0; j < 200; j++)
          A[2*i + 3*j + 5] = 0;
    ```

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