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

[Nikita Popov via Phabricator via llvm-commits]

nikic added a comment.

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. I expect you can also drop the separate `KnownBits::mul(XKnown, YKnown).isNonZero()` call and just return this in all cases.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D150425