RFR: 8365205: C2: Optimize popcount value computation using knownbits [v10]

[Jatin Bhateja]

On Fri, 19 Sep 2025 11:16:26 GMT, Hannes Greule <hgreule at openjdk.org> wrote:

>> Jatin Bhateja has updated the pull request incrementally with one additional commit since the last revision:
>> 
>>   Update TestPopCountValueTransforms.java
>
> src/hotspot/share/opto/countbitsnode.cpp line 123:
> 
>> 121: // we have at least and at most.
>> 122: // From the definition of KnownBits, we know:
>> 123: //   zeros: Indicates which bits must be 0: ones[i] =1 -> t[i]=0
> 
> I'm a bit confused by this, is ones[i] mixed up with zeros[i]? I.e., t[i]=0 if zeros[i]=1

@SirYwell , comment updated.

Links to formal z3 proofs for this:-

https://github.com/openjdk/jdk/pull/25928#discussion_r2256750507

https://bugs.openjdk.org/browse/JDK-8365205?focusedId=14807707&page=com.atlassian.jira.plugin.system.issuetabpanels%3Acomment-tabpanel#comment-14807707:~:text=C%3A%5CGithub%5Csoftwares%5Cz3%5Cz3%2D4.15.2%2Dx64%2Dwin%5Cbin%5Cpython%3Epython3%20known_bits_popcount.py%0AMain%20constraints%20satisfiable.%0AConstraints%20are%20valid%20(negation%20unsatisfiable).

-------------

PR Review Comment: https://git.openjdk.org/jdk/pull/27075#discussion_r2364498821