RFR: 8360192: C2: Make the type of count leading/trailing zero nodes more precise [v7]

[Qizheng Xing]

On Wed, 6 Aug 2025 10:42:42 GMT, Jatin Bhateja <jbhateja at openjdk.org> wrote:

>> Qizheng Xing has updated the pull request with a new target base due to a merge or a rebase. The incremental webrev excludes the unrelated changes brought in by the merge/rebase. The pull request contains nine additional commits since the last revision:
>> 
>>  - Merge branch 'master' into enhance-clz-type
>>  - Add checks for results of all test methods
>>  - Replace `isa_*` with `is_*` and add checks for `Type::BOTTOM`
>>  - Merge branch 'master' into enhance-clz-type
>>  - Move `TestCountBitsRange` to `compiler.c2.gvn`
>>  - Fix null checks
>>  - Narrow type bound
>>  - Use `BitsPerX` constant instead of `sizeof`
>>  - Make the type of count leading/trailing zero nodes more precise
>
> src/hotspot/share/opto/countbitsnode.cpp line 89:
> 
>> 87:   return TypeInt::make(count_leading_zeros_long(~tl->_bits._zeros),
>> 88:                        count_leading_zeros_long(tl->_bits._ones),
>> 89:                        tl->_widen);
> 
> Hi @MaxXSoft, Taking the liberty to add some comments related to the proof of the above assumptions, hope you won't mind :-)
> 
> **Z3 proof for [KnownBits.ONES, ~KnownBits.ZEROS] >= [LB, UB] where >= is a superset relation.**
> 
> 
> from z3 import *
> from functools import reduce
> 
> # 64-bit symbolic unsigned integers
> UB = BitVec('UB', 64)
> LB = BitVec('LB', 64)
> 
> # XOR for detecting differing bits
> xor_val = UB ^ LB
> 
> # COUNT_LEADING_ZEROS
> def count_leading_zeros(x):
>     """Returns number of leading zeros in a 64-bit word."""
>     clauses = []
>     for i in range(64):
>         bit_is_one = LShR(x, 63 - i) & 1 == 1
>         bits_before_zero = And([LShR(x, 63 - j) & 1 == 0 for j in range(i)])
>         clauses.append(If(And(bits_before_zero, bit_is_one), BitVecVal(i, 64), BitVecVal(64, 64)))
>     return reduce(lambda a, b: If(a == 64, b, a), clauses)
> 
> # Step 1: Compute common prefix length
> CPL = count_leading_zeros(xor_val)
> 
> # Step 2: COMMON_PREFIX_MASK = ((1 << CPL) - 1) << (64 - CPL)
> one_shifted = (BitVecVal(1, 64) << CPL)
> mask = one_shifted - 1
> COMMON_PREFIX_MASK = mask << (64 - CPL)
> 
> # Step 3: COMMON_PREFIX
> COMMON_PREFIX = UB & COMMON_PREFIX_MASK
> 
> # Step 4: ZEROS and ONES
> ZEROS = COMMON_PREFIX_MASK & (~COMMON_PREFIX)
> ONES = COMMON_PREFIX
> 
> # Step 5: Prove that [ONES, ~ZEROS] ⊇ [LB, UB]
> prop = And(ULE(ONES, LB), ULE(UB, ~ZEROS))
> 
> # Step 6: Try to disprove (i.e., check if any UB, LB violates the above)
> s = Solver()
> s.add(Not(prop))  # Look for counterexamples
> 
> # Check the result
> if s.check() == sat:
>     m = s.model()
>     ub_val = m.eval(UB).as_long()
>     lb_val = m.eval(LB).as_long()
>     ones_val = m.eval(ONES).as_long()
>     zeros_val = m.eval(ZEROS).as_long()
>     not_zeros_val = (~zeros_val) & 0xFFFFFFFFFFFFFFFF
> 
>     print("❌ Property does NOT hold. Counterexample found:")
>     print(f"LB     = {lb_val:#018x}")
>     print(f"UB     = {ub_val:#018x}")
>     print(f"ONES   = {ones_val:#018x}")
>     print(f"~ZEROS = {not_zeros_val:#018x}")
>     print(f"ONES <= LB? {ones_val <= lb_val}")
>     print(f"UB <= ~ZEROS? {ub_val <= not_zeros_val}")
> else:
>     print("✅ Property holds: [ONES, ~ZEROS] always covers [LB, UB] (UNSAT)")		 
> 
> 
> 
> <img width="975" height="88" alt="image" src="https://github.com/user-attachments/assets/244a373d-99ac-45d7-ab57-24e78b1ea216" ...

Thanks for the addition! Very nice and solid proof.

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

PR Review Comment: https://git.openjdk.org/jdk/pull/25928#discussion_r2258707055