[PATCH] D12073: Make ScalarEvolution::isKnownPredicate a little smarter

[hfinkel@anl.gov via llvm-commits]

hfinkel added a comment.

In http://reviews.llvm.org/D12073#225873, @sanjoy wrote:

> I'd solve this differently -- if I understand the problem correctly, you should really only need to teach SCEV that `{0,+,1}<nsw>` is `slt` `{1,+,1}<nsw>` (or something similar to that) in `isImpliedCondOperandsHelper`.


That's correct (but it triggers in some other cases too); I need to look at this in more detail, but a quick check reveals that for this code:

  $ cat /tmp/t.c
  void foo (int *a, int *b, int n) {
    for (int i = 0; i < n; ++i) {
      if (i > n)
        a[i] = b[i] + 1;
    }
  }

these statements trigger to do the following:

- proving that {0,+,1}<nuw><nsw><%for.body> sle {1,+,1}<nuw><nsw><%for.body> (the subtraction simplifies to -1)
- proving that (sext i32 %n to i64) sle (1 + (sext i32 %n to i64))<nsw> (again, the subtraction simplifies to -1)

for this code (which differs from the above only by the +4):

  $ cat /tmp/t4.c
  void foo (int *a, int *b, int n) {
    for (int i = 0; i < n; ++i) {
      if (i > n + 4)
        a[i] = b[i] + 1;
    }
  }

this code is used to:

- prove that %n sle (4 + %n) (the subtraction simplifies to -4)
- prove that {0,+,1}<nuw><nsw><%for.body> sle {1,+,1}<nuw><nsw><%for.body> (the subtraction simplifies to -1)

In the pr17473.ll test case, the statements trigger to:

- prove that 0 sle {1,+,1}<%for.body> (the subtraction simplifies to {-1,+,-1}<%for.body>
- prove that 127 sle {-2,+,-1}<%for.body> (the subtraction simplifies to {-127,+,1}<%for.body>)

That last one does indeed seem wrong (certainly justifying your point below).


================
Comment at: lib/Analysis/ScalarEvolution.cpp:6873
@@ -6872,3 +6872,3 @@
 bool
 ScalarEvolution::isKnownPredicateWithRanges(ICmpInst::Predicate Pred,
                                             const SCEV *LHS, const SCEV *RHS) {
----------------
sanjoy wrote:
> This should probably live in `ScalarEvolution::isKnownPredicate` or `ScalarEvolution::isImpliedCondOperandsHelper`, not here.
I put these here as they exactly mirror the check done below as part of the ICmpInst::ICMP_NE case below (which could certainly also be moved if we'd like).


================
Comment at: lib/Analysis/ScalarEvolution.cpp:6892
@@ -6891,1 +6891,3 @@
       return false;
+
+    const SCEV *Diff = getMinusSCEV(LHS, RHS);
----------------
sanjoy wrote:
> I'm not sure this is sound w.r.t. overflow.  For instance, if `LHS` = `i8 127` and `RHS` = `i8 -1` then `!(LHS < RHS)` but `LHS - RHS = i8 128 < 0`
This is precisely what was worrying me w.r.t. to correctness, and given the output, it seems this is exactly what happens. Sign-extending first would fix that, right?


Repository:
  rL LLVM

http://reviews.llvm.org/D12073