[PATCH] D110517: [SCEV] Prove implication X <u Y, Y >=s 0 --> X <s Y

[Max Kazantsev via Phabricator via llvm-commits]

mkazantsev planned changes to this revision.
mkazantsev added inline comments.


================
Comment at: llvm/lib/Analysis/ScalarEvolution.cpp:10725
+        return isImpliedCondOperands(FoundPred, LHS, RHS, FoundLHS, FoundRHS);
+  }
 
----------------
reames wrote:
> nikic wrote:
> > This looks correct to me, but also rather ad-hoc -- it handles one out of multiple symmetrical patterns. For example, if we just swap both predicates (Pred == SGT and non-negative LHS) this will not trigger anymore. Or did that already get canonicalized away (in which case we should test it)?
> In line with the point Nikita makes, there's also an interesting case we should handle when RHS is known negative.  In that case, ult A, B && A < 0 is enough to prove slt A, B.  What's interesting to me is that we've already paid the cost of determining if A is known negative, so this becomes just a canonicalization.  
> 
> All of this is building on the equivalence:
> SLT A, B == (ULT A, B && signof(A) == signof(B)) || (A < 0 && B > 0)
> 
> (Note that ULT A, B + B > 0 => A > 0.)
> 
> Thinking about all this, it feels unfortunate that we're dropping to implication instead of rewriting based on equivalence.  At the same time though, I don't really see an obvious code structure to use the equivalence fact though, so maybe there's nothing we can do on that front.  
As for canonicalization, we try to canonicalize so that `LHS` matched `FoundLHS` or `RHS` matched `FoundRHS`, and we also try to move constant to right hand side. So in practice, I think in some cases it will be canonicalized so that constant (which is surely a known (non) negative) will be in RHS, but it's not guaranteed for all cases. I'll add more tests to see how it reacts on different equivalent code patterns, and if it's not general enough, I'll try to make the logic smarter.


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D110517/new/

https://reviews.llvm.org/D110517