[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:
> > 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.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D142832