[ValueTracking] deduce `X * Y != 0` if `LowestKnownBit(X) * LowestKnownBit(Y) != 0`

[goldstein.w.n]

Summary

For X * Y, if there exists a subset of X and subset of Y s.t sX * sY != 0,
then X * Y != 0.

• See first proof: https://alive2.llvm.org/ce/z/28C9CG
• NB: This is why the previous Odd case works.

In knownbits we could exhaustively hunt for such a subset, but
LSB(X) and LSB(Y) actually works. If LSB(X) * LSB(Y) != 0, then
X * Y != 0

• See proof: https://alive2.llvm.org/ce/z/p5wWid

In isKnownNonZero we can use this as if the `LowestKnownOne(X) *
LowestKnownOne(Y) != 0`, then X * Y != 0, and we don't need to try
and other subsets.

[goldstein.w.n]

Rebase

[nikic]

I find the formulation here kind of confusing. Wouldn't something like this be more obvious? https://alive2.llvm.org/ce/z/p5wWid

[goldstein.w.n]

In D150425#4340180, @nikic wrote:

I find the formulation here kind of confusing. Wouldn't something like this be more obvious? https://alive2.llvm.org/ce/z/p5wWid

That works for the second proof, but not the first. We can't actually compute the LSB. Only the Lowest KnownBit.
Truthfully the first formula is enough for everything (as the arbitrary x_subset and y_subset include the set
of an known lowest bit).

[goldstein.w.n]

In D150425#4340180, @nikic wrote:

I find the formulation here kind of confusing. Wouldn't something like this be more obvious? https://alive2.llvm.org/ce/z/p5wWid

Updated second proof to yours

[nikic]

In D150425#4340187, @goldstein.w.n wrote:

In D150425#4340180, @nikic wrote:

I find the formulation here kind of confusing. Wouldn't something like this be more obvious? https://alive2.llvm.org/ce/z/p5wWid

That works for the second proof, but not the first. We can't actually compute the LSB. Only the Lowest KnownBit.
Truthfully the first formula is enough for everything (as the arbitrary x_subset and y_subset include the set
of an known lowest bit).

Maybe I'm missing something, but can't we implement this as return XKnown.countMaxTrailingZeros() + YKnown.countMaxTrailingZeros() < BitWidth?

[goldstein.w.n]

In D150425#4340195, @nikic wrote:

In D150425#4340187, @goldstein.w.n wrote:

In D150425#4340180, @nikic wrote:

I find the formulation here kind of confusing. Wouldn't something like this be more obvious? https://alive2.llvm.org/ce/z/p5wWid

That works for the second proof, but not the first. We can't actually compute the LSB. Only the Lowest KnownBit.
Truthfully the first formula is enough for everything (as the arbitrary x_subset and y_subset include the set
of an known lowest bit).

Maybe I'm missing something, but can't we implement this as return XKnown.countMaxTrailingZeros() + YKnown.countMaxTrailingZeros() < BitWidth?

We can. Just through LowBit(X) * LowBit(Y) != 0 was clearer. Would you prefer trailing zeros version?

[nikic]

In D150425#4340196, @goldstein.w.n wrote:

In D150425#4340195, @nikic wrote:

In D150425#4340187, @goldstein.w.n wrote:

In D150425#4340180, @nikic wrote:

I find the formulation here kind of confusing. Wouldn't something like this be more obvious? https://alive2.llvm.org/ce/z/p5wWid

That works for the second proof, but not the first. We can't actually compute the LSB. Only the Lowest KnownBit.
Truthfully the first formula is enough for everything (as the arbitrary x_subset and y_subset include the set
of an known lowest bit).

Maybe I'm missing something, but can't we implement this as return XKnown.countMaxTrailingZeros() + YKnown.countMaxTrailingZeros() < BitWidth?

We can. Just through LowBit(X) * LowBit(Y) != 0 was clearer. Would you prefer trailing zeros version?

Yes, as it is less code and requires less proofs. I expect you can also drop the separate KnownBits::mul(XKnown, YKnown).isNonZero() call and just return this in all cases.

[goldstein.w.n]

In D150425#4340211, @nikic wrote:

In D150425#4340196, @goldstein.w.n wrote:

In D150425#4340195, @nikic wrote:

In D150425#4340187, @goldstein.w.n wrote:

In D150425#4340180, @nikic wrote:

I find the formulation here kind of confusing. Wouldn't something like this be more obvious? https://alive2.llvm.org/ce/z/p5wWid

That works for the second proof, but not the first. We can't actually compute the LSB. Only the Lowest KnownBit.
Truthfully the first formula is enough for everything (as the arbitrary x_subset and y_subset include the set
of an known lowest bit).

Maybe I'm missing something, but can't we implement this as return XKnown.countMaxTrailingZeros() + YKnown.countMaxTrailingZeros() < BitWidth?

We can. Just through LowBit(X) * LowBit(Y) != 0 was clearer. Would you prefer trailing zeros version?

Yes, as it is less code and requires less proofs.

Okay.

I expect you can also drop the separate KnownBits::mul(XKnown, YKnown).isNonZero() call and just return this in all cases.

I would prefer not to do that. I _think_ this should cover all cases, but I'm by no means certain there aren't other edge cases. I think its more future-proof to still fallback on KnownBits::mul. Since we already have the KnownBits for X/Y, I think the cost is pretty minimal. That okay?

[goldstein.w.n]

Do X.TrailingZero + Y.TrailingZero < BitWidth instead of explicit Mul on Lowbits

[nikic]

In D150425#4340213, @goldstein.w.n wrote:

In D150425#4340211, @nikic wrote:

In D150425#4340196, @goldstein.w.n wrote:

In D150425#4340195, @nikic wrote:

In D150425#4340187, @goldstein.w.n wrote:

In D150425#4340180, @nikic wrote:

I find the formulation here kind of confusing. Wouldn't something like this be more obvious? https://alive2.llvm.org/ce/z/p5wWid

That works for the second proof, but not the first. We can't actually compute the LSB. Only the Lowest KnownBit.
Truthfully the first formula is enough for everything (as the arbitrary x_subset and y_subset include the set
of an known lowest bit).

Maybe I'm missing something, but can't we implement this as return XKnown.countMaxTrailingZeros() + YKnown.countMaxTrailingZeros() < BitWidth?

We can. Just through LowBit(X) * LowBit(Y) != 0 was clearer. Would you prefer trailing zeros version?

Yes, as it is less code and requires less proofs.

Okay.

I expect you can also drop the separate KnownBits::mul(XKnown, YKnown).isNonZero() call and just return this in all cases.

I would prefer not to do that. I _think_ this should cover all cases, but I'm by no means certain there aren't other edge cases. I think its more future-proof to still fallback on KnownBits::mul. Since we already have the KnownBits for X/Y, I think the cost is pretty minimal. That okay?

The alive2 proof shows that this is as good as we can do (it's not an implication, it's an equivalence). I think it's valuable to retain that fact.

[goldstein.w.n]

In D150425#4340254, @nikic wrote:

In D150425#4340213, @goldstein.w.n wrote:

In D150425#4340211, @nikic wrote:

In D150425#4340196, @goldstein.w.n wrote:

In D150425#4340195, @nikic wrote:

In D150425#4340187, @goldstein.w.n wrote:

In D150425#4340180, @nikic wrote:

I find the formulation here kind of confusing. Wouldn't something like this be more obvious? https://alive2.llvm.org/ce/z/p5wWid

That works for the second proof, but not the first. We can't actually compute the LSB. Only the Lowest KnownBit.
Truthfully the first formula is enough for everything (as the arbitrary x_subset and y_subset include the set
of an known lowest bit).

Maybe I'm missing something, but can't we implement this as return XKnown.countMaxTrailingZeros() + YKnown.countMaxTrailingZeros() < BitWidth?

We can. Just through LowBit(X) * LowBit(Y) != 0 was clearer. Would you prefer trailing zeros version?

Yes, as it is less code and requires less proofs.

Okay.

I expect you can also drop the separate KnownBits::mul(XKnown, YKnown).isNonZero() call and just return this in all cases.

I would prefer not to do that. I _think_ this should cover all cases, but I'm by no means certain there aren't other edge cases. I think its more future-proof to still fallback on KnownBits::mul. Since we already have the KnownBits for X/Y, I think the cost is pretty minimal. That okay?

The alive2 proof shows that this is as good as we can do (it's not an implication, it's an equivalence). I think it's valuable to retain that fact.

Okay. I think the proofs need to be slightly strengthened to show that because we don't actually be the trailining zeros count. We have
the best guess trailing zeros count. But:
https://alive2.llvm.org/ce/z/6ASRJz
Should do it.

Edit: Actually I'm not sure it works:
https://alive2.llvm.org/ce/z/V3c2Bk

[goldstein.w.n]

In D150425#4340254, @nikic wrote:

In D150425#4340213, @goldstein.w.n wrote:

In D150425#4340211, @nikic wrote:

In D150425#4340196, @goldstein.w.n wrote:

In D150425#4340195, @nikic wrote:

In D150425#4340187, @goldstein.w.n wrote:

In D150425#4340180, @nikic wrote:

I find the formulation here kind of confusing. Wouldn't something like this be more obvious? https://alive2.llvm.org/ce/z/p5wWid

That works for the second proof, but not the first. We can't actually compute the LSB. Only the Lowest KnownBit.
Truthfully the first formula is enough for everything (as the arbitrary x_subset and y_subset include the set
of an known lowest bit).

Maybe I'm missing something, but can't we implement this as return XKnown.countMaxTrailingZeros() + YKnown.countMaxTrailingZeros() < BitWidth?

We can. Just through LowBit(X) * LowBit(Y) != 0 was clearer. Would you prefer trailing zeros version?

Yes, as it is less code and requires less proofs.

Okay.

I expect you can also drop the separate KnownBits::mul(XKnown, YKnown).isNonZero() call and just return this in all cases.

I would prefer not to do that. I _think_ this should cover all cases, but I'm by no means certain there aren't other edge cases. I think its more future-proof to still fallback on KnownBits::mul. Since we already have the KnownBits for X/Y, I think the cost is pretty minimal. That okay?

The alive2 proof shows that this is as good as we can do (it's not an implication, it's an equivalence). I think it's valuable to retain that fact.

You're right :)

testBinaryOpExhaustive(
    [](const KnownBits &Known1, const KnownBits &Known2) {
      KnownBits Ret(Known1.getBitWidth());
      Ret.resetAll();
      if ((Known1.countMaxTrailingZeros() + Known2.countMaxTrailingZeros()) <
          Known1.getBitWidth()) {
        Ret.setAllOnes();
      } else if ((Known1.countMinTrailingZeros() +
                  Known2.countMinTrailingZeros()) >= Known1.getBitWidth()) {
        Ret.setAllZero();
      }
      return Ret;
    },
    [](const APInt &N1, const APInt &N2) {
      APInt V = N1 * N2;
      return V.isZero() ? V : APInt::getAllOnes(V.getBitWidth());
    });

Love the new knownbits tests you added. They are really useful :)
Updating.

[goldstein.w.n]

Use LSB(X) * LSB(Y) != 0 as final check instead of KnownBits::mul

[nikic]

LGTM

llvm/lib/Analysis/ValueTracking.cpp

if (XKnown.One[0])
       return isKnownNonZero(I->getOperand(1), DemandedElts, Depth, Q);
 
     KnownBits YKnown =
         computeKnownBits(I->getOperand(1), DemandedElts, Depth, Q);
     if (YKnown.One[0])
       return XKnown.isNonZero() ||
              isKnownNonZero(I->getOperand(0), DemandedElts, Depth, Q);
 
-    return KnownBits::mul(XKnown, YKnown).isNonZero();
+    // If there exists any subset of X (sX) and subset of Y (sY) s.t sX * sY is
+    // non-zero, then X * Y is non-zero. We can find sX and sY by just taking
+    // the the lowest known One of X and Y. If they are non-zero, the result
+    // must be non-zero. We can check if LSB(X) * LSB(Y) != 0 by doing
+    // X.CountLeadingZeros + Y.CountLeadingZeros < BitWidth.
+    return (XKnown.countMaxTrailingZeros() + YKnown.countMaxTrailingZeros()) <
+           BitWidth;
   }
   case Instruction::Select:
     // (C ? X : Y) != 0 if X != 0 and Y != 0.
     if (isKnownNonZero(I->getOperand(1), DemandedElts, Depth, Q) &&
         isKnownNonZero(I->getOperand(2), DemandedElts, Depth, Q))
       return true;
     break;
   case Instruction::PHI: {

llvm/test/Analysis/ValueTracking/known-non-zero.ll

;
   %x = call i8 @llvm.smax.i8(i8 %xx, i8 %yy)
   %z = or i8 %x, %ind
   %r = icmp eq i8 %z, 0
   ret i1 %r
 }
 
 define i1 @mul_nonzero_contains_nonzero_mul(i8 %x, i8 %y) {
 ; CHECK-LABEL: @mul_nonzero_contains_nonzero_mul(
-; CHECK-NEXT:    [[XX:%.*]] = or i8 [[X:%.*]], 16
-; CHECK-NEXT:    [[YY:%.*]] = or i8 [[Y:%.*]], 8
-; CHECK-NEXT:    [[XY:%.*]] = mul i8 [[XX]], [[YY]]
-; CHECK-NEXT:    [[NZ:%.*]] = icmp ne i8 [[XY]], 0
-; CHECK-NEXT:    ret i1 [[NZ]]
+; CHECK-NEXT:    ret i1 true
 ;
   %xx = or i8 %x, 16
   %yy = or i8 %y, 8
   %xy = mul i8 %xx, %yy
   %nz = icmp ne i8 %xy, 0
   ret i1 %nz
 }