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

[Sanjoy Das via llvm-commits]

sanjoy added a comment.

In http://reviews.llvm.org/D12948#248493, @aadg wrote:

>




> I'm no scev expert, so I'm most probably missing something here: why

>  limit ourselves to "A < B => (A+1) < (B+1)" when "A < B => (A+Cst) <

>  (B+Cst)" also holds --- assuming there are no overflows ?


You're right, on no overflow, "A < B => (A+Cst) < (B+Cst)" (with the caveat that Cst
be positive if the comparison is signed).

I was initially working with "(A+1) < (B+1)" because that's the case
that had shown up, and hence that was the case I cared about.  But
you're right -- given handing arbitrary constants is not much more
work, we should be handling those.  I've updated the patch to do the
same (uploading shortly).

> Thanks,

> Arnaud



================
Comment at: lib/Analysis/ScalarEvolution.cpp:7369-7372
@@ +7368,6 @@
+
+  // If we can prove B + 1 does not signed / unsigned overflow, then we can
+  // prove
+  //
+  //  A < B => (A + 1) < (B + 1)
+  //
----------------
majnemer wrote:
> Let's say I have the following:
>   A = 0x7FFFFFFF
>   B = 0x7FFFBC80
> 
> In this case, `B+1` does not signed overflow and  `A` is not less than `B`.
> 
> However, this results in the following:
>   A+1 = 0x80000000
>   B+1 = 0x7FFFBC81
> 
> Thus the claim is made false, `A+1` is now less than `B+1`.
> 
> However, the claim is valid if we can prove that `B+1` does not signed/unsigned overflow *and* `A+1` will not overflow in kind.
> 
> I'm no SCEV expert but it seems to me that the code is doing the right thing, is it only the comment that needs adjustment?
As discussed on IRC, the `=>` here is implication; so cases where `!(A < B)` don't matter.


http://reviews.llvm.org/D12948