[PATCH] D142832: [ValueTracking] Add support in `isKnownNonZero` for dominating condition from `X > C1 && X < C2`

[Noah Goldstein via Phabricator via llvm-commits]

goldstein.w.n added inline comments.


================
Comment at: llvm/lib/Transforms/InstCombine/InstCombineCompares.cpp:2826
+    // both lose information and de-canonicalize the (A < C1 && A > C2) case
+    if (!Cmp.isAssumedTrue(/*OneUse*/ true)) {
+      const SimplifyQuery Q = SQ.getWithInstruction(&Cmp);
----------------
nikic wrote:
> What is the motivating test case for this? And what information are we losing? This looks very dubious.
> What is the motivating test case for this? And what information are we losing? This looks very dubious.

`check_ucmp_range_from0_assumed` and `check_ucmp_range_from0_and_abs` both rely on it. Diff w.o is roughly:

```
 define i1 @check_ucmp_range_from0_assumed(i8 %x, i8 %y) {
 ; CHECK-LABEL: @check_ucmp_range_from0_assumed(
-; CHECK-NEXT:    [[UB:%.*]] = add i8 [[X:%.*]], -1
-; CHECK-NEXT:    [[NE:%.*]] = icmp ult i8 [[UB]], 14
+; CHECK-NEXT:    [[NE:%.*]] = icmp ult i8 [[X:%.*]], 15
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[NE]])
 ; CHECK-NEXT:    [[CMP0:%.*]] = icmp ugt i8 [[X]], [[Y:%.*]]
-; CHECK-NEXT:    ret i1 [[CMP0]]
+; CHECK-NEXT:    [[CMP1:%.*]] = icmp eq i8 [[Y]], 0
+; CHECK-NEXT:    [[R:%.*]] = or i1 [[CMP0]], [[CMP1]]
+; CHECK-NEXT:    ret i1 [[R]]
```
and
```
 define i1 @check_ucmp_range_from0_and_abs(i8 %x, i8 %y) {
 ; CHECK-LABEL: @check_ucmp_range_from0_and_abs(
 ; CHECK-NEXT:    [[X1:%.*]] = and i8 [[X:%.*]], 123
-; CHECK-NEXT:    [[TMP1:%.*]] = add nsw i8 [[X1]], -1
-; CHECK-NEXT:    [[NE:%.*]] = icmp ult i8 [[TMP1]], 14
+; CHECK-NEXT:    [[NE:%.*]] = icmp ult i8 [[X1]], 15
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[NE]])
 ; CHECK-NEXT:    [[CMP0:%.*]] = icmp ugt i8 [[X]], [[Y:%.*]]
-; CHECK-NEXT:    ret i1 [[CMP0]]
+; CHECK-NEXT:    [[CMP1:%.*]] = icmp eq i8 [[Y]], 0
+; CHECK-NEXT:    [[R:%.*]] = or i1 [[CMP0]], [[CMP1]]
+; CHECK-NEXT:    ret i1 [[R]]
 ;
```

The expression `X - 1 u< C` cannot be true for `X == 0`, the expression `X u< C` can be true for `X == 0` so when doing the dom analysis if we make the transform we end up unable to prove about `X != 0`. Its a but circular, i.e we use `isKnownNonZero(X)` which is true, make the change, then at a later use of `X` are unable to reprove `isKnownNonZero(X)`


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D142832/new/

https://reviews.llvm.org/D142832