This is an archive of the discontinued LLVM Phabricator instance.

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

Authored by goldstein.w.n on May 11 2023, 10:05 PM.

Details

Summary

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

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

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.

Diff Detail

Unit TestsFailed

Event Timeline

goldstein.w.n created this revision.May 11 2023, 10:05 PM
Herald added a project: Restricted Project. · View Herald TranscriptMay 11 2023, 10:05 PM
Herald added a subscriber: hiraditya. · View Herald Transcript
goldstein.w.n requested review of this revision.May 11 2023, 10:05 PM
Herald added a project: Restricted Project. · View Herald TranscriptMay 11 2023, 10:05 PM

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

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 edited the summary of this revision. (Show Details)May 13 2023, 12:17 PM

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

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?

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?

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.

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?

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

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 added a comment.EditedMay 13 2023, 1:14 PM

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

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.

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

nikic accepted this revision.May 16 2023, 1:13 AM

LGTM

This revision is now accepted and ready to land.May 16 2023, 1:13 AM
This revision was landed with ongoing or failed builds.May 16 2023, 4:58 PM
This revision was automatically updated to reflect the committed changes.