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

Fri Feb 14 09:46:35 UTC 2025

On Thu, 13 Feb 2025 14:59:02 GMT, Quan Anh Mai <qamai at openjdk.org> wrote:

>> Hi,
>> 
>> This patch adds unsigned bounds and known bits constraints to TypeInt and TypeLong. This opens more transformation opportunities in an elegant manner as well as helps avoid some ad-hoc rules in Hotspot.
>> 
>> In general, a `TypeInt/Long` represents a set of values `x` that satisfies: `x s>= lo && x s<= hi && x u>= ulo && x u<= uhi && (x & zeros) == 0 && (x & ones) == ones`. These constraints are not independent, e.g. an int that lies in [0, 3] in signed domain must also lie in [0, 3] in unsigned domain and have all bits but the last 2 being unset. As a result, we must canonicalize the constraints (tighten the constraints so that they are optimal) before constructing a `TypeInt/Long` instance.
>> 
>> This is extracted from #15440 , node value transformations are left for later PRs. I have also added unit tests to verify the soundness of constraint normalization.
>> 
>> Please kindly review, thanks a lot.
>> 
>> Testing
>> 
>> - [x] GHA
>> - [x] Linux x64, tier 1-4
>
> 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

Things are looking steadily better! I have a few more suggestions.

src/hotspot/share/opto/rangeinference.cpp line 149:

> 147: 
> 148:   Call r the smallest value not smaller than lo that satisfies bits. Since lo
> 149:   does not satisfy bits, lo < r (2.7)

You could reorder things to make it more straight forward:
- First define `r`:
  - the smallest value not smaller than lo that satisfies bits
- Then construct `v`
- Lemma: `v` satisfies bits (probably helpful to get started...)
- Statement: `r = v`
- Proof
  - (a): `r <= v` (using the Lemma)
  - (b): `r >= v` (via contradiction if `r < v`)

src/hotspot/share/opto/rangeinference.cpp line 153:

> 151:   a. Firstly, we prove that r <= v:
> 152: 
> 153:     Trivially, lo < v since:

Suggestion:

    We know that lo < v since:

It's a little funny to say its trivial and then go ahead and prove it 😅

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?

src/hotspot/share/opto/rangeinference.cpp line 164:

> 162: 
> 163:     As a result, v > lo and v satisfies bits since all of its bits satisfy bits. Which
> 164:     means r <= v since r is the smallest such value.

This is a little quick...
- You proved `v > lo` above, so give it a name and reference it here.
- `v satisfies bits` can be its separate step as I suggested above. Give it a name and reference it here.
- `v` is a value larger than `lo` that satisfies bits, and `r` is the smallest value larger than `lo` that satisfies bits, hence `v >= r`.

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:

src/hotspot/share/opto/rangeinference.cpp line 179:

> 177:       v[j] == 1 (according to 2.b.2)
> 178:       r[x] == v[x], for x < j (according to 2.b.3)
> 179:       v[x] == lo[x], for x < j (according to 2,4 because j < i)

Suggestion:

      v[x] == lo[x], for x < j (according to 2.4 because j < i)

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?

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

Changes requested by epeter (Reviewer).

PR Review: https://git.openjdk.org/jdk/pull/17508#pullrequestreview-2617160068
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1955816531
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1955799188
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1955809601
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1955828802
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1955832072
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1955837820
PR Review Comment: https://git.openjdk.org/jdk/pull/17508#discussion_r1955849996