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

[Ehsan Amiri 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);
   }();
----------------
amehsan wrote:

Thanks for the comments. I am familiar with the background of this issue. You are right that the recent attempt to address this issue requires clients to opt-in (https://github.com/llvm/llvm-project/pull/91961 , https://github.com/llvm/llvm-project/pull/91964 and probably some other patches). But:

1) DA has good reasons to opt-in if this feature is developed. Consider the following loop

```
for (int i = 0; i <1000; i++) {

  if (some condition) {
     A[3i] = ...
  }
  if (another condition) {
     A[3i+1] = ....
  }
}
```
Currently we cannot prove that these two memory accesses are independent. But if we can prove AddRecs are nowrap, then it will be possible. Why this could be useful? for example in loop distribution. Without nowrap flag for the AddRecs, we won't be able to prove that loop distribution is safe. But with AddRec flag, we can prove that the two memory accesses are independent and we can separate them in two different loops.

2) If there is enough motivation in the future, it might be possible to even change the SCEV, even if it breaks LAA. When LLVM switched from typed pointers to opaque pointers, many problems were introduced. But there was enough motivation in the community to go through it and fix all the issues. We cannot rule out that SCEV might change in the future. If/when there is a strong enough motivation people may decide to change the SCEV and fix all issues.

That said, we have two algorithms here. One of them has more limitations to the other and no clear advantage that I can see. It is not clear to me why we should choose the more limited algorithm.

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