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

Let me try to write down a neutral summary (as much as I can):

We have two approaches:

**Approach 1:** This PR. 
**Pros and Cons:** Simpler code.  Risk of correctness issue if SCEV changes in future.

**Approach 2:** Existing code (plus an additional Check that `isKnowNenNegative(BTC)` is true. 
**Pros and Cons:** More complex code. Correctness is proven.

The rest is my opinion (not neutral)

In my opinion, at this level of complexity, confidence about correctness is definitely more important. The other issue is that, in future, if we actually have the correctness problem, then we need to rediscover the existing method. Those of us who are here right now, may not be around 5 years from now or may not remember everything. The knowledge hidden in hundreds of thousands of  issues and PRs may not be easy to rediscover. Even the fact that this two approaches are different in terms of their assumptions may not be easy to realize. So from my point of view, the choice is clear. 


What I am trying to do right now is to look into the history and see if a similar decision has been made in the past? Learning from past decisions and reasoning could help us make a better decision. I checked a little already, will look more to see if I can find anything.

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