This is an archive of the discontinued LLVM Phabricator instance.

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

Authored by sanjoy on Sep 17 2015, 4:01 PM.

Diff Detail

Repository
rL LLVM

Event Timeline

sanjoy updated this revision to Diff 35045.Sep 17 2015, 4:01 PM
sanjoy retitled this revision from to [SCEV] Teach SCEV that A < B => (A+1) < (B+1) on no overflow..
sanjoy updated this object.
sanjoy added reviewers: atrick, reames, majnemer.
sanjoy added a subscriber: llvm-commits.
sanjoy updated this revision to Diff 35055.Sep 17 2015, 7:46 PM
  • add a test that had I had accidentally split into D12949
majnemer added inline comments.Sep 17 2015, 7:57 PM
lib/Analysis/ScalarEvolution.cpp
7369–7372 ↗(On Diff #35055)

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?

aadg added a subscriber: aadg.Sep 17 2015, 11:52 PM

Hi Sanjoy,

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 ?

Thanks,
Arnaud

In 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

lib/Analysis/ScalarEvolution.cpp
7369–7372 ↗(On Diff #35055)

As discussed on IRC, the => here is implication; so cases where !(A < B) don't matter.

sanjoy updated this revision to Diff 35132.Sep 18 2015, 1:57 PM
  • address review by Arnaud: handle addition by arbitrary constants, not just 1
sanjoy retitled this revision from [SCEV] Teach SCEV that A < B => (A+1) < (B+1) on no overflow. to [SCEV] Teach SCEV that A < B => (A+K) < (B+K) on no overflow..Sep 21 2015, 11:52 AM
hfinkel added inline comments.Sep 23 2015, 12:56 AM
lib/Analysis/ScalarEvolution.cpp
7299 ↗(On Diff #35132)

Remove final // line.

7400 ↗(On Diff #35132)

Can't this just be -RDiff?

7408 ↗(On Diff #35132)

Add some comment here that this is the overflow check mentioned above.

sanjoy updated this revision to Diff 35576.Sep 23 2015, 5:16 PM
sanjoy marked 3 inline comments as done.
  • Address Hal's review.
  • Generalize the transform a little bit -- A s< B => A + C s< B + C if B s< INT_MIN - C even if C is negative. Add a test case for the same.
sanjoy added inline comments.Sep 23 2015, 10:27 PM
lib/Analysis/ScalarEvolution.cpp
7367 ↗(On Diff #35576)

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
sanjoy updated this revision to Diff 35661.Sep 24 2015, 11:30 AM
  • clarify comment with a cleaner proof
sanjoy updated this revision to Diff 35662.Sep 24 2015, 11:34 AM
  • Fix for accidentally fat-fingering the last edit.
sanjoy updated this revision to Diff 35691.Sep 24 2015, 5:59 PM
  • Clarify comments a bit more and fix typos in comments. Only comments changed in this update.
hfinkel accepted this revision.Sep 25 2015, 12:26 PM
hfinkel edited edge metadata.

LGTM.

This revision is now accepted and ready to land.Sep 25 2015, 12:26 PM
This revision was automatically updated to reflect the committed changes.