[PATCH] D12948: [SCEV] Teach SCEV that A < B => (A+K) < (B+K) on no overflow.

[Sanjoy Das via llvm-commits]

sanjoy added inline comments.

================
Comment at: lib/Analysis/ScalarEvolution.cpp:7367
@@ +7366,3 @@
+
+  // If we can prove "FoundRHS < Limit - C" where Limit is
+  // (Pred == SLT ?  INT_MIN : 0) then we have:
----------------
There is actually a simpler proof for the signed case (I'll update the
comment with this tomorrow):

The proof hinges on `(A s< B) == ((A + INT_MIN) u< (B + INT_MIN))` `... (1)`
(this can be proved separately, but I'll assume this as an axiom for
now).

We'll also assume the unsigned variant of the implication, (
`A u< B u< -C => (A + C) u< (B + C)` `... (2)`) for this.

```
       A s< B s< INT_MIN - C
  <=>  (A + INT_MIN) u< (B + INT_MIN) u< -C   [ using (1) ]
  <=>  (A + INT_MIN + C) u< (B + INT_MIN + C) [ using (2) ]
  <=>  (A + INT_MIN + C + INT_MIN) s< (B + INT_MIN + C + INT_MIN) [ using (1) ]
  <=>  A + C s< B + C
```



http://reviews.llvm.org/D12948