On Fri, 19 Sep 2025 11:16:26 GMT, Hannes Greule <[email protected]> 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
