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

[Max Kazantsev via Phabricator via llvm-commits]

mkazantsev added inline comments.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8501
+  if (Pred == ICmpInst::ICMP_SLT)
+    return isImpliedViaOperations(ICmpInst::ICMP_SGT, RHS, LHS, FoundRHS,
+                                  FoundLHS);
----------------
mkazantsev wrote:
> sanjoy wrote:
> > The usual way to do this is
> > 
> > ```
> > if (Pred == ICmpInst::ICMP_SLT) {
> >   Pred = ICmpInst::ICMP_SGT;
> >   std::swap(LHS, RHS);
> >   std::swap(FoundLHS, FoundRHS);
> > }
> > ```
> > 
> > Actually, you should not need to do this. `ScalarEvolution::isImpliedCond` should be handling this case for you.
> I will check this. If you are right, checking "less" cases in switch of ScalarEvolution::isImpliedCondOperandsHelper seems redundant.
This is not true, we sometimes have "less" conditions at this point.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8532
+  if (auto *Operation = dyn_cast<SCEVAddExpr>(LHS)) {
+    // Should not overflow.
+    if (!Operation->hasNoSignedWrap())
----------------
sanjoy wrote:
> Did you consider putting this logic in `ScalarEvolution::isKnownPredicateViaNoOverflow`?
Actually isKnownPredicateViaNoOverflow already does a particular case of it, which is "X + C > X if C > 0". The point here is that I need the context of FoundLHS and FounrRHS for further proofs. For example, I want to prove thing like "1 + n / 2 > 1 if n > 1". The rule which is used in isKnownPredicateViaNoOverflow does not work here, because n/2 does not match with 0 or 1. It also is unable to prove that n/2 > 0, because for this we need the proof via operation that uses context.

For the same reason I don't want to split this into two patches, because the only real benefit of the rule for addition is that it can recursively invoke the rule for division with the same context, and vice versa. Without the division rule, this addition work simply duplicates the logic of "isKnownPredicateViaNoOverflow".

I have removed "isKnownPredicate" invocation from here to avoid potential recursion, replacing it with more light-weight check. But we cannot move it out of here due to this context restriction.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8551
+      // Now we know that at least one of the operands in non-negative. It
+      // implies that Op1 + Op2 >= min(Op1, Op2). If we prove that
+      // (Op1 > RHS) && (Op2 > RHS), then (Op1 + Op2) >= min(Op1, Op2) > RHS.
----------------
sanjoy wrote:
> This is probably too expensive to put in here (at the very least, this is risky from a compile time perspective).  How far can we get just by looking at the ranges for each of the inputs (i.e. via calling `getRange` and doing some manipulations on the returned ranges)?
Ok, I got rid of recursive checks.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8565
+      // Rules for division.
+      auto *Num = getSCEV(Op1);
+      auto *Denum = getSCEV(Op2);
----------------
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?


https://reviews.llvm.org/D30887