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

[Andrew Dinn]

On Fri, 6 Sep 2024 15:21:31 GMT, Quan Anh Mai <qamai at openjdk.org> wrote:

>> If _lo <= x <= _hi, then I believe the dual is _hi <= x <= _lo 
>> 
>> If dual is really only needed for join, then it seems like we could remove the concept of dual and just implement join.
>
> @dean-long Thanks, that is really helpful. IIUC, the duality here refers to the set of all `TypeInt` with a set `a` considered higher than `b` if `a` is a subset of `b`. This leads to our notion of bottom type being the universe set and top type being the empty set. It still does not make sense for the concept of a dual `TypeInt`, though, since the concept of duality applies to the set of `TypeInt`, not the `TypeInt`s themselves.
> 
>> My understanding is "join" means "union", "meet" means "intersection", and "dual" means "complement".
> 
> You got it backward, "join" means intersection and "meet" means union.

If you want to understand full details of how a (symmetrical) type lattice with duals supports a unified model for many different type flow analysis algorithms you can read up on it in Nielsen, Nielsen and Hankin's book Principles of Program Analysis. If it is new to you then a more simplified account of the use of (unqualified) TOP and BOTTOM types in type flow analysis can be found in Muchnick's book Advanced Compiler Design and Implementation. Note that Cliff Click goes against conventional mathematical terminology in making BOTTOM a universal type and TOP an empty (unrealizable) type.

One detail that may not be obvious is that the sub-lattice for int and long sorts includes the hierarchy of single, continuous intervals. Individual integral values (on the lattice centre line) are modelled as singleton ranges i.e. [a,a]. Given the large cardinality of the set of continuous intervals this makes it necessary to place a bound on any fixed point iterations that widen interval ranges. The iteration is killed by widening to the maximum range (this is what Cliff refers to in the code as a 'death march').

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

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