[llvm] [DA] Rewrite the formula in the Strong SIV test (PR #179665)

[Ryotaro Kasuga via llvm-commits]

================
@@ -1353,38 +1331,55 @@ bool DependenceInfo::strongSIVtest(const SCEV *Coeff, const SCEV *SrcConst,
   assert(0 < Level && Level <= CommonLevels && "level out of range");
   Level--;
 
-  const SCEV *Delta = minusSCEVNoSignedOverflow(SrcConst, DstConst, *SE);
-  if (!Delta) {
-    Result.Consistent = false;
-    return false;
-  }
-  LLVM_DEBUG(dbgs() << "\t    Delta = " << *Delta);
-  LLVM_DEBUG(dbgs() << ", " << *Delta->getType() << "\n");
-
-  // check that |Delta| < iteration count
-  bool IsDeltaLarge = [&] {
-    const SCEV *UpperBound = collectUpperBound(CurSrcLoop, Delta->getType());
+  // Src: [a*0 + c1], [a*1 + c1], [a*2 + c1], ..., [a*BTC + c1]
+  // Dst: [a*0 + c2], [a*1 + c2], [a*2 + c2], ..., [a*BTC + c2]
+  //
+  // When 0 <=s a, we can prove independence if:
+  //
+  //   (a*BTC + c1 <s a*0 + c2) or (a*BTC + c2 <s a*0 + c1)
+  //
+  // When a <s 0, we can prove independence if:
+  //
+  //   (a*0 + c1 <s a*BTC + c2) or (a*0 + c2 <s a*BTC + c1)
+  //
+  // These can be combined by computing the smin and smax of the Src and Dst.
+  //
+  // FIXME: Currently the nowrap properties of Src and Dst are not checked.
+  // Therefore, evaluating them at the last iteration may produce incorrect
+  // results.
+  bool IsNoOverlap = [&] {
+    const SCEV *UpperBound = collectUpperBound(Src->getLoop(), Src->getType());
     if (!UpperBound)
       return false;
-
     LLVM_DEBUG(dbgs() << "\t    UpperBound = " << *UpperBound);
     LLVM_DEBUG(dbgs() << ", " << *UpperBound->getType() << "\n");
-    const SCEV *AbsDelta = absSCEVNoSignedOverflow(Delta, *SE);
-    const SCEV *AbsCoeff = absSCEVNoSignedOverflow(Coeff, *SE);
-    if (!AbsDelta || !AbsCoeff)
-      return false;
-    const SCEV *Product = mulSCEVNoSignedOverflow(UpperBound, AbsCoeff, *SE);
-    if (!Product)
-      return false;
-    return SE->isKnownPredicate(CmpInst::ICMP_SGT, AbsDelta, Product);
+
+    const SCEV *SrcBegin = SrcConst;
+    const SCEV *DstBegin = DstConst;
+    const SCEV *SrcEnd = Src->evaluateAtIteration(UpperBound, *SE);
+    const SCEV *DstEnd = Dst->evaluateAtIteration(UpperBound, *SE);
+    const SCEV *SrcMin = SE->getSMinExpr(SrcBegin, SrcEnd);
+    const SCEV *SrcMax = SE->getSMaxExpr(SrcBegin, SrcEnd);
+    const SCEV *DstMin = SE->getSMinExpr(DstBegin, DstEnd);
+    const SCEV *DstMax = SE->getSMaxExpr(DstBegin, DstEnd);
+    return SE->isKnownPredicate(ICmpInst::ICMP_SLT, SrcMax, DstMin) ||
+           SE->isKnownPredicate(ICmpInst::ICMP_SLT, DstMax, SrcMin);
   }();
----------------
kasuga-fj wrote:

> > No, DA can prove the independence of them.
> 
> Right, my example was incorrect. But the point is valid and the example can be modified easily.

(Forgot to mention about this comment)

I don't think it's easy. If you want to argue an advantage of your approach under the assumption of "nowrap property under certain conditions" (this concept is still unclear to me, though), you need to show an example that satisfies the followings:

- The nowrap properties holds *only* under certain conditions. Especially, the property doesn't hold in the entire iteration space.
- We can prove that the multiplication of the coefficient and the backedge-taken count doesn't overflow in a signed sense.
- We can prove `AbsDelta >=s Product`.

What comes to my mind is something like this, which is not a practical one:

```c
for (i = 0; i < (1 << 62) - 100; i++) {
  if (i < 10) {
    A[2*i] = 0;
    A[2*i + (INT64_MAX - 20)] = 1;
  }
}
```

In general, I don't think there are many real-world examples where we cannot prove the nowrap properties hold in the entire iteration space, but we can prove the product of the coefficient and the BTC doesn't overflow. In such cases, the BTC or the constant values of the addrecs would be very large constant.

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