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

[Emanuel Peter]

On Fri, 2 May 2025 07:29:41 GMT, Emanuel Peter <epeter at openjdk.org> wrote:

>> Quan Anh Mai has updated the pull request incrementally with one additional commit since the last revision:
>> 
>>   Emanuel's reviews
>
> src/hotspot/share/opto/type.hpp line 708:
> 
>> 706:  *   I.e. x <= y in the signed domain iff x <= y in the unsigned domain
>> 707:  *
>> 708:  *   Then, we have:
> 
> The two `Then` are confusing me a little. The assumption is only the first sentence, not `x <= y iff juint(x) <= juint(y)`, right?
> 
> Hmm, ah you have an additional Lemma 3.1 here. But it is a little unclear where that starts and ends. Maybe that can be fixed with some indentation?

Or you just cram in the Lemma 3.1 before you start the proof of Lemma 3. That would probably be cleanest.

> src/hotspot/share/opto/type.hpp line 745:
> 
>> 743:  *
>> 744:  *     In this case, all elements of t belongs to either [t._lo, jint(t._uhi)] or
>> 745:  *     [jint(t._ulo), t._hi].
> 
> When you say "all elements belong to x or y", one might misunderstand that they all are in one range and the other is empty.
> Suggestion:
> 
>  *     In this case, each element of t belongs to either [t._lo, jint(t._uhi)] or
>  *     [jint(t._ulo), t._hi].
> 
> Here we look at them individually, and so it sounds a little less misleading to me. But that may just be my brain that sees it like this 😅

Anyway: either
all elements belong
or
each element belongs

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

PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r2071216411
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r2071233010