RFR: 8315066: Add unsigned bounds and known bits to TypeInt/Long [v43]

[Quan Anh Mai]

On Fri, 14 Feb 2025 09:20:10 GMT, Emanuel Peter <epeter at openjdk.org> wrote:

>> Quan Anh Mai has updated the pull request with a new target base due to a merge or a rebase. The pull request now contains 56 commits:
>> 
>>  - Merge branch 'master' into unsignedbounds
>>  - Merge branch 'master' into unsignedbounds
>>  - harden SimpleCanonicalResult
>>  - number lemmas
>>  - include
>>  - clean up intn_t
>>  - refine first_violation
>>  - assignment operator
>>  - exhaustive tests
>>  - make con
>>  - ... and 46 more: https://git.openjdk.org/jdk/compare/c2fc9478...3cd25862
>
> src/hotspot/share/opto/rangeinference.cpp line 158:
> 
>> 156:       bits at x > i have lower significance, and are thus irrelevant
>> 157: 
>> 158:     As established above, the first (i + 1) bits of v satisfy bits.
> 
> Two things:
> - I don't see immediately how it is true
> - And we are not trying to prove that v satisfies bits here. But we should prove that somewhere, just not under section `a. Firstly, we prove that r <= v:`, right?

The layout here may be a little confusing, I have added more detailed section label. In this part we are proving that `r <= v` by proving that `v > lo` (a.1) and `v` satisfies `bits` (a.2).

> src/hotspot/share/opto/rangeinference.cpp line 166:
> 
>> 164:     means r <= v since r is the smallest such value.
>> 165: 
>> 166:   b. Secondly, we prove that r == v. Suppose r < v:
> 
> Suggestion:
> 
>   b. Secondly, we prove that r >= v. Suppose r < v:

Doing it like this avoids having to mention `r <= v` again further below. We just say that since we know `r <= v`, the contradiction of `r == v` would be `r < v`.

> src/hotspot/share/opto/rangeinference.cpp line 184:
> 
>> 182:       r[j] == 0
>> 183:       lo[j] == 1
>> 184:       r[x] == lo[x], for x < j
> 
> Suggestion:
> 
>       r[j] == 0    (according to 2.b.1)
>       lo[j] == 1   (lo[j] == v[j] == 1, according to 2.4 because j < i, and according to 2.b.2)
>       r[x] == lo[x], for x < j  (according to 2.4 because j < i)
> 
> Then you could even drop the other list above, right?

Yes you are right, thanks a lot for your suggestions, I have done as you suggested and improved the format a little bit.

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

PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1956103750
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1956105088
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1956107220