VM model and aconst_init

[forax at univ-mlv.fr]

> From: "John Rose" <john.r.rose at oracle.com>
> To: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "valhalla-spec-experts" <valhalla-spec-experts at openjdk.java.net>
> Sent: Wednesday, January 19, 2022 9:40:15 AM
> Subject: Re: VM model and aconst_init

> I think (based on our most recent conversations)
> that aconst_init can return a Q-type for B3 types
> and an L-type for B2 types. And likewise for the input
> and output of withfield .

Yes ! 

> The net result is that both bytecodes need to be
> permissive about L and Q types, because B2 and B3
> translation strategies require distinct parallel use
> cases.

> This is probably not clear in the docs, but I think
> it makes sense.

> Can you mix and match both modes in the same method?
> Probably, since the interpreter doesn’t care about
> multi-bytecode patterns. Dunno if this causes a testing
> problem, and if so how to fix it. I think it’s probably
> OK, especially if we require the two-way checkcast
> (Q-Foo not a subtype of L-Foo in the verifier) so that
> each mode stays “in its own lane”.

> More explicitly, this is a set of use cases for using
> Q-types in C_Class entries in the constant pool to switch
> to Q-mode for bytecodes that refer to classes, including
> withfield and aconst_init .

Let's talk a bit about having the L world and the Q world completely disjoint at least from the bytecode verifier POV. 

It means that we need some checkcasts to move in both direction, from a Q-type to a L-type and vice-versa. 
But at the same time, an array of L-type is a subtype of an array of Q-type ? 
The result to a very uncommon/unconventional type system, and i'm not a big fan of surprises in that area. 

Furthermore, i believe that subtyping is a key to avoid multiple bytecode verification of the generics code. 
By example, with the TypeRestriction attribute [1], the restriction has to be subtype of the declared type/descriptor. 

Rémi 

[1] https://cr.openjdk.java.net/~jrose/values/parametric-vm.html#type-restricted-methods-and-fields-and-the-typerestriction-attribute