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

[Nikita Popov via Phabricator via llvm-commits]

nikic 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);
----------------
goldstein.w.n wrote:
> 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)`
Why isn't this covered by ephemeral value handling? That is supposed to prevent an assume from simplifying its own condition.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D142832