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

[Max Kazantsev via Phabricator via llvm-commits]

mkazantsev added inline comments.


================
Comment at: lib/Analysis/ScalarEvolution.cpp:8527
+    return isKnownViaSimpleReasoning(Pred, S1, S2) ||
+           isImpliedCondOperandsHelper(Pred, S1, S2, OrigFoundLHS, FoundRHS);
   };
----------------
mkazantsev wrote:
> sanjoy wrote:
> > mkazantsev wrote:
> > > sanjoy wrote:
> > > > Can we avoid the recursion via `isImpliedCondOperandsHelper`?
> > > That's the point of the optimization! Sometimes we cannot simply prove that (a + b > c), but can do it via the context passed from division. And vice versa, if we have something like ( a / ( a / b + c)), we can prove the inner division using the context from outer division.
> > > 
> > > We are now not creating non-constant SCEVs, so all recursion will stay between the isImpliedCondOperandsHelper and isImpliedViaOperations, and we will always go down the syntax tree and never go into the infinite recursion. Actually its depth is not really big (not bigger than the depth of expressions).
> > Do you rely only recursing into `isImpliedViaOperations` or into the whole of `isImpliedCondOperandsHelper`?  If the former, I'd be much more comfortable if you:
> > 
> >  - Changed `IsProvedViaContext` to directly call into isImpliedViaOperations
> >  - Passed along a `Depth` parameter and cap it at a fairly low threshold (let's say 3?) to protect us from the truly pathological cases
> > 
> > We should implement the second point even if we need to recurse into `isImpliedCondOperandsHelper`, but if recursing into `isImpliedViaOperations` directly gives us what we want for cheap, we should just do that.
> > 
> > I'm not just worried about infinite recursion -- `isImpliedCondOperandsHelper` is called often enough that even a somewhat deep recursion here will slow things down.
> The logic here is following: the chain isImpliedViaOperations -> IsProvedViaContext -> isImpliedViaOperations goes down the expression tree to its operands. This process cannot be infinite since it always goes only UP by CFG and never comes down through Phis. Its depth doesn't exceed the depth of expression tree.
> 
> This recursive chain does not prove anything by itself. The terminal facts it uses are proved in isImpliedCondOperandsHelper (via range analysis etc). So we cannot throw it away, since it is the essential part for proving the lowest-level facts.
> 
> I can add a depth here to avoid analyzing too big expression trees, though.
UPD: I took a carefull look into it and now think that you are right. Seems that it is sufficient to have proofs without implication for terminal impressions which is done in isKnownViaSimpleReasoning. Context-biased analysis in helper seems redundant.


https://reviews.llvm.org/D30887