[PATCH] D13686: [SCEV] Teach SCEV some axioms about non-wrapping arithmetic

[Sanjoy Das via llvm-commits]

sanjoy added inline comments.

================
Comment at: include/llvm/Analysis/ScalarEvolution.h:579
@@ -578,1 +578,3 @@
 
+    /// Try to prove the condition described by "LHS Pred RHS" by ruling out
+    /// certain kinds of overflow.
----------------
reames wrote:
> The naming of this seems really odd.  Possibly: ViaIntegerFacts?
> 
> "certian kinds of overflow" is confusing in the comment.  
`ViaIntegerFacts` seems just as vague as (if not more) `ViaNoOverflow` to me. :)  There are many integer facts that we can use without proving no overflow (e.g. transitivity of `<`), but this function focuses on using integer facts that are not valid if the the operation in `LHS` / `RHS` overflow.  I can work this into the comment if you think that'll help.  I can also drop the "certain kinds" bit form the comment and just say "ruling out integer overflow".


================
Comment at: lib/Analysis/ScalarEvolution.cpp:7177
@@ +7176,3 @@
+
+  auto MatchBinaryAdd = [this](const SCEV *Result, const SCEV *X, APInt &OutY,
+                               SCEV::NoWrapFlags ExpectedFlags) {
----------------
reames wrote:
> A comment explaining what this matches would help.  
Will do.

================
Comment at: lib/Analysis/ScalarEvolution.cpp:7199
@@ +7198,3 @@
+  case ICmpInst::ICMP_SLE:
+    // X s<= (X + C)<nsw> if C >= 0
+    if (MatchBinaryAdd(RHS, LHS, C, SCEV::FlagNSW) && C.isNonNegative())
----------------
reames wrote:
> Notation wise: X s<= (X +<nsw> C) if C >= 0 would be far more clear.
`(A + B)<nsw>` is the standard notation used when printing SCEV expressions, so I'd rather keep it that way for consistency.


http://reviews.llvm.org/D13686