[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:

> Currently we cannot prove that these two memory accesses are independent.

No, DA can prove the independence of them. SCEV already can infer nowrap flags in that case.
 
> If there is enough motivation in the future, it might be possible to even change the SCEV, even if it breaks LAA.

If that were to happen, we could think about it then.

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

See the description of this PR. The advantage of this approach is that it allows us to avoid dealing with many edge cases (such as overflow checks, computing absolute values, etc.), which makes the software more robust and easier to maintain. Also note that, at the moment, the current implementation requires more constraints than this one. With this approach, we can also handle cases where `a * BTC` may overflow, `BTC` may be negative, and so on.

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