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

[Emanuel Peter]

On Mon, 4 Nov 2024 08:58:47 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 32 commits:
>> 
>>  - Merge branch 'master' into unsignedbounds
>>  - address reviews
>>  - comment adjust_lo empty case
>>  - formality
>>  - address reviews
>>  - add comments, refactor functions to helper class
>>  - refine comments
>>  - remove leftover code
>>  - add doc to TypeInt, rename parameters, remove unused methods
>>  - change (~v & ones) == 0 to (v & ones) == ones
>>  - ... and 22 more: https://git.openjdk.org/jdk/compare/309b9291...7f3316fa
>
> src/hotspot/share/opto/type.hpp line 622:
> 
>> 620:  * TypeInt lie in the intervals [_lo, jint(_uhi)] or [jint(_ulo), _hi]
>> 621:  *
>> 622:  * Proof: For 2 jint value x, y such that they are both >= 0 or < 0. Then:
> 
> Suggestion:
> 
>  * Proof: For 2 jint value x, y such that they are both >= 0 or both < 0. Then:
> 
> Or are you allowing them to one be positive and one negative?

Also: this is more of a "Lemma", and could be stated before the "Proof" of you property 2... it is property 2 that you are trying to prove here, right? The indentation would help for that as well.

> src/hotspot/share/opto/type.hpp line 634:
> 
>> 632:  * juint(t._lo) <= juint(jint(t._ulo)) == t._ulo <= juint(t._lo)
>> 633:  *
>> 634:  * Which means that t._lo == jint(t._ulo). Similarly, t._hi == jint(t._uhi).
> 
> Hmm. I feel like I don't immediately see the "Similarly" here.... too many hidden steps.

I'm going to stop reading the proof below.... I'll read again once you respond to the comments above ;)

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

PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1827671624
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1827680976