missed fold, zext(x + 1) - 1 > C => x > C

[zhengyang92]

https://alive2.llvm.org/ce/z/-mgzSg
https://godbolt.org/z/xWreoG6x5

define i1 @src(i32 %0) {
entry:
  %2 = add i32 %0, 1
  %3 = zext i32 %2 to i64
  %4 = add i64 %3, -1
  %5 = icmp ult i64 %4, 8
  ret i1 %5
}

define i1 @tgt(i32 %0) {
entry:
  %r = icmp ult i32 %0, 8
  ret i1 %r
}

@regehr @dtcxzyw

[dtcxzyw]

I don't know how to generalize this pattern :(
Any thoughts?

cc @nikic @goldsteinn

[nikic]

I don't know how to generalize this pattern :(

The generalization here is you can commute zext over nuw operations -- but we currently cannot preserve sub nuw x, C due to canonicalization to add x, -C. We would need a new poison flag for this. (This is a recurring problem, also a big issue in SCEV.)

Of course, we can work around it locally by explicitly proving no overflow, it just doesn't scale.

[dtcxzyw]

We would need a new poison flag for this.

Do you mean introducing "always-wrap" flags?
Alive2: https://alive2.llvm.org/ce/z/6XgsFv

[nikic]

I don't think your proof is working correctly (you used sadd instead of uadd and it still passed?)

But yes, I believe "always wrap" is a possible, if somewhat unintuitive, way to formulate it.

[dtcxzyw]

(you used sadd instead of uadd and it still passed?)

Sorry, the return value should be %res instead of %c. So the proof is incorrect :(

[nikic]

@dtcxzyw Ah yes, it doesn't work if the negated value is zero: https://alive2.llvm.org/ce/z/Onv-xv Duh.

[nikic]

In that case something like nnuw (negated no unsigned wrap)that specifically means thatadd nnuw x, yis equivalent tosub nuw x, -y`.

[dtcxzyw]

Generalized fold: https://alive2.llvm.org/ce/z/Z_nK2c

[goldsteinn]

@dtcxzyw are you working on a patch for this? Otherwise I'm happy to make one.