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

[Noah Goldstein via Phabricator via llvm-commits]

goldstein.w.n added a comment.

In D150425#4340254 <https://reviews.llvm.org/D150425#4340254>, @nikic wrote:

> In D150425#4340213 <https://reviews.llvm.org/D150425#4340213>, @goldstein.w.n wrote:
>
>> In D150425#4340211 <https://reviews.llvm.org/D150425#4340211>, @nikic wrote:
>>
>>> In D150425#4340196 <https://reviews.llvm.org/D150425#4340196>, @goldstein.w.n wrote:
>>>
>>>> In D150425#4340195 <https://reviews.llvm.org/D150425#4340195>, @nikic wrote:
>>>>
>>>>> In D150425#4340187 <https://reviews.llvm.org/D150425#4340187>, @goldstein.w.n wrote:
>>>>>
>>>>>> In D150425#4340180 <https://reviews.llvm.org/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.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D150425