[PATCH] D12948: [SCEV] Teach SCEV that A < B => (A+K) < (B+K) on no overflow.
Sanjoy Das via llvm-commits
llvm-commits at lists.llvm.org
Wed Sep 23 22:27:16 PDT 2015
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
More information about the llvm-commits
mailing list