[PATCH] D30887: [ScalarEvolution] Predicate implication from operations

[Sanjoy Das via Phabricator via llvm-commits]

sanjoy requested changes to this revision.
sanjoy added a comment.
This revision now requires changes to proceed.

One more round of comments.



================
Comment at: lib/Analysis/ScalarEvolution.cpp:8565
+      // Rules for division.
+      auto *Num = getSCEV(Op1);
+      auto *Denum = getSCEV(Op2);
----------------
mkazantsev wrote:
> sanjoy wrote:
> > mkazantsev wrote:
> > > sanjoy wrote:
> > > > Let's avoid creating SCEV expressions here (via `getSCEV` or `getAddExpr`).  One problem is that it may be a compile time hit.  They can also cause use to compute overly conservative trip counts, since this call to `isImpliedViaOperations` may have itself been done during a trip count computation, and invoking `getSCEV` may try to (recursively) compute the trip count of the same loop again which would cache a conservative `SCEVCouldNotCompute` (to avoid recursing infinitely).
> > > I have removed the call of "isKnownPredicate" that might request recursive recalculation of the same trip count; now we use more light-weight check that used to be "IsKnownPredicateFull" lambda. So now this problem should have gone.
> > > 
> > > As for the compile time issue, what is the alternative to using SCEV for Num/Denum/FoundRHS+ 1?
> > One possibility would be to put the actual core of the logic in `llvm::isImpliedCondition` (which is in ValueTracking), and then try to call into that helper from there.
> > 
> > That is, say the antecedent is `(sext i16 %t to i32) s< i32 44` and the consequent is `%s != 400`.  We could then ask ValueTracking `llvm::isImpliedCondition(i16 %t s< i16 44, %s != 400)` [0] and return whatever ValueTracking told us.
> > 
> > We will probably need to generalize the interface of ValueTracking's `llvm::isImpliedCondition` a bit though, but that should be fine.
> > 
> > [0] Using the fact that `(sext(A) s< sext(B)) == A s< B`.
> I noticed that Num never needs a new SCEV creation in good case, because all we want is to prove that it's SCEV is actually FoundLHS. thus, it and some type conversions have gone.
> 
> Now we only have SCEV creation left for Denum-related stuff (such as constructing -Denum and Denum + 1). Here I believe that we cannot get rid of it, because for using implied conditions interfaces we will have to construct those sum and neg in terms of values if not in terms of SCEVs.
> 
> To avoid reculsive recalculations in this last case, let's just reduce the scope of the optimization to Denum being a constant. In this case creating Denum+1, -Denum or type extensions will only require constants creation, and there is a very high chance that these contant SCEVs already exist.
Your point is solid.

What do you think about creating a helper called (say) `isSCEVSameAsValue(const SCEV *, const Value *)` that checks cheaply (i.e. without creating new SCEV expressions) if a `SCEV *` and `Value *` compute the same thing at runtime?  It would have to be best effort, but that's fine for now.

You can use this `getExistingSCEV` trick in that helper, and also use `ExprValueMap` to do the inverse.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8512
+
+  auto GetOpFromExt = [&](const SCEV *S) {
+    if (auto *Ext = dyn_cast<SCEVSignExtendExpr>(S))
----------------
This should be called `GetOpFromSExt`.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8527
+    return isKnownViaSimpleReasoning(Pred, S1, S2) ||
+           isImpliedCondOperandsHelper(Pred, S1, S2, OrigFoundLHS, FoundRHS);
   };
----------------
Can we avoid the recursion via `isImpliedCondOperandsHelper`?


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8539
+    auto IsSumGreaterThanRHS = [&](const SCEV *S1, const SCEV *S2) {
+      if (IsProvedViaContext(ICmpInst::ICMP_SGE, S1, getZero(RHS->getType())))
+        if (IsProvedViaContext(Pred, S2, RHS))
----------------
Why not just

```
return IsProvedViaContext(ICmpInst::ICMP_SGE, S1, getZero(RHS->getType()))) && IsProvedViaContext(Pred, S2, RHS);
```

?

Please also avoid using `Pred` in the second call to `IsProvedViaContext`, but use a literal `ICmpInst::ICMP_SGT` instead.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8571
+      auto *Num = getExistingSCEV(LL);
+
+      // Make sure that it exists and has the same type.
----------------
This is minor, and I'll understand if you don't want to change it, but let's call `Num` `Numerator`.  `Num` is too ambiguous -- it can also mean `Number` for instance.

Paradoxically, I think `N` and `D` is less ambiguous than `Num` and `Denum`. :)

I'd also call `Denum` `Denom` if you must use an abbreviation, since the full spelling is `Denominator`.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8586
+      // Try to prove the following rule:
+      // (Denum <= FoundRHS + 1) && (RHS <= 0) => (LHS > RHS).
+      auto *Next = getAddExpr(FoundRHSExt, getOne(Ty2));
----------------
Any reason why you need to check `Denum <= FoundRHS + 1` instead of `Denum < FoundRHS`?  Since `FoundRHS < FoundLHS`, `FoundRHS + 1` can't sign overflow, so the above two should be equivalent with `Denum < FoundRHS` being (slightly) faster since we're not adding.

Can you also add one or two lines of comment as an informal proof on why this is correct?

Same for the second rule.


https://reviews.llvm.org/D30887