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

[Philip Reames via Phabricator via llvm-commits]

reames added inline comments.


================
Comment at: llvm/lib/Analysis/ScalarEvolution.cpp:10725
+        return isImpliedCondOperands(FoundPred, LHS, RHS, FoundLHS, FoundRHS);
+  }
 
----------------
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.  


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

https://reviews.llvm.org/D110517