[PATCH] D31238: [ScalarEvolution] Re-enable Predicate implication from operations

[Sanjoy Das via Phabricator via llvm-commits]

sanjoy accepted this revision.
sanjoy added a comment.
This revision is now accepted and ready to land.

lgtm with minor comments (i.e. fix these and check in without further review).



================
Comment at: lib/Analysis/ScalarEvolution.cpp:8549
+                                             unsigned Depth) {
+  // We want to avoid hurting the compile time with analysis of too big trees.
+  if (Depth > MaxSCEVOperationsImplicationDepth)
----------------
How about asserting here that

 - The types of `LHS` and `RHS` match
 - The types of `FoundLHS` and `FoundRHS` match

?


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8563
+  auto GetOpFromSExt = [&](const SCEV *S) {
+    if (auto *Ext = dyn_cast<SCEVSignExtendExpr>(S))
+      return Ext->getOperand();
----------------
There is one enhancement possible here, please add that as a TODO: if `S` is a `SCEVConstant` then too you can cheaply "strip" the `sext` off the constant in some cases.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8586
+    // types of LHS and RHS do not match.
+    if (LHSAddExpr->getType() != RHS->getType())
+      return false;
----------------
Another TODO here would be that we can also do `RHS = GetOpFromSExt(RHS)` earlier to catch more cases.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8648
+      // least 3. If we divide it by Denominator <= 3, we will have at least 1.
+      // (Denominator - 1 <= FoundRHS) <=> (FoundRHS > Denominator - 2).
+      auto *DenomMinusTwo = getMinusSCEV(DenominatorExt, getConstant(Ty2, 2));
----------------
The code is correct, but the comment is wrong.  We only have the implication one way: `(FoundRHS > Denominator - 2) => (Denominator - 1 <= FoundRHS)`, since if `Denominator` is `INT_SMAX + 2` then `Denominator - 2` = `INT_SMAX`, but `Denominator - 1` = `INT_SMIN`.  For any `FoundRHS`, this means `Denominator - 1 <= FoundRHS` is `true`, but `FoundRHS > Denominator - 2` is `false`.

Secondly, the comment would be more readable if you write the comment with `FoundRHS` on the same side on both the antecedent and the consequent.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8661
+      // Anyways, the result is non-negative.
+      // (-Denominator <= FoundRHS) <=> (FoundRHS > -1 - Denominator)
+      auto *MinusOne = getNegativeSCEV(getOne(Ty2));
----------------
I think the issue mentioned for the previous comment above applies here as well.


================
Comment at: test/Analysis/ScalarEvolution/scev-division.ll:3
+
+declare void @llvm.experimental.guard(i1, ...)
+
----------------
I should have noticed in the previous iteration of the patch, but we should call these test files something more specific -- like `implied-via-division.ll` or something.  Also: the `scev-` prefix is redundant since we're in the `ScalarEvolution` directory (though I do see it used in a few other tests).


https://reviews.llvm.org/D31238