[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:
> goldstein.w.n wrote:
> > nikic wrote:
> > > 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.
> > > Why isn't this covered by ephemeral value handling? That is supposed to prevent an assume from simplifying its own condition.
> > 
> > I don't know, what file should I look at?
> > 
> > My preference would be to keep as is and add `TODO` to see if this can be handled by ephemeral value handling. But can also do the inverse (remove this and add `TODO` to fix by handling in ephemeral value handling).
> See isEphemeralValueOf() used by isValidAssumeForContext() in ValueTracking.
> See isEphemeralValueOf() used by isValidAssumeForContext() in ValueTracking.

So I'm not sure what you're getting at with re:"Why isn't this covered by ephemeral value handling?", the issue isn't that the assume doesn't check the expression, the issue is that after we visit the `X0 + 1 u< C0` the new expression `X1 u<= C1` no longer exclude zero.

Do isEphemeralValueOf` exclude the instruction from going the `instcombine`? If not I don't see how it could help avoid this case.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D142832