This specification is not final and is subject to change. Use is subject to license terms.

JVM Types Cleanup

Changes to the Java® Virtual Machine Specification • Version 15-internal+0-adhoc.dlsmith.20200210

This document describes changes to the Java Virtual Machine Specification to clean up its treatment of types. Changes mainly fall into one of the following categories:

One behavioral change for JVM implementations is proposed: tightening the verification check that an interface named by invokespecial is a direct superinterface (4.10.1.9.invokespecial).

All other changes only presentational, with no intention to change the behavior of JVM implementations.

Changes are described with respect to existing sections of the JVM Specification. New text is indicated like this and deleted text is indicated like this. Explanation and discussion, as needed, is set aside in grey boxes.

Chapter 2: The Structure of the Java Virtual Machine

2.2 Data Types

Like the Java programming language, the The Java Virtual Machine operates on two kinds of types: primitive types and reference types. There are, correspondingly, two kinds of values that can be stored in variables, passed as arguments, returned by methods, and operated upon: primitive values and reference values.

The Java Virtual Machine expects that nearly all type checking is done prior to run time, typically by a compiler, and does not have to be done by the Java Virtual Machine itself. Values of primitive types need not be tagged or otherwise be inspectable to determine their types at run time, or to be distinguished from values of reference types. Instead, the instruction set of the Java Virtual Machine distinguishes its operand types using instructions intended to operate on values of specific types. For instance, iadd, ladd, fadd, and dadd are all Java Virtual Machine instructions that add two numeric values and produce numeric results, but each is specialized for its operand type: int, long, float, and double, respectively. For a summary of type support in the Java Virtual Machine instruction set, see 2.11.1.

The Java Virtual Machine contains explicit support for objects. An object is either a dynamically allocated class instance or an array. A reference to an object is considered to have Java Virtual Machine type reference. References are polymorphic: a single reference may also be a value of multiple class types, interface types, or array types. Values of type reference can be thought of as pointers to objects. More than one reference to an object may exist. Objects are always operated on, passed, and tested via values of type reference.

2.6 Frames

2.6.1 Local Variables

Each frame (2.6) contains an array of variables known as its local variables. The length of the local variable array of a frame is determined at compile-time and supplied in the binary representation of a class or interface along with the code for the method associated with the frame (4.7.3).

A single local variable can hold a value of type boolean, byte, char, short, int, float, reference, or returnAddress. A pair of local variables can hold a value of type long or double.

Local variables are addressed by indexing. The index of the first local variable is zero. An integer is considered to be an index into the local variable array if and only if that integer is between zero and one less than the size of the local variable array.

A value of type long or type double occupies two consecutive local variables. Such a value may only be addressed using the lesser index. For example, a value of type double stored in the local variable array at index n actually occupies the local variables with indices n and n+1; however, the local variable at index n+1 cannot be loaded from. It can be stored into. However, doing so invalidates the contents of local variable n.

The Java Virtual Machine does not require n to be even. In intuitive terms, values of types long and double need not be 64-bit aligned in the local variables array. Implementors are free to decide the appropriate way to represent such values using the two local variables reserved for the value.

The Java Virtual Machine uses local variables to pass parameters on method invocation. On class method invocation, any parameters are passed in consecutive local variables starting from local variable 0. On instance method invocation, local variable 0 is always used to pass a reference to the object on which the instance method is being invoked (this in the Java programming language). Any parameters are subsequently passed in consecutive local variables starting from local variable 1.

2.11 Instruction Set Summary

2.11.1 Types and the Java Virtual Machine

Most of the instructions in the Java Virtual Machine instruction set encode type information about the operations they perform. For instance, the iload instruction (6.5.iload) loads the contents of a local variable, which must be an int, onto the operand stack. The fload instruction (6.5.fload) does the same with a float value. The two instructions may have identical implementations, but have distinct opcodes.

For the majority of typed instructions, the instruction type is represented explicitly in the opcode mnemonic by a letter: i for an int operation, l for long, s for short, b for byte, c for char, f for float, d for double, and a for reference. Some instructions for which the type is unambiguous do not have a type letter in their mnemonic. For instance, arraylength always operates on an object that is an array. Some instructions, such as goto, an unconditional control transfer, do not operate on typed operands.

Given the Java Virtual Machine's one-byte opcode size, encoding types into opcodes places pressure on the design of its instruction set. If each typed instruction supported all of the Java Virtual Machine's run-time data types, there would be more instructions than could be represented in a byte. Instead, the instruction set of the Java Virtual Machine provides a reduced level of type support for certain operations. In other words, the instruction set is intentionally not orthogonal. Separate instructions can be used to convert between unsupported and supported data types as necessary.

Table 2.11.1-A summarizes the type support in the instruction set of the Java Virtual Machine. A specific instruction, with type information, is built by replacing the T in the instruction template in the opcode column by the letter in the type column. If the type column for some instruction template and type is blank, then no instruction exists supporting that type of operation. For instance, there is a load instruction for type int, iload, but there is no load instruction for type byte.

Note that most instructions in Table 2.11.1-A do not have forms for the integral types byte, char, and short. None have forms for the boolean type. A compiler encodes loads of literal values of types byte and short using Java Virtual Machine instructions that sign-extend those values to values of type int at compile-time or run-time. Loads of literal values of types boolean and char are encoded using instructions that zero-extend the literal to a value of type int at compile-time or run-time. Likewise, loads from arrays of values of type boolean, byte, short, and char are encoded using Java Virtual Machine instructions that sign-extend or zero-extend the values to values of type int. Whenever values of types byte and short are loaded onto the operand stack, they are implicitly converted by sign extension to values of type int. Similarly, whenever values of types boolean and char are loaded onto the operand stack, they are implicitly converted by zero extension to values of type int. Thus, most operations on values originally of actual types boolean, byte, char, and short are correctly performed by instructions operating on values of computational type int.

Table 2.11.1-A. Type support in the Java Virtual Machine instruction set

opcode byte short int long float double char reference
Tipush bipush sipush
Tconst iconst lconst fconst dconst aconst
Tload iload lload fload dload aload
Tstore istore lstore fstore dstore astore
Tinc iinc
Taload baload saload iaload laload faload daload caload aaload
Tastore bastore sastore iastore lastore fastore dastore castore aastore
Tadd iadd ladd fadd dadd
Tsub isub lsub fsub dsub
Tmul imul lmul fmul dmul
Tdiv idiv ldiv fdiv ddiv
Trem irem lrem frem drem
Tneg ineg lneg fneg dneg
Tshl ishl lshl
Tshr ishr lshr
Tushr iushr lushr
Tand iand land
Tor ior lor
Txor ixor lxor
i2T i2b i2s i2l i2f i2d
l2T l2i l2f l2d
f2T f2i f2l f2d
d2T d2i d2l d2f
Tcmp lcmp
Tcmpl fcmpl dcmpl
Tcmpg fcmpg dcmpg
if_TcmpOP if_icmpOP if_acmpOP
Treturn ireturn lreturn freturn dreturn areturn

The mapping between Java Virtual Machine actual original types and Java Virtual Machine computational types is summarized by Table 2.11.1-B.

Certain Java Virtual Machine instructions such as pop and swap operate on the operand stack without regard to type; however, such instructions are constrained to use only on values of certain categories of computational types, also given in Table 2.11.1-B.

Table 2.11.1-B. Actual Original and Computational types in the Java Virtual Machine

Actual Original type Computational type Category
boolean int 1
byte int 1
char int 1
short int 1
int int 1
float float 1
reference reference 1
returnAddress returnAddress 1
long long 2
double double 2

2.11.2 Load and Store Instructions

The load and store instructions transfer values between the local variables (2.6.1) and the operand stack (2.6.2) of a Java Virtual Machine frame (2.6):

Instructions that access fields of objects and elements of arrays (2.11.5) also transfer data to and from the operand stack.

Instruction mnemonics shown above with trailing letters between angle brackets (for instance, iload_<n>) denote families of instructions (with members iload_0, iload_1, iload_2, and iload_3 in the case of iload_<n>). Such families of instructions are specializations of an additional generic instruction (iload) that takes one operand. For the specialized instructions, the operand is implicit and does not need to be stored or fetched. The semantics are otherwise the same (iload_0 means the same thing as iload with the operand 0). The letter between the angle brackets specifies the type of the implicit operand for that family of instructions: for <n>, a nonnegative integer; for <i>, an int; for <l>, a long; for <f>, a float; and for <d>, a double. Forms for type int are used in many cases to perform operations on values of type byte, char, and short (2.11.1).

This notation for instruction families is used throughout this specification.

2.11.8 Method Invocation and Return Instructions

The following five instructions invoke methods:

The method return instructions, which are distinguished by return type, are ireturn (used to return values of type boolean, byte, char, short, or int), lreturn, freturn, dreturn, and areturn. In addition, the return instruction is used to return from methods declared to be void, instance initialization methods, and class or interface initialization methods.

Chapter 4: The class File Format

4.3 Descriptors

A descriptor is a string representing the type of a field or method. Descriptors are represented in the class file format using modified UTF-8 strings (4.4.7) and thus may be drawn, where not further constrained, from the entire Unicode codespace.

4.3.1 Grammar Notation

Descriptors are specified using a grammar. The grammar is a set of productions that describe how sequences of characters can form syntactically correct descriptors of various kinds. Terminal symbols of the grammar are shown in fixed width font, and should be interpreted as ASCII characters. Nonterminal symbols are shown in italic type. The definition of a nonterminal is introduced by the name of the nonterminal being defined, followed by a colon. One or more alternative definitions for the nonterminal then follow on succeeding lines.

The syntax {x} on the right-hand side of a production denotes zero or more occurrences of x.

The phrase (one of) on the right-hand side of a production signifies that each of the terminal symbols on the following line or lines is an alternative definition.

4.3.2 Field Descriptors

A field descriptor represents the type of a class, instance, or local variable.

FieldDescriptor:
FieldType
FieldType:
BaseType
ObjectType ClassType
ArrayType
BaseType:
(one of)
B C D F I J S Z
ObjectType: ClassType:
L ClassName ;
ArrayType:
[ ComponentType
ComponentType:
FieldType

The characters of BaseType, the L and ; of ObjectType, and the [ of ArrayType are all ASCII characters.

ClassName represents a binary class or interface name encoded in internal form (4.2.1).

A field descriptor mentions a class or interface name if the name appears as a ClassName in the descriptor. This includes a ClassName nested in the ComponentType of an ArrayType.

This definition of mentions allows us to eliminate boilerplate in a handful of other sections and gives us a single location to identify the classes that are subject to loading constraints, resolution, etc. The definition is flexible enough to support new kinds of types that may be added in the future.

The interpretation of field descriptors as types is shown in Table 4.3-A. See 2.2, 2.3, and 2.4 for the meaning of these types.

A field descriptor representing an array type is valid only if it represents a type with 255 or fewer dimensions.

Table 4.3-A. Interpretation of field descriptors

FieldType term Type Interpretation
B byte signed byte
C char Unicode character code point in the Basic Multilingual Plane, encoded with UTF-16
D double double-precision floating-point value
F float single-precision floating-point value
I int integer
J long long integer
L ClassName ; reference Named class or interface type an instance of class ClassName
S short signed short
Z boolean true or false
[ reference Array of given component type one array dimension

The field descriptor of an instance variable of type int is simply I.

The field descriptor of an instance variable of type Object is Ljava/lang/Object;. Note that the internal form of the binary name for class Object is used.

The field descriptor of an instance variable of the multidimensional array type double[][][] is [[[D.

The "Interpretation" column of Table 4.3-A is redundant; these details are better left to sections 2.2, 2.3 and 2.4.

4.3.3 Method Descriptors

A method descriptor contains zero or more parameter descriptors, representing the types of parameters that the method takes, and a return descriptor, representing the type of the value (if any) that the method returns.

MethodDescriptor:
( {ParameterDescriptor} ) ReturnDescriptor
ParameterDescriptor:
FieldType
ReturnDescriptor:
FieldType
VoidDescriptor
VoidDescriptor:
V

The character V indicates that the method returns no value (its result is void).

A method descriptor mentions a class or interface name if the name appears as a ClassName in the FieldType of a parameter descriptor or return descriptor.

The method descriptor for the method:

Object m(int i, double d, Thread t) {...}

is:

(IDLjava/lang/Thread;)Ljava/lang/Object;

Note that the internal forms of the binary names of Thread and Object are used.

A method descriptor is valid only if it represents method parameters with a total length of 255 or less, where that length includes the contribution for this in the case of instance or interface method invocations. The total length is calculated by summing the contributions of the individual parameters, where a parameter of type long or double contributes two units to the length and a parameter of any other type contributes one unit.

A method descriptor is the same whether the method it describes is a class method or an instance method. Although an instance method is passed this, a reference to the object on which the method is being invoked, in addition to its intended arguments, that fact is not reflected in the method descriptor. The reference to this is passed implicitly by the Java Virtual Machine instructions which invoke instance methods (2.6.1, 4.11).

4.7 Attributes

4.7.16 The RuntimeVisibleAnnotations Attribute

4.7.16.1 The element_value structure

...

class_info_index

The class_info_index item denotes a class literal as the value of this element-value pair.

The class_info_index item must be a valid index into the constant_pool table. The constant_pool entry at that index must be a CONSTANT_Utf8_info structure (4.4.7) representing a return descriptor (4.3.3). The return descriptor gives the type corresponding to the class literal represented by this element_value structure. Types correspond to class literals as follows:

  • For a class literal C.class, where C is the name of a class, or interface, or array type, the corresponding type is C. The return descriptor in the constant_pool will be an ObjectType or an ArrayType a ClassType.

  • For a class literal T[].class, where T[] is an array type, the corresponding type is T[]. The return descriptor in the constant_pool will be an ArrayType.

  • For a class literal p.class, where p is the name of a primitive type, the corresponding type is p. The return descriptor in the constant_pool will be a BaseType character.

  • For a class literal void.class, the corresponding type is void. The return descriptor in the constant_pool will be V.

For example, the class literal Object.class corresponds to the type Object, so the constant_pool entry is Ljava/lang/Object;, whereas the class literal int.class corresponds to the type int, so the constant_pool entry is I.

The class literal void.class corresponds to void, so the constant_pool entry is V, whereas the class literal Void.class corresponds to the type Void, so the constant_pool entry is Ljava/lang/Void;.

...

4.9 Constraints on Java Virtual Machine Code

The code for a method, instance initialization method (2.9.1), or class or interface initialization method (2.9.2) is stored in the code array of the Code attribute of a method_info structure of a class file (4.7.3). This section describes the constraints associated with the contents of the Code_attribute structure.

Initialization methods are methods. No need to call them out separately.

4.9.1 Static Constraints

The static constraints on a class file are those defining the well-formedness of the file. These constraints have been given in the previous sections, except for static constraints on the code in the class file. The static constraints on the code in a class file specify how Java Virtual Machine instructions must be laid out in the code array and what the operands of individual instructions must be.

The static constraints on the instructions in the code array are as follows:

The static constraints on the operands of instructions in the code array are as follows:

4.9.2 Structural Constraints

The structural constraints on the code array specify constraints on relationships between Java Virtual Machine instructions. The structural constraints are as follows:

4.10 Verification of class Files

4.10.1 Verification by Type Checking

4.10.1.1 Accessors for Java Virtual Machine Artifacts

We stipulate the existence of 28 Prolog predicates ("accessors") that have certain expected behavior but whose formal definitions are not given in this specification.

classClassName(Class, ClassName)

Extracts the name, ClassName, of the class Class.

classIsInterface(Class)

True iff the class, Class, is an interface.

classIsNotFinal(Class)

True iff the class, Class, is not a final class.

classSuperClassName(Class, SuperClassName)

Extracts the name, SuperClassName, of the superclass of class Class.

classInterfaces(Class, Interfaces) classInterfaceNames(Class, InterfaceNames)

Extracts a list, Interfaces InterfaceNames, of the names of the direct superinterfaces of the class Class.

classMethods(Class, Methods)

Extracts a list, Methods, of the methods declared in the class Class.

classAttributes(Class, Attributes)

Extracts a list, Attributes, of the attributes of the class Class.

Each attribute is represented as a functor application of the form attribute(AttributeName, AttributeContents), where AttributeName is the name of the attribute. The format of the attribute's contents is unspecified.

classDefiningLoader(Class, Loader)

Extracts the defining class loader, Loader, of the class Class.

isBootstrapLoader(Loader)

True iff the class loader Loader is the bootstrap class loader.

loadedClass(Name, InitiatingLoader, ClassDefinition)

True iff there exists a class named Name whose representation (in accordance with this specification) when loaded by the class loader InitiatingLoader is ClassDefinition.

methodName(Method, Name)

Extracts the name, Name, of the method Method.

methodAccessFlags(Method, AccessFlags)

Extracts the access flags, AccessFlags, of the method Method.

methodDescriptor(Method, Descriptor)

Extracts the descriptor, Descriptor, of the method Method.

methodAttributes(Method, Attributes)

Extracts a list, Attributes, of the attributes of the method Method.

isInit(Method)

True iff Method (regardless of class) is <init>.

isNotInit(Method)

True iff Method (regardless of class) is not <init>.

isNotFinal(Method, Class)

True iff Method in class Class is not final.

isStatic(Method, Class)

True iff Method in class Class is static.

isNotStatic(Method, Class)

True iff Method in class Class is not static.

isPrivate(Method, Class)

True iff Method in class Class is private.

isNotPrivate(Method, Class)

True iff Method in class Class is not private.

isProtected(MemberClass, MemberName, MemberDescriptor)

True iff there is a member named MemberName with descriptor MemberDescriptor in the class MemberClass and it is protected.

isNotProtected(MemberClass, MemberName, MemberDescriptor)

True iff there is a member named MemberName with descriptor MemberDescriptor in the class MemberClass and it is not protected.

parseFieldDescriptor(Descriptor, Type)

Converts a field descriptor, Descriptor, into the corresponding verification type Type (4.10.1.2).

The verification type derived from descriptor types byte, short, boolean, and char is int.

parseMethodDescriptor(Descriptor, ArgTypeList, ReturnType)

Converts a method descriptor, Descriptor, into a list of verification types, ArgTypeList, corresponding to the method argument types, and a verification type, ReturnType, corresponding to the return type.

The verification type derived from descriptor types byte, short, boolean, and char is int. A void return is represented with the special symbol void.

parseCodeAttribute(Class, Method, FrameSize, MaxStack, ParsedCode, Handlers, StackMap)

Extracts the instruction stream, ParsedCode, of the method Method in Class, as well as the maximum operand stack size, MaxStack, the maximal number of local variables, FrameSize, the exception handlers, Handlers, and the stack map StackMap.

The representation of the instruction stream and stack map attribute must be as specified in 4.10.1.3 and 4.10.1.4.

samePackageName(Class1, Class2)

True iff the package names of Class1 and Class2 are the same.

differentPackageName(Class1, Class2)

True iff the package names of Class1 and Class2 are different.

The above accessors are used to define loadedSuperclasses, which produces a list of a class's superclasses.

loadedSuperclasses(Class, [ Superclass | Rest ]) :-
    classSuperClassName(Class, SuperclassName),
    classDefiningLoader(Class, L),
    loadedClass(SuperclassName, L, Superclass),
    loadedSuperclasses(Superclass, Rest).

loadedSuperclasses(Class, []) :-
    classClassName(Class, 'java/lang/Object'),
    classDefiningLoader(Class, BL),
    isBootstrapLoader(BL).

The loadedSuperclasses predicate replaces superclassChain (4.10.1.2), which had the same effect, but produced a list of class types rather than loaded classes. (Despite the change in representation, all superclasses are loaded in either case.)

This helps reduce reliance on class types when what is really wanted is classes. The verifier already has a first-class notion of a class, a black-box "live" representation of a loaded class file. Using an extra layer of indirection to encode these classes as verification type structures is unnecessary and risks problems when the type system evolves.

When type checking a method's body, it is convenient to access information about the method. For this purpose, we define an environment, a six-tuple consisting of:

We specify accessors to extract information from the environment.

allInstructions(Environment, Instructions) :-
    Environment = environment(_Class, _Method, _ReturnType,
                              Instructions, _, _).

exceptionHandlers(Environment, Handlers) :-
    Environment = environment(_Class, _Method, _ReturnType,
                              _Instructions, _, Handlers).

maxOperandStackLength(Environment, MaxStack) :-
    Environment = environment(_Class, _Method, _ReturnType,
                              _Instructions, MaxStack, _Handlers).
currentClassLoader(Environment, Loader) :-
    Environment = environment(Class, _Method, _ReturnType,
                              _Instructions, _, _),
    classDefiningLoader(Class, L).
thisClass(Environment, class(ClassName, L)) :-
    Environment = environment(Class, _Method, _ReturnType,
                              _Instructions, _, _),
    classDefiningLoader(Class, L),
    classClassName(Class, ClassName).
thisClass(Environment, Class) :-
    Environment = environment(Class, _Method, _ReturnType,
                              _Instructions, _, _).

thisType(Environment, class(ClassName, L)) :-
    Environment = environment(Class, _Method, _ReturnType,
                              _Instructions, _, _),
    classDefiningLoader(Class, L),
    classClassName(Class, ClassName).
thisMethodReturnType(Environment, ReturnType) :-
    Environment = environment(_Class, _Method, ReturnType,
                              _Instructions, _, _).

We specify additional predicates to extract higher-level information from the environment.

offsetStackFrame(Environment, Offset, StackFrame) :-
    allInstructions(Environment, Instructions),
    member(stackMap(Offset, StackFrame), Instructions).
currentClassLoader(Environment, Loader) :-
    thisClass(Environment, class(_, Loader)).

The old thisClass predicate operated on types, not classes. While both are useful, often it's unnecessary to work with types, so thisClass now operates on a live class; thisType preserves the old behavior.

These changes are made to reduce reliance on class types when what is really wanted is classes. The verifier already has a first-class notion of a class, a black-box "live" representation of a loaded class file. Using an extra layer of indirection to encode these classes as verification type structures is unnecessary and risks problems when the type system evolves. :::

Finally, we specify a general predicate used throughout the type rules:

notMember(_, []).
notMember(X, [A | More]) :- X \= A, notMember(X, More).

The principle guiding the determination as to which accessors are stipulated and which are fully specified is that we do not want to over-specify the representation of the class file. Providing specific accessors to the Class or Method term would force us to completely specify the format for a Prolog term representing the class file.

4.10.1.2 Verification Type System

The type checker enforces a type system based upon a hierarchy of verification types, illustrated below.

Verification type hierarchy:

                             top
                 ____________/\____________
                /                          \
               /                            \
            oneWord                       twoWord
           /   |   \                     /       \
          /    |    \                   /         \
        int  float  reference        long        double
                     /     \
                    /       \_____________
                   /                      \
                  /                        \
           uninitialized                    +---------------------+
            /         \                     |  Java reference     |
            /         \                     |  reference          |
           /           \                    |  type hierarchy     |
uninitializedThis  uninitialized(Offset)    +---------------------+
                                                     |
                                                     |
                                                    null

The "reference type hierarchy" was previously referred to as the "Java reference type hierarchy". But the reference type subtyping graph doesn't rely on the Java language at all, and in fact, as of Java 5, differs significantly from it.

Most verification types have a direct correspondence with the primitive and reference types described in 2.2 and represented by field descriptors in Table 4.3-A:

The remaining verification types are described as follows:

The subtyping rules for verification types are as follows.

Subtyping is reflexive.

isAssignable(X, X).

The verification types which are not reference types in the Java programming language have subtype rules of the form:

isAssignable(v, X) :- isAssignable(the_direct_supertype_of_v, X).

That is, v is a subtype of X if the direct supertype of v is a subtype of X. The rules are:

The type top is a supertype of all other types.

isAssignable(oneWord, top).
isAssignable(twoWord, top).

A type is a subtype of some other type, X, if its direct supertype is a subtype of X.

isAssignable(int, X)    :- isAssignable(oneWord, X).
isAssignable(float, X)  :- isAssignable(oneWord, X).
isAssignable(long, X)   :- isAssignable(twoWord, X).
isAssignable(double, X) :- isAssignable(twoWord, X).

isAssignable(reference, X)   :- isAssignable(oneWord, X).
isAssignable(class(_, _), X) :- isAssignable(reference, X).
isAssignable(arrayOf(_), X)  :- isAssignable(reference, X).
isAssignable(null, X) :- isAssignable(reference, X).
isAssignable(uninitialized, X)     :- isAssignable(reference, X).
isAssignable(uninitializedThis, X) :- isAssignable(uninitialized, X).
isAssignable(uninitialized(_), X)  :- isAssignable(uninitialized, X).

The type null is a subtype of all reference types.

isAssignable(null, class(_, _)).
isAssignable(null, arrayOf(_)).
isAssignable(null, X) :- isAssignable(class('java/lang/Object', BL), X),
                         isBootstrapLoader(BL).

These subtype rules are not necessarily the most obvious formulation of subtyping. There is a clear split between subtyping rules for reference types in the Java programming language among reference types, and rules for the remaining verification types. The split allows us to state general subtyping relations between Java programming language reference types and other verification types. These relations hold independently of a Java reference type's position in the type hierarchy, and help to prevent excessive class loading by a Java Virtual Machine implementation. For example, we do not want to start climbing the Java superclass hierarchy in response to a query of the form class(foo, L) <: twoWord.

We also have a rule that says subtyping is reflexive, so together these rules cover most verification types that are not reference types in the Java programming language.

Subtype rules for the reference types in the Java programming language are specified recursively with isJavaAssignable isWideningReference.

isAssignable(class(X, Lx), class(Y, Ly)) :-
    isJavaAssignable(class(X, Lx), class(Y, Ly)).

isAssignable(arrayOf(X), class(Y, L)) :-
    isJavaAssignable(arrayOf(X), class(Y, L)).

isAssignable(arrayOf(X), arrayOf(Y)) :-
    isJavaAssignable(arrayOf(X), arrayOf(Y)).
isAssignable(From, To) :- isWideningReference(From, To).

The isWideningReference predicate is only defined for reference types, and will fail to match any non-reference inputs. So it's unnecessary to restrict the form of the inputs to avoid testing non-referene types.

For assignments, interfaces are treated like Object. The verifier allows any reference type to be widened to an interface type.

isJavaAssignable(class(_, _), class(To, L)) :-
    loadedClass(To, L, ToClass),
    classIsInterface(ToClass).
isWideningReference(class(_, _), class(To, L)) :-
    loadedClass(To, L, ToClass),
    classIsInterface(ToClass).

isWideningReference(arrayOf(_), class(To, L)) :-
    loadedClass(To, L, ToClass),
    classIsInterface(ToClass).

This approach is less strict than the Java Programming Language, which will not allow an assignment to an interface unless the value is statically known to implement or extend the interface. The Java Virtual Machine instead uses a run-time check to ensure that invocations of interface methods actually operate on objects that implement the interface (6.5.invokeinterface). But there is no requirement that a reference stored by a local variable of an interface type refers to an object that actually implements that interface.

A class type can be widened to another class type if that type refers to the loaded class or one of its superclasses.

isJavaAssignable(From, To) :-
    isJavaSubclassOf(From, To).
isWideningReference(class(ClassName, L1), class(ClassName, L2)) :-
    L1 \= L2,
    loadedClass(ClassName, L1, Class),
    loadedClass(ClassName, L2, Class).

isWideningReference(class(From, L1), class(To, L2)) :-
    From \= To,
    loadedClass(From, L1, FromClass),
    loadedClass(To, L2, ToClass),
    loadedSuperclases(FromClass, Supers),
    member(ToClass, Supers).

A bug in the previous rules failed to allow the same class to be treated as a subtype of itself when referenced in the context of different initiating class loaders. It's not clear if this has any practical impact (are subtype tests ever performed between types referenced from different classes?), but the first rule above addresses it.

In the case in which two class types have the same name and the same initiating class loader, neither of these rules apply. If the types are the same, that's an identity, not a widening. The reflexive isAssignable rule applies, and the class should not be loaded.

Array types are subtypes of Object. The intent is also that array types are subtypes of Cloneable and java.io.Serializable.

isJavaAssignable(arrayOf(_), class('java/lang/Object', BL)) :-
    isBootstrapLoader(BL).

isJavaAssignable(arrayOf(_), X) :-
    isArrayInterface(X).

isArrayInterface(class('java/lang/Cloneable', BL)) :-
    isBootstrapLoader(BL).

isArrayInterface(class('java/io/Serializable', BL)) :-
    isBootstrapLoader(BL).
isWideningReference(arrayOf(_), class('java/lang/Object', L)) :-
    loadedClass('java/lang/Object', L, ObjectClass),
    classDefiningLoader(ObjectClass, BL),
    isBootstrapLoader(BL).

A bug in the previous rules fails to treat array types as subtypes of class('java/lang/Object', L) unless L is the bootstrap loader. Since L is the initiating loader, that rule failed to support the common case of java/lang/Object being referenced outside of bootstrap classes.

The previous rules also fail to allow an array type to be treated as a subtype of an arbitrary interface type. In practice, it is possible to, say, pass an array as an argument to a method expecting a Runnable. The earlier rules for interface types address this, making it unnecessary to single out Cloneable and Serializable for special treatment.

Subtyping between arrays of primitive type is the identity relation.

isJavaAssignable(arrayOf(X), arrayOf(Y)) :-
    atom(X),
    atom(Y),
    X = Y.

Subtyping between arrays of reference type is covariant.

isJavaAssignable(arrayOf(X), arrayOf(Y)) :-
    compound(X), compound(Y), isJavaAssignable(X, Y).
isWideningReference(arrayOf(X), arrayOf(Y)) :-
    isWideningReference(X, Y).

The subtyping rule for arrays of primitive types is an identity conversion, not a widening; and it is already covered by the reflexive rule for isAssignable.

The subtyping rule for arrays of reference types does not need to check that the inputs are reference types—if not, isWideningReference will not succeed.

Subclassing is reflexive.

isJavaSubclassOf(class(SubclassName, L), class(SubclassName, L)).
isJavaSubclassOf(class(SubclassName, LSub), class(SuperclassName, LSuper)) :-
    superclassChain(SubclassName, LSub, Chain),
    member(class(SuperclassName, L), Chain),
    loadedClass(SuperclassName, L, Sup),
    loadedClass(SuperclassName, LSuper, Sup).

This relation is expressed directly with isWideningReference, above. No need to introduce another predicate.

superclassChain(ClassName, L, [class(SuperclassName, Ls) | Rest]) :-
    loadedClass(ClassName, L, Class),
    classSuperClassName(Class, SuperclassName),
    classDefiningLoader(Class, Ls),
    superclassChain(SuperclassName, Ls, Rest).

superclassChain('java/lang/Object', L, []) :-
    loadedClass('java/lang/Object', L, Class),
    classDefiningLoader(Class, BL),
    isBootstrapLoader(BL).

This predicate is moved to 4.10.1.1 and renamed loadedSuperclasses.

4.10.1.3 Instruction Representation

Bug fix: member references and instructions like checkcast and ldc can refer to array types, so CONSTANT_Class structures need to be encoded as types, not class names.

Individual bytecode instructions are represented in Prolog as terms whose functor is the name of the instruction and whose arguments are its parsed operands.

For example, an aload instruction is represented as the term aload(N), which includes the index N that is the operand of the instruction.

The instructions as a whole are represented as a list of terms of the form:

instruction(Offset, AnInstruction)

For example, instruction(21, aload(1)).

The order of instructions in this list must be the same as in the class file.

Some instructions have operands that refer to entries in the constant_pool table representing fields, methods, and dynamically-computed call sites. Such entries are represented as functor applications of the form:

We've combined the two lists of constant forms into one. Because CONSTANT_Class_info is relevant to both lists, it's awkward to keep the two separate. It would require, say, a forward reference from the first list to the second.

For clarity, we assume that field and method descriptors (4.3.2, 4.3.3) are mapped into more readable names: the leading L and trailing ; are dropped from class names, and the BaseType characters used for primitive types are mapped to the names of those types.

The descriptor should always be processed with parseFieldDescriptor, so its format doesn't need to be specified.

For example, a getfield instruction whose operand refers to a constant pool entry representing a field foo of type F in class Bar would be represented as getfield(field('Bar', 'foo', 'F')) getfield(field(class('Bar', L), 'foo', 'F')), where L is the class loader of the class containing the instruction. An ldc instruction for loading the int constant 91 would be represented as ldc(int(91)).

The ldc instruction, among others, has an operand that refers to a loadable entry in the constant_pool table. There are nine kinds of loadable entry (see Table 4.4-C), represented by functor applications of the following forms:

4.10.1.6 Type Checking Methods with Code

...

For the initial type state of an instance method, we compute the type of this and put it in a list. The type of this in the <init> method of Object is Object; in other <init> methods, the type of this is uninitializedThis; otherwise, the type of this in an instance method is class(N, L) where N is the name of the class containing the method and L is its defining class loader.

For the initial type state of a static method, this is irrelevant, so the list is empty.

methodInitialThisType(_Class, Method, []) :-
    methodAccessFlags(Method, AccessFlags),
    member(static, AccessFlags),
    methodName(Method, MethodName),
    MethodName \= '`<init>`'.
methodInitialThisType(_Class, Method, []) :-
    methodAccessFlags(Method, AccessFlags),
    member(static, AccessFlags).

An instance initialization method cannot be static, so checking for it is redundant.

methodInitialThisType(Class, Method, [This]) :-
    methodAccessFlags(Method, AccessFlags),
    notMember(static, AccessFlags),
    instanceMethodInitialThisType(Class, Method, This).

instanceMethodInitialThisType(Class, Method, class('java/lang/Object', L)) :-
    methodName(Method, '`<init>`'),
    classDefiningLoader(Class, L),
    isBootstrapLoader(L),
    classClassName(Class, 'java/lang/Object').
instanceMethodInitialThisType(Class, Method, uninitializedThis) :-
    methodName(Method, '`<init>`'),
    classClassName(Class, ClassName),
    classDefiningLoader(Class, CurrentLoader),
    superclassChain(ClassName, CurrentLoader, Chain),
    Chain \= [].
instanceMethodInitialThisType(Class, Method, uninitializedThis) :-
    methodName(Method, '`<init>`'),
    loadedSuperclasses(Class, Supers),
    Supers \= [].
instanceMethodInitialThisType(Class, Method, class(ClassName, L)) :-
    methodName(Method, MethodName),
    MethodName \= '`<init>`',
    classDefiningLoader(Class, L),
    classClassName(Class, ClassName).

...

4.10.1.8 Type Checking for protected Members

Member references can refer to array types, so the rules in this section need to be defined in terms of a type, not a class name.

All instructions that access members must contend with the rules concerning protected members. This section describes the protected check that corresponds to JLS §6.6.2.1.

The protected check applies only to protected members of superclasses of the current class. protected members in other classes will be caught by the access checking done at resolution (5.4.4). There are four cases:

The predicate classesInOtherPkgWithProtectedMember(Class, MemberName, MemberDescriptor, MemberClassName, Chain, List) is true if List is the set of classes in Chain with name MemberClassName that are in a different run-time package than Class which have a protected member named MemberName with descriptor MemberDescriptor.

classesInOtherPkgWithProtectedMember(_, _, _, _, [], []).
classesInOtherPkgWithProtectedMember(Class, MemberName,
                                     MemberDescriptor, MemberClassName,
                                     [class(MemberClassName, L) | Tail],
                                     [class(MemberClassName, L) | T]) :-
    differentRuntimePackage(Class, class(MemberClassName, L)),
    loadedClass(MemberClassName, L, Super),
    isProtected(Super, MemberName, MemberDescriptor),
    classesInOtherPkgWithProtectedMember(
      Class, MemberName, MemberDescriptor, MemberClassName, Tail, T).
classesInOtherPkgWithProtectedMember(Class, MemberName,
                                     MemberDescriptor, MemberClassName,
                                     [Super | Tail],
                                     [Super | T]) :-
    classClassName(Super, MemberClassName),
    differentRuntimePackage(Class, Super),
    isProtected(Super, MemberName, MemberDescriptor),
    classesInOtherPkgWithProtectedMember(
      Class, MemberName, MemberDescriptor, MemberClassName, Tail, T).
classesInOtherPkgWithProtectedMember(Class, MemberName,
                                     MemberDescriptor, MemberClassName,
                                     [class(MemberClassName, L) | Tail],
                                     T) :-
    differentRuntimePackage(Class, class(MemberClassName, L)),
    loadedClass(MemberClassName, L, Super),
    isNotProtected(Super, MemberName, MemberDescriptor),
    classesInOtherPkgWithProtectedMember(
      Class, MemberName, MemberDescriptor, MemberClassName, Tail, T).
classesInOtherPkgWithProtectedMember(Class, MemberName,
                                     MemberDescriptor, MemberClassName,
                                     [Super | Tail],
                                     T) :-
    classClassName(Super, MemberClassName),
    differentRuntimePackage(Class, Super),
    isNotProtected(Super, MemberName, MemberDescriptor),
    classesInOtherPkgWithProtectedMember(
      Class, MemberName, MemberDescriptor, MemberClassName, Tail, T).
classesInOtherPkgWithProtectedMember(Class, MemberName,
                                     MemberDescriptor, MemberClassName,
                                     [class(MemberClassName, L) | Tail],
                                     T] :-
    sameRuntimePackage(Class, class(MemberClassName, L)),
    classesInOtherPkgWithProtectedMember(
      Class, MemberName, MemberDescriptor, MemberClassName, Tail, T).
classesInOtherPkgWithProtectedMember(Class, MemberName,
                                     MemberDescriptor, MemberClassName,
                                     Super | Tail],
                                     T) :-
    classClassName(Super, MemberClassName),
    sameRuntimePackage(Class, Super),
    classesInOtherPkgWithProtectedMember(
      Class, MemberName, MemberDescriptor, MemberClassName, Tail, T).
sameRuntimePackage(Class1, Class2) :-
    classDefiningLoader(Class1, L),
    classDefiningLoader(Class2, L),
    samePackageName(Class1, Class2).

differentRuntimePackage(Class1, Class2) :-
    classDefiningLoader(Class1, L1),
    classDefiningLoader(Class2, L2),
    L1 \= L2.

differentRuntimePackage(Class1, Class2) :-
    differentPackageName(Class1, Class2).
4.10.1.9 Type Checking Instructions
getfield

A getfield instruction with operand CP is type safe iff CP refers to a constant pool entry denoting a field whose declared type is FieldType, declared in a class FieldClassName type FieldClassType, and one can validly replace a type matching FieldClassName FieldClassType with type FieldType on the incoming operand stack yielding the outgoing type state. FieldClassName must not be an array type. protected fields are subject to additional checks (4.10.1.8).

Array types are allowed here.

instructionIsTypeSafe(getfield(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    CP = field(FieldClassName, FieldName, FieldDescriptor),
    CP = field(FieldClassType, FieldName, FieldDescriptor),
    parseFieldDescriptor(FieldDescriptor, FieldType),
    passesProtectedCheck(Environment, FieldClassName, FieldName,
                         FieldDescriptor, StackFrame),
    currentClassLoader(Environment, CurrentLoader),
    validTypeTransition(Environment,
                        [class(FieldClassName, CurrentLoader)], FieldType,
                        StackFrame, NextStackFrame),
    passesProtectedCheck(Environment, FieldClassType, FieldName,
                         FieldDescriptor, StackFrame),
    validTypeTransition(Environment, [FieldClassType], FieldType,
                        StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).
getstatic

A getstatic instruction with operand CP is type safe iff CP refers to a constant pool entry denoting a field whose declared type is FieldType, and one can validly push FieldType on the incoming operand stack yielding the outgoing type state.

instructionIsTypeSafe(getstatic(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    CP = field(_FieldClassName, _FieldName, FieldDescriptor),
    CP = field(_FieldClassType, _FieldName, FieldDescriptor),
    parseFieldDescriptor(FieldDescriptor, FieldType),
    validTypeTransition(Environment, [], FieldType,
                        StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).
invokeinterface

An invokeinterface instruction is type safe iff all of the following are true:

instructionIsTypeSafe(invokeinterface(CP, Count, 0), Environment, _Offset,
                      StackFrame, NextStackFrame, ExceptionStackFrame) :-
    CP = imethod(MethodIntfName, MethodName, Descriptor),
    CP = imethod(MethodClassType, _MethodName, Descriptor),
    MethodName \= '`<init>`',
    MethodName \= '`<clinit>`',
    parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
    currentClassLoader(Environment, CurrentLoader),
    reverse([class(MethodIntfName, CurrentLoader) | OperandArgList],
            StackArgList),
    reverse([MethodClassType | OperandArgList], StackArgList),
    canPop(StackFrame, StackArgList, TempFrame),
    validTypeTransition(Environment, [], ReturnType,
                        TempFrame, NextStackFrame),
    countIsValid(Count, StackFrame, TempFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

Array types are allowed here.

The Count operand of an invokeinterface instruction is valid if it equals the size of the arguments to the instruction. This is equal to the difference between the size of InputFrame and OutputFrame.

countIsValid(Count, InputFrame, OutputFrame) :-
    InputFrame = frame(_Locals1, OperandStack1, _Flags1),
    OutputFrame = frame(_Locals2, OperandStack2, _Flags2),
    length(OperandStack1, Length1),
    length(OperandStack2, Length2),
    Count =:= Length1 - Length2.
invokespecial

An invokespecial instruction is type safe iff all of the following are true:

instructionIsTypeSafe(invokespecial(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    CP = method(MethodClassName, MethodName, Descriptor),
    (CP = method(MethodClassType, MethodName, Descriptor) ;
     CP = imethod(MethodClassType, MethodName, Descriptor)),
    MethodName \= '`<init>`',
    MethodName \= '`<clinit>`',
    validSpecialMethodClassType(Environment, MethodClassType),
    parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
    thisClass(Environment, class(CurrentClassName, CurrentLoader)),
    isAssignable(class(CurrentClassName, CurrentLoader),
                 class(MethodClassName,  CurrentLoader)),
    reverse([class(CurrentClassName, CurrentLoader) | OperandArgList],
            StackArgList),
    thisType(Environment, ThisType),
    reverse([ThisType | OperandArgList], StackArgList),
    validTypeTransition(Environment, StackArgList, ReturnType,
                        StackFrame, NextStackFrame),
    reverse([class(MethodClassName, CurrentLoader) | OperandArgList],
            StackArgList2),
    validTypeTransition(Environment, StackArgList2, ReturnType,
                        StackFrame, _ResultStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).
validSpecialMethodClassType(Environment, class(MethodClassName, L)) :-
    loadedClass(MethodClassName, L, MethodClass),
    \+ classIsInterface(MethodClass),
    thisClass(Environment, ThisClass),
    loadedSuperclasses(ThisClass, Supers),
    member(MethodClass, Supers).

validSpecialMethodClassType(Environment, class(MethodClassName, L)) :-
    loadedClass(MethodClassName, L, MethodClass),
    classIsInterface(MethodClass),
    thisClass(Environment, ThisClass),
    classInterfaceNames(ThisClass, InterfaceNames),
    member(MethodClassName, InterfaceNames).

Interface methods are allowed here (4.9.1).

The old rules attempt to enforce the constraints on MethodClassName via an isAssignable call, deferring some complexity to subtype testing. Unfortunately, this isn't correct for interfaces: every reference type is "assignable" to every interface type.

In practice, Hotspot appears to perform the following check:

This allows, for example, the name of a valid interface that is not related to the current class to appear in a Methodref. Verification succeeds, and no error occurs until resolution of the Methodref.

That's some unnecessary complexity that doesn't quite align with 4.9.2. Instead, these new rules directly test for a valid class/interface name: the current class, a superclass, or a direct superinterface. The rules do some class loading, but note that the same loading occurred before in the isAssignable test.

Another problem with the old rules is a redundant subtyping check via validTypeTransition. Given that CurrentClass <: MethodClassType and the stack operand <: CurrentClass, there's no need to also check that the stack operand <: MethodClassType.

Array types are syntactically allowed here, but the validSpecialMethodClassType clause will reject them.

The isAssignable validSpecialMethodClassType clause enforces the structural constraint that invokespecial, for other than an instance initialization method, must name a method in the current class/interface or a superclass/superinterface.

The first validTypeTransition clause enforces the structural constraint that invokespecial, for other than an instance initialization method, targets a receiver object of the current class or deeper. To see why, consider that StackArgList simulates the list of types on the operand stack expected by the method, starting with the current class (the class performing invokespecial). The actual types on the operand stack are in StackFrame. The effect of validTypeTransition is to pop the first type from the operand stack in StackFrame and check it is a subtype of the first term of StackArgList, namely the current class. Thus, the actual receiver type is compatible with the current class.

A sharp-eyed reader might notice that enforcing this structural constraint supercedes the structural constraint pertaining to invokespecial of a protected method. Thus, the Prolog code above makes no reference to passesProtectedCheck (4.10.1.8), whereas the Prolog code for invokespecial of an instance initialization method uses passesProtectedCheck to ensure the actual receiver type is compatible with the current class when certain protected instance initialization methods are named.

The second validTypeTransition clause enforces the structural constraint that any method invocation instruction must target a receiver object whose type is compatible with the type named by the instruction. To see why, consider that StackArgList2 simulates the list of types on the operand stack expected by the method, starting with the type named by the instruction. Again, the actual types on the operand stack are in StackFrame, and the effect of validTypeTransition is to check the actual receiver type in StackFrame is compatible with the type named by the instruction in StackArgList2.

instructionIsTypeSafe(invokespecial(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    CP = method(MethodClassName, '`<init>`', Descriptor),
    (CP = method(MethodClassType, '`<init>`', Descriptor) ;
     CP = imethod(MethodClassType, '`<init>`', Descriptor)),
    parseMethodDescriptor(Descriptor, OperandArgList, void),
    reverse(OperandArgList, StackArgList),
    canPop(StackFrame, StackArgList, TempFrame),
    TempFrame = frame(Locals, [uninitializedThis | OperandStack], Flags),
    currentClassLoader(Environment, CurrentLoader),
    rewrittenUninitializedType(uninitializedThis, Environment,
                               class(MethodClassName, CurrentLoader), This),
    rewrittenUninitializedType(uninitializedThis, Environment,
                               MethodClassType, This),
    rewrittenInitializationFlags(uninitializedThis, Flags, NextFlags),
    substitute(uninitializedThis, This, OperandStack, NextOperandStack),
    substitute(uninitializedThis, This, Locals, NextLocals),
    NextStackFrame = frame(NextLocals, NextOperandStack, NextFlags),
    ExceptionStackFrame = frame(Locals, [], Flags).
instructionIsTypeSafe(invokespecial(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    CP = method(MethodClassName, '`<init>`', Descriptor),
    (CP = method(MethodClassType, '`<init>`', Descriptor) ;
     CP = imethod(MethodClassType, '`<init>`', Descriptor)),
    parseMethodDescriptor(Descriptor, OperandArgList, void),
    reverse(OperandArgList, StackArgList),
    canPop(StackFrame, StackArgList, TempFrame),
    TempFrame = frame(Locals, [uninitialized(Address) | OperandStack], Flags),
    currentClassLoader(Environment, CurrentLoader),
    rewrittenUninitializedType(uninitialized(Address), Environment,
                               class(MethodClassName, CurrentLoader), This),
    rewrittenUninitializedType(uninitialized(Address), Environment,
                               MethodClassType, This),
    rewrittenInitializationFlags(uninitialized(Address), Flags, NextFlags),
    substitute(uninitialized(Address), This, OperandStack, NextOperandStack),
    substitute(uninitialized(Address), This, Locals, NextLocals),
    NextStackFrame = frame(NextLocals, NextOperandStack, NextFlags),
    ExceptionStackFrame = frame(Locals, [], Flags),
    passesProtectedCheck(Environment, MethodClassName, '`<init>`',
                         Descriptor, NextStackFrame).
    passesProtectedCheck(Environment, MethodClassType, '`<init>`',
                         Descriptor, NextStackFrame).

Array types are syntactically allowed here, but the rewrittenUninitializedType clause will reject them.

I've confirmed that Hotspot behavior in JDK 13 is to allow interface method references named <init>, delaying any errors until resolution/runtime.

To compute what type the uninitialized argument's type needs to be rewritten to, there are two cases:

rewrittenUninitializedType(uninitializedThis, Environment,
                           MethodClass, MethodClass) :-
    MethodClass = class(MethodClassName, CurrentLoader),
    thisClass(Environment, MethodClass).
rewrittenUninitializedType(uninitializedThis, Environment,
                           MethodClassType, MethodClassType) :-
    thisType(Environment, MethodClassType).
rewrittenUninitializedType(uninitializedThis, Environment,
                           MethodClass, MethodClass) :-
    MethodClass = class(MethodClassName, CurrentLoader),
    thisClass(Environment, class(thisClassName, thisLoader)),
    superclassChain(thisClassName, thisLoader, [MethodClass | Rest]).
rewrittenUninitializedType(uninitializedThis, Environment,
                           MethodClassType, MethodClassType) :-
    MethodClassType = class(MethodClassName, _),
    thisClass(Environment, ThisClass),
    classSuperClassName(ThisClass, MethodClassName).
rewrittenUninitializedType(uninitialized(Address), Environment,
                           MethodClass, MethodClass) :-
    allInstructions(Environment, Instructions),
    member(instruction(Address, new(MethodClass)), Instructions).
rewrittenUninitializedType(uninitialized(Address), Environment,
                           MethodClassType, MethodClassType) :-
    allInstructions(Environment, Instructions),
    member(instruction(Address, new(MethodClassType)), Instructions).
rewrittenInitializationFlags(uninitializedThis, _Flags, []).
rewrittenInitializationFlags(uninitialized(_), Flags, Flags).

substitute(_Old, _New, [], []).
substitute(Old, New, [Old | FromRest], [New | ToRest]) :-
    substitute(Old, New, FromRest, ToRest).
substitute(Old, New, [From1 | FromRest], [From1 | ToRest]) :-
    From1 \= Old,
    substitute(Old, New, FromRest, ToRest).

The rule for invokespecial of an <init> method is the sole motivation for passing back a distinct exception stack frame. The concern is that when initializing an object within its constructor, invokespecial can cause a superclass <init> method to be invoked, and that invocation could fail, leaving this uninitialized. This situation cannot be created using source code in the Java programming language, but can be created by programming in bytecode directly.

In this situation, the original frame holds an uninitialized object in local variable 0 and has flag flagThisUninit. Normal termination of invokespecial initializes the uninitialized object and turns off the flagThisUninit flag. But if the invocation of an <init> method throws an exception, the uninitialized object might be left in a partially initialized state, and needs to be made permanently unusable. This is represented by an exception frame containing the broken object (the new value of the local) and the flagThisUninit flag (the old flag). There is no way to get from an apparently-initialized object bearing the flagThisUninit flag to a properly initialized object, so the object is permanently unusable.

If not for this situation, the flags of the exception stack frame would always be the same as the flags of the input stack frame.

invokestatic

An invokestatic instruction is type safe iff all of the following are true:

instructionIsTypeSafe(invokestatic(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    CP = method(_MethodClassName, MethodName, Descriptor),
    (CP = method(_MethodClassType, MethodName, Descriptor) ;
     CP = imethod(_MethodClassType, MethodName, Descriptor)),
    MethodName \= '`<init>`',
    MethodName \= '`<clinit>`',
    parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
    reverse(OperandArgList, StackArgList),
    validTypeTransition(Environment, StackArgList, ReturnType,
                        StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

Interface methods are allowed here (4.9.1).

invokevirtual

An invokevirtual instruction is type safe iff all of the following are true:

instructionIsTypeSafe(invokevirtual(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    CP = method(MethodClassName, MethodName, Descriptor),
    CP = method(MethodClassType, MethodName, Descriptor),
    MethodName \= '`<init>`',
    MethodName \= '`<clinit>`',
    parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
    reverse(OperandArgList, ArgList),
    currentClassLoader(Environment, CurrentLoader),
    reverse([class(MethodClassName, CurrentLoader) | OperandArgList],
            StackArgList),
    reverse([MethodClassType | OperandArgList], StackArgList),
    validTypeTransition(Environment, StackArgList, ReturnType,
                        StackFrame, NextStackFrame),
    canPop(StackFrame, ArgList, PoppedFrame),
    passesProtectedCheck(Environment, MethodClassName, MethodName,
                         Descriptor, PoppedFrame),
    passesProtectedCheck(Environment, MethodClassType, MethodName,
                         Descriptor, PoppedFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).
ldc, ldc_w, ldc2_w

An ldc instruction with operand CP is type safe iff CP refers to a constant pool entry denoting an entity of type Type, where Type is loadable (4.4), but not long or double, and one can validly push Type onto the incoming operand stack yielding the outgoing type state.

instructionIsTypeSafe(ldc(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    loadableConstant(CP, Type),
    Type \= long,
    Type \= double,
    validTypeTransition(Environment, [], Type, StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

loadableConstant(CP, Type) :-
    member([CP, Type], [
        [int(_),    int],
        [float(_),  float],
        [long(_),   long],
        [double(_), double]
    ]).
loadableConstant(CP, Type) :-
    isBootstrapLoader(BL),
    member([CP, Type], [
        [class(_),          class('java/lang/Class', BL)],
        [class(_,_),        class('java/lang/Class', BL)],
        [arrayOf(_),        class('java/lang/Class', BL)],
        [string(_),         class('java/lang/String', BL)],
        [methodHandle(_,_), class('java/lang/invoke/MethodHandle', BL)],
        [methodType(_,_),   class('java/lang/invoke/MethodType', BL)]
    ]).
loadableConstant(CP, Type) :-
    CP = dconstant(_, FieldDescriptor),
    parseFieldDescriptor(FieldDescriptor, Type).

An ldc_w instruction is type safe iff the equivalent ldc instruction is type safe.

instructionHasEquivalentTypeRule(ldc_w(CP), ldc(CP))

An ldc2_w instruction with operand CP is type safe iff CP refers to a constant pool entry denoting an entity of type Type, where Type is either long or double, and one can validly push Type onto the incoming operand stack yielding the outgoing type state.

instructionIsTypeSafe(ldc2_w(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    loadableConstant(CP, Type),
    (Type = long ; Type = double),
    validTypeTransition(Environment, [], Type, StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).
multianewarray

A multianewarray instruction with operands CP and Dim is type safe iff CP refers to a constant pool entry denoting an array type whose dimension is greater or equal to Dim, Dim is strictly positive, and one can validly replace Dim int types on the incoming operand stack with the type denoted by CP yielding the outgoing type state.

instructionIsTypeSafe(multianewarray(CP, Dim), Environment, _Offset,
                      StackFrame, NextStackFrame, ExceptionStackFrame) :-
    CP = arrayOf(_),
    classDimension(CP, Dimension),
    Dimension >= Dim,
    Dim > 0,
    /* Make a list of Dim ints */
    findall(int, between(1, Dim, _), IntList),
    validTypeTransition(Environment, IntList, CP,
                        StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

The dimension dimensions of an array type whose component type is also an array type is one more than the dimension dimensions of its component type.

classDimension(arrayOf(X), Dimension) :-
    classDimension(X, Dimension1),
    Dimension is Dimension1 + 1.

classDimension(_, Dimension) :-
    Dimension = 0.
arrayDimensions(arrayOf(X), XDimensions + 1) :-
    arrayDimensions(X, XDimensions).

arrayDimensions(Type, 0) :-
    Type \= arrayOf(_).

Renamed this predicate, since the element type is not necessarily a class type. Also addressed a bug: the second rule previously would match array types as well as non-array types.

putfield

A putfield instruction with operand CP is type safe iff all of the following are true:

instructionIsTypeSafe(putfield(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    CP = field(FieldClassName, FieldName, FieldDescriptor),
    CP = field(FieldClassType, FieldName, FieldDescriptor),
    parseFieldDescriptor(FieldDescriptor, FieldType),
    canPop(StackFrame, [FieldType], PoppedFrame),
    passesProtectedCheck(Environment, FieldClassName, FieldName,
                         FieldDescriptor, PoppedFrame),
    currentClassLoader(Environment, CurrentLoader),
    canPop(StackFrame, [FieldType, class(FieldClassName, CurrentLoader)],
           NextStackFrame),
    passesProtectedCheck(Environment, FieldClassType, FieldName,
                         FieldDescriptor, PoppedFrame),
    canPop(StackFrame, [FieldType, FieldClassType], NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).
instructionIsTypeSafe(putfield(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    CP = field(FieldClassName, _FieldName, FieldDescriptor),
    CP = field(FieldClassType, _FieldName, FieldDescriptor),
    parseFieldDescriptor(FieldDescriptor, FieldType),
    Environment = environment(CurrentClass, CurrentMethod, _, _, _, _),
    CurrentClass = class(FieldClassName, _),
    thisType(Environment, FieldClassType),
    Environment = environment(_, CurrentMethod, _, _, _, _),
    isInit(CurrentMethod),
    canPop(StackFrame, [FieldType, uninitializedThis], NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).
putstatic

A putstatic instruction with operand CP is type safe iff CP refers to a constant pool entry denoting a field whose declared type is FieldType, and one can validly pop a type matching FieldType off the incoming operand stack yielding the outgoing type state.

instructionIsTypeSafe(putstatic(CP), _Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    CP = field(_FieldClassName, _FieldName, FieldDescriptor),
    CP = field(_FieldClassType, _FieldName, FieldDescriptor),
    parseFieldDescriptor(FieldDescriptor, FieldType),
    canPop(StackFrame, [FieldType], NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

Chapter 5: Loading, Linking, and Initializing

5.4 Linking

5.4.2 Preparation

Preparation involves creating the static fields for a class or interface and initializing such fields to their default values (2.3, 2.4). This does not require the execution of any Java Virtual Machine code; explicit initializers for static fields are executed as part of initialization (5.5), not preparation.

During preparation of a class or interface C, the Java Virtual Machine also imposes loading constraints (5.3.4):

  1. Let L1 be the defining loader of C. For each instance method m declared in C that can override (5.4.5) an instance method declared in a superclass or superinterface <D, L2>, the Java Virtual Machine imposes loading constraints as follows for each class or interface name N mentioned by the descriptor of m (4.3.3), the Java Virtual Machine imposes the loading constraint NL1 = NL2.

    Given that the return type of m is Tr, and that the formal parameter types of m are Tf1, ..., Tfn:

    If Tr not an array type, let T0 be Tr; otherwise, let T0 be the element type of Tr.

    For i = 1 to n: If Tfi is not an array type, let Ti be Tfi; otherwise, let Ti be the element type of Tfi.

    Then TiL1 = TiL2 for i = 0 to n.

  2. For each instance method m declared in a superinterface <I, L3> of C, if C does not itself declare an instance method that can override m, then a method is selected (5.4.6) with respect to C and the method m in <I, L3>. Let <D, L2> be the class or interface that declares the selected method. The Java Virtual Machine imposes loading constraints as follows. For each class or interface name N mentioned by the descriptor of m, the Java Virtual Machine imposes the loading constraint NL2 = NL3.

    Given that the return type of m is Tr, and that the formal parameter types of m are Tf1, ..., Tfn:

    If Tr not an array type, let T0 be Tr; otherwise, let T0 be the element type of Tr.

    For i = 1 to n: If Tfi is not an array type, let Ti be Tfi; otherwise, let Ti be the element type of Tfi.

    Then TiL2 = TiL3 for i = 0 to n.

Preparation may occur at any time following creation but must be completed prior to initialization.

5.4.3 Resolution

5.4.3.2 Field Resolution

To resolve an unresolved symbolic reference from D to a field in a class or interface C, the symbolic reference to C given by the field reference must first be resolved (5.4.3.1). Therefore, any exception that can be thrown as a result of failure of resolution of a class or interface reference can be thrown as a result of failure of field resolution. If the reference to C can be successfully resolved, an exception relating to the failure of resolution of the field reference itself can be thrown.

When resolving a field reference, field resolution first attempts to look up the referenced field in C and its superclasses:

  1. If C declares a field with the name and descriptor specified by the field reference, field lookup succeeds. The declared field is the result of the field lookup.

  2. Otherwise, field lookup is applied recursively to the direct superinterfaces of the specified class or interface C.

  3. Otherwise, if C has a superclass S, field lookup is applied recursively to S.

  4. Otherwise, field lookup fails.

Then, the result of field resolution is determined:

5.4.3.3 Method Resolution

To resolve an unresolved symbolic reference from D to a method in a class C, the symbolic reference to C given by the method reference is first resolved (5.4.3.1). Therefore, any exception that can be thrown as a result of failure of resolution of a class reference can be thrown as a result of failure of method resolution. If the reference to C can be successfully resolved, exceptions relating to the resolution of the method reference itself can be thrown.

When resolving a method reference:

  1. If C is an interface, method resolution throws an IncompatibleClassChangeError.

  2. Otherwise, method resolution attempts to locate the referenced method in C and its superclasses:

    • If C declares exactly one method with the name specified by the method reference, and the declaration is a signature polymorphic method (2.9.3), then method lookup succeeds. All the class names mentioned in the descriptor are resolved (5.4.3.1). The descriptor specified by the method reference is resolved, as if by resolution of an unresolved symbolic reference to a method type (5.4.3.5).

      The resolved method is the signature polymorphic method declaration. It is not necessary for C to declare a method with the descriptor specified by the method reference.

    • Otherwise, if C declares a method with the name and descriptor specified by the method reference, method lookup succeeds.

    • Otherwise, if C has a superclass, step 2 of method resolution is recursively invoked on the direct superclass of C.

  3. Otherwise, method resolution attempts to locate the referenced method in the superinterfaces of the specified class C:

    • If the maximally-specific superinterface methods of C for the name and descriptor specified by the method reference include exactly one method that does not have its ACC_ABSTRACT flag set, then this method is chosen and method lookup succeeds.

    • Otherwise, if any superinterface of C declares a method with the name and descriptor specified by the method reference that has neither its ACC_PRIVATE flag nor its ACC_STATIC flag set, one of these is arbitrarily chosen and method lookup succeeds.

    • Otherwise, method lookup fails.

A maximally-specific superinterface method of a class or interface C for a particular method name and descriptor is any method for which all of the following are true:

The result of method resolution is determined as follows:

When resolution searches for a method in the class's superinterfaces, the best outcome is to identify a maximally-specific non-abstract method. It is possible that this method will be chosen by method selection, so it is desirable to add class loader constraints for it.

Otherwise, the result is nondeterministic. This is not new: The Java® Virtual Machine Specification has never identified exactly which method is chosen, and how "ties" should be broken. Prior to Java SE 8, this was mostly an unobservable distinction. However, beginning with Java SE 8, the set of interface methods is more heterogenous, so care must be taken to avoid problems with nondeterministic behavior. Thus:

Note that if the result of resolution is an abstract method, the referenced class C may be non-abstract. Requiring C to be abstract would conflict with the nondeterministic choice of superinterface methods. Instead, resolution assumes that the run time class of the invoked object has a concrete implementation of the method.

5.4.3.4 Interface Method Resolution

To resolve an unresolved symbolic reference from D to an interface method in an interface C, the symbolic reference to C given by the interface method reference is first resolved (5.4.3.1). Therefore, any exception that can be thrown as a result of failure of resolution of an interface reference can be thrown as a result of failure of interface method resolution. If the reference to C can be successfully resolved, exceptions relating to the resolution of the interface method reference itself can be thrown.

When resolving an interface method reference:

  1. If C is not an interface, interface method resolution throws an IncompatibleClassChangeError.

  2. Otherwise, if C declares a method with the name and descriptor specified by the interface method reference, method lookup succeeds.

  3. Otherwise, if the class Object declares a method with the name and descriptor specified by the interface method reference, which has its ACC_PUBLIC flag set and does not have its ACC_STATIC flag set, method lookup succeeds.

  4. Otherwise, if the maximally-specific superinterface methods (5.4.3.3) of C for the name and descriptor specified by the method reference include exactly one method that does not have its ACC_ABSTRACT flag set, then this method is chosen and method lookup succeeds.

  5. Otherwise, if any superinterface of C declares a method with the name and descriptor specified by the method reference that has neither its ACC_PRIVATE flag nor its ACC_STATIC flag set, one of these is arbitrarily chosen and method lookup succeeds.

  6. Otherwise, method lookup fails.

The result of interface method resolution is determined as follows:

Access control is necessary because interface method resolution may pick a private method of interface C. (Prior to Java SE 8, the result of interface method resolution could be a non-public method of class Object or a static method of class Object; such results were not consistent with the inheritance model of the Java programming language, and are disallowed in Java SE 8 and above.)

5.4.3.5 Method Type and Method Handle Resolution

To resolve an unresolved symbolic reference to a method type, it is as if resolution occurs of unresolved symbolic references to classes and interfaces (5.4.3.1) whose names correspond to the types given in are mentioned by the method descriptor (4.3.3), in the order in which they are mentioned.

Any exception that can be thrown as a result of failure of resolution of a class reference to a class or interface can thus be thrown as a result of failure of method type resolution.

The result of successful method type resolution is a reference to an instance of java.lang.invoke.MethodType which represents the method descriptor.

Method type resolution occurs regardless of whether the run-time constant pool actually contains symbolic references to classes and interfaces indicated in the method descriptor. Also, the resolution is deemed to occur on unresolved symbolic references, so a failure to resolve one method type will not necessarily lead to a later failure to resolve another method type with the same textual method descriptor, if suitable classes and interfaces can be loaded by the later time.

Resolution of an unresolved symbolic reference to a method handle is more complicated. Each method handle resolved by the Java Virtual Machine has an equivalent instruction sequence called its bytecode behavior, indicated by the method handle's kind. The integer values and descriptions of the nine kinds of method handle are given in Table 5.4.3.5-A.

Symbolic references by an instruction sequence to fields or methods are indicated by C.x:T, where x and T are the name and descriptor (4.3.2, 4.3.3) of the field or method, and C is the class or interface in which the field or method is to be found.

Table 5.4.3.5-A. Bytecode Behaviors for Method Handles

Kind Description Interpretation
1 REF_getField getfield C.f:T
2 REF_getStatic getstatic C.f:T
3 REF_putField putfield C.f:T
4 REF_putStatic putstatic C.f:T
5 REF_invokeVirtual invokevirtual C.m:(A*)T
6 REF_invokeStatic invokestatic C.m:(A*)T
7 REF_invokeSpecial invokespecial C.m:(A*)T
8 REF_newInvokeSpecial new C; dup; invokespecial C.<init>:(A*)V
9 REF_invokeInterface invokeinterface C.m:(A*)T

Let MH be the symbolic reference to a method handle (5.1) being resolved. Also:

To resolve MH, all symbolic references to classes, interfaces, fields, and methods in MH's bytecode behavior are resolved, using the following four steps:

  1. R is resolved. This occurs as if by field resolution (5.4.3.2) when MH's bytecode behavior is kind 1, 2, 3, or 4, and as if by method resolution (5.4.3.3) when MH's bytecode behavior is kind 5, 6, 7, or 8, and as if by interface method resolution (5.4.3.4) when MH's bytecode behavior is kind 9.

  2. The following constraints apply to the result of resolving R. These constraints correspond to those that would be enforced during verification or execution of the instruction sequence for the relevant bytecode behavior.

    • If MH's bytecode behavior is kind 8 (REF_newInvokeSpecial), then R must resolve to an instance initialization method declared in class C.

    • If R resolves to a protected member, then the following rules apply depending on the kind of MH's bytecode behavior:

      • For kinds 1, 3, and 5 (REF_getField, REF_putField, and REF_invokeVirtual): If C.f or C.m resolved to a protected field or method, and C is in a different run-time package than the current class, then C must be assignable to the current class.

      • For kind 8 (REF_newInvokeSpecial): If C . <init> resolved to a protected method, then C must be declared in the same run-time package as the current class.

    • R must resolve to a static or non-static member depending on the kind of MH's bytecode behavior:

      • For kinds 1, 3, 5, 7, and 9 (REF_getField, REF_putField, REF_invokeVirtual, REF_invokeSpecial, and REF_invokeInterface): C.f or C.m must resolve to a non-static field or method.

      • For kinds 2, 4, and 6 (REF_getStatic, REF_putStatic, and REF_invokeStatic): C.f or C.m must resolve to a static field or method.

  3. Resolution occurs as if of unresolved symbolic references to classes and interfaces whose names correspond to each type in A* , and to the type T, in that order.

    This is phrased incorrectly—not all types correspond to class and interface names. It's also unnecessary: the next step will perform MethodType resolution which, as described above, resolves all the mentioned classes and interfaces.

  4. A reference to an instance of java.lang.invoke.MethodType is obtained as if by resolution of an unresolved symbolic reference to a method type that contains the method descriptor specified in Table 5.4.3.5-B for the kind of MH.

    It is as if the symbolic reference to a method handle contains a symbolic reference to the method type that the resolved method handle will eventually have. The detailed structure of the method type is obtained by inspecting Table 5.4.3.5-B.

    Table 5.4.3.5-B. Method Descriptors for Method Handles

    Kind Description Method descriptor
    1 REF_getField (C)T
    2 REF_getStatic ()T
    3 REF_putField (C,T)V
    4 REF_putStatic (T)V
    5 REF_invokeVirtual (C,A*)T
    6 REF_invokeStatic (A*)T
    7 REF_invokeSpecial (C,A*)T
    8 REF_newInvokeSpecial (A*)C
    9 REF_invokeInterface (C,A*)T

In steps 1, 3, and 4 1 and 3, any exception that can be thrown as a result of failure of resolution of a symbolic reference to a class, interface, field, or method can be thrown as a result of failure of method handle resolution. In step 2, any failure due to the specified constraints causes a failure of method handle resolution due to an IllegalAccessError.

The intent is that resolving a method handle can be done in exactly the same circumstances that the Java Virtual Machine would successfully verify and resolve the symbolic references in the bytecode behavior. In particular, method handles to private, protected, and static members can be created in exactly those classes for which the corresponding normal accesses are legal.

The result of successful method handle resolution is a reference to an instance of java.lang.invoke.MethodHandle which represents the method handle MH.

The type descriptor of this java.lang.invoke.MethodHandle instance is the java.lang.invoke.MethodType instance produced in the third step of method handle resolution above.

The type descriptor of a method handle is such that a valid call to invokeExact in java.lang.invoke.MethodHandle on the method handle has exactly the same stack effects as the bytecode behavior. Calling this method handle on a valid set of arguments has exactly the same effect and returns the same result (if any) as the corresponding bytecode behavior.

If the method referenced by R has the ACC_VARARGS flag set (4.6), then the java.lang.invoke.MethodHandle instance is a variable arity method handle; otherwise, it is a fixed arity method handle.

A variable arity method handle performs argument list boxing (JLS §15.12.4.2) when invoked via invoke, while its behavior with respect to invokeExact is as if the ACC_VARARGS flag were not set.

Method handle resolution throws an IncompatibleClassChangeError if the method referenced by R has the ACC_VARARGS flag set and either A* is an empty sequence or the last parameter type in A* is not an array type. That is, creation of a variable arity method handle fails.

An implementation of the Java Virtual Machine is not required to intern method types or method handles. That is, two distinct symbolic references to method types or method handles which are structurally identical might not resolve to the same instance of java.lang.invoke.MethodType or java.lang.invoke.MethodHandle respectively.

The java.lang.invoke.MethodHandles class in the Java SE Platform API allows creation of method handles with no bytecode behavior. Their behavior is defined by the method of java.lang.invoke.MethodHandles that creates them. For example, a method handle may, when invoked, first apply transformations to its argument values, then supply the transformed values to the invocation of another method handle, then apply a transformation to the value returned from that invocation, then return the transformed value as its own result.

5.5 Initialization

Initialization of a class or interface consists of executing its class or interface initialization method (2.9.2).

A class or interface C may be initialized only as a result of:

Prior to initialization, a class or interface must be linked, that is, verified, prepared, and optionally resolved.

Because the Java Virtual Machine is multithreaded, initialization of a class or interface requires careful synchronization, since some other thread may be trying to initialize the same class or interface at the same time. There is also the possibility that initialization of a class or interface may be requested recursively as part of the initialization of that class or interface. The implementation of the Java Virtual Machine is responsible for taking care of synchronization and recursive initialization by using the following procedure. It assumes that the Class object class or interface has already been verified and prepared, and that the Class object class or interface contains state that indicates one of four situations:

Here and below, we eliminate the unnecessary assertion that the initialization state of the class is stored by an instance of java.lang.Class. The specification need not concern itself with how classes are internally represented and how this representation relates to instances of java.lang.Class.

For each class or interface C, there is a unique initialization lock LC. The mapping from C to LC is left to the discretion of the Java Virtual Machine implementation. For example, LC could be the Class object for C, or the monitor associated with that Class object. The procedure for initializing C is then as follows:

  1. Synchronize on the initialization lock, LC, for C. This involves waiting until the current thread can acquire LC.

  2. If the Class object for C indicates that initialization is in progress for C by some other thread, then release LC and block the current thread until informed that the in-progress initialization has completed, at which time repeat this procedure.

    Thread interrupt status is unaffected by execution of the initialization procedure.

  3. If the Class object for C indicates that initialization is in progress for C by the current thread, then this must be a recursive request for initialization. Release LC and complete normally.

  4. If the Class object for C indicates that C it has already been initialized, then no further action is required. Release LC and complete normally.

  5. If the Class object for C is in an erroneous state, then initialization is not possible. Release LC and throw a NoClassDefFoundError.

  6. Otherwise, record the fact that initialization of the Class object for C is in progress by the current thread, and release LC.

    Then, initialize each final static field of C with the constant value in its ConstantValue attribute (4.7.2), in the order the fields appear in the ClassFile structure.

  7. Next, if C is a class rather than an interface, then let SC be its superclass and let SI1, ..., SIn be all superinterfaces of C (whether direct or indirect) that declare at least one non-abstract, non-static method. The order of superinterfaces is given by a recursive enumeration over the superinterface hierarchy of each interface directly implemented by C. For each interface I directly implemented by C (in the order of the interfaces array of C), the enumeration recurs on I's superinterfaces (in the order of the interfaces array of I) before returning I.

    For each S in the list [ SC, SI1, ..., SIn ], if S has not yet been initialized, then recursively perform this entire procedure for S. If necessary, verify and prepare S first.

    If the initialization of S completes abruptly because of a thrown exception, then acquire LC, label the Class object for C as erroneous, notify all waiting threads, release LC, and complete abruptly, throwing the same exception that resulted from initializing SC S.

  8. Next, determine whether assertions are enabled for C by querying its defining class loader.

  9. Next, execute the class or interface initialization method of C.

  10. If the execution of the class or interface initialization method completes normally, then acquire LC, label the Class object for C as fully initialized, notify all waiting threads, release LC, and complete this procedure normally.

  11. Otherwise, the class or interface initialization method must have completed abruptly by throwing some exception E. If the class of E is not Error or one of its subclasses, then create a new instance of the class ExceptionInInitializerError with E as the argument, and use this object in place of E in the following step. If a new instance of ExceptionInInitializerError cannot be created because an OutOfMemoryError occurs, then use an OutOfMemoryError object in place of E in the following step.

  12. Acquire LC, label the Class object for C as erroneous, notify all waiting threads, release LC, and complete this procedure abruptly with reason E or its replacement as determined in the previous step.

A Java Virtual Machine implementation may optimize this procedure by eliding the lock acquisition in step 1 (and release in step 4/5) when it can determine that the initialization of the class has already completed, provided that, in terms of the Java memory model, all happens-before orderings (JLS §17.4.5) that would exist if the lock were acquired, still exist when the optimization is performed.

Chapter 6: The Java Virtual Machine Instruction Set

6.5 Instructions

aastore

Operation

Store into reference array

Format

aastore

Forms

aastore = 83 (0x53)

Operand Stack

..., arrayref, index, value

...

Description

The arrayref must be of type reference and must refer to an array whose components are of type reference. The index must be of type int, and value must be of type reference. The arrayref, index, and value are popped from the operand stack.

If value is null, then value is stored as the component of the array at index.

Otherwise, value is non-null. If the type of value is assignment compatible with the type of the components of the array referenced by arrayref, then value is stored as the component of the array at index. If value is a value of the component type of the array referenced by arrayref, then value is stored as the component of the array at index.

The following rules are used to determine whether a value that is not null is assignment compatible with the array component type. If S is the type of the object referred to by value, and T is the reference type of the array components, then aastore determines whether assignment is compatible as follows:

  • If S is a class type, then:

    • If T is a class type, then S must be the same class as T, or S must be a subclass of T;

    • If T is an interface type, then S must implement interface T.

  • If S is an array type SC[], that is, an array of components of type SC, then:

    • If T is a class type, then T must be Object.

    • If T is an interface type, then T must be one of the interfaces implemented by arrays (JLS §4.10.3).

    • If T is an array type TC[], that is, an array of components of type TC, then one of the following must be true:

      • TC and SC are the same primitive type.

      • TC and SC are reference types, and type SC is assignable to TC by these run-time rules.

Whether value is a value of the array component type is determined according to the rules given for checkcast.

Appealing to "assignment compatible" is a roundabout way to say what we really mean—value must be a value of the array's component type.

aastore, checkcast, and instanceof use the same rules to interpret types. It's helpful to consolidate those rules in one place, so that readers can clearly see that the rules are the same, and so that future enhancements to the type system have fewer rules to maintain.

Run-time Exceptions

If arrayref is null, aastore throws a NullPointerException.

Otherwise, if index is not within the bounds of the array referenced by arrayref, the aastore instruction throws an ArrayIndexOutOfBoundsException.

Otherwise, if arrayref is not null and the actual type of the non-null value is not assignment compatible with the actual type of the components of the array a value of the array component type, aastore throws an ArrayStoreException.

"Otherwise" here implies "arrayref is not null".

checkcast

Operation

Check whether object is of given type

Format

checkcast
indexbyte1
indexbyte2

Forms

checkcast = 192 (0xc0)

Operand Stack

..., objectref

..., objectref

Description

The objectref must be of type reference. The unsigned indexbyte1 and indexbyte2 are used to construct an index into the run-time constant pool of the current class (2.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The run-time constant pool entry at the index must be a symbolic reference to a class, array, or interface type.

If objectref is null, then the operand stack is unchanged.

Otherwise, the named class, array, or interface type is resolved (5.4.3.1). If objectref can be cast to the resolved class, array, or interface type is a value of the type given by the resolved class, interface, or array type, the operand stack is unchanged; otherwise, the checkcast instruction throws a ClassCastException.

The following rules are used to determine whether an objectref that is not null can be cast to the resolved type a reference to an object is a value of a reference type, T. If S is the type of the object referred to by objectref, and T is the resolved class, array, or interface type, then checkcast determines whether objectref can be cast to type T as follows:

  • If S is a class type the reference is to an instance of a class C, then:

    • If T is a class type, then S must be the same class as T, or S must be a subclass of T;

      If T is the type of a class D, then the reference is a value of T if C is D or a subclass of D.

    • If T is an interface type, then S must implement interface T.

      If T is the type of an interface I, then the reference is a value of T if C implements I.

  • If S is an array type SC[], that is, an array of components of type SC the reference is to an array with component type SC, then:

    • If T is a class type, then T must be Object the reference is a value of T if T is Object.

    • If T is an interface type, then T must be one of the interfaces implemented by arrays (JLS §4.10.3) the reference is a value of T if T is Cloneable or java.io.Serializable (as loaded by the bootstrap class loader).

      It's unnecessary and especially risky to tie JVMS to the Java Language Specification here—we certainly don't want language changes to accidentally impact the routine behavior of JVM instructions.

    • If T is an array type TC[], that is, an array of components of type TC, then one of the following must be true the reference is a value of T if one of the following are true:

      • TC and SC are the same primitive type.

      • TC and SC are reference types, and type SC can be cast to TC by recursive application of these rules.

        Bug fix: an earlier cleanup of these rules (JDK-8069130) removed cases to handle an interface type S. These cases appeared vacuous at the top level, but were necessary to support a recursive analysis for array types. Rather than restoring the old rules, it's probably easier to follow if the recursion is contained within the array type discussion.

        Further, recursion to the top level is no longer a good fit, because the rules are expressed in terms of a specific reference, not types.

      • TC is the class type Object.

      • TC is a class type, SC is a class type, and the class of SC is a subclass of the class of TC.

      • TC is an interface type, SC is a class type, and the class of SC implements the interface of TC.

      • TC is an interface type, SC is an interface type, and the interface of SC extends the interface of TC.

      • TC is the interface type Cloneable or java.io.Serializable (as loaded by the bootstrap class loader), and SC is an array type.

      • TC is an array type TCC[], SC is an array type SCC[], and one of these tests of array component types apply recursively to TCC and SCC.

Linking Exceptions

During resolution of the symbolic reference to the class, array, or interface type, any of the exceptions documented in 5.4.3.1 can be thrown.

Run-time Exception

Otherwise, if objectref cannot be cast to the resolved class, array, or interface type is not null and is not a value of the type given by the resolved class, interface, or array type, the checkcast instruction throws a ClassCastException.

Notes

The checkcast instruction is very similar to the instanceof instruction (6.5.instanceof). It differs in its treatment of null, its behavior when its test fails (checkcast throws an exception, instanceof pushes a result code), and its effect on the operand stack.

instanceof

Operation

Determine if object is of given type

Format

instanceof
indexbyte1
indexbyte2

Forms

instanceof = 193 (0xc1)

Operand Stack

..., objectref

..., result

Description

The objectref, which must be of type reference, is popped from the operand stack. The unsigned indexbyte1 and indexbyte2 are used to construct an index into the run-time constant pool of the current class (2.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The run-time constant pool entry at the index must be a symbolic reference to a class, array, or interface type.

If objectref is null, the instanceof instruction pushes an int result of 0 as an int onto the operand stack.

Otherwise, the named class, array, or interface type is resolved (5.4.3.1). If objectref is an instance of a value of the type given by the resolved class, interface, or array type, or implements the resolved interface, the instanceof instruction pushes an int result of 1 as an int onto the operand stack; otherwise, it pushes an int result of 0.

The following rules are used to determine whether an objectref that is not null is an instance of the resolved type. If S is the type of the object referred to by objectref, and T is the resolved class, array, or interface type, then instanceof determines whether objectref is an instance of T as follows:

  • If S is a class type, then:

    • If T is a class type, then S must be the same class as T, or S must be a subclass of T;

    • If T is an interface type, then S must implement interface T.

  • If S is an array type SC[], that is, an array of components of type SC, then:

    • If T is a class type, then T must be Object.

    • If T is an interface type, then T must be one of the interfaces implemented by arrays (JLS §4.10.3).

    • If T is an array type TC[], that is, an array of components of type TC, then one of the following must be true:

      • TC and SC are the same primitive type.

      • TC and SC are reference types, and type SC can be cast to TC by these run-time rules.

Whether objectref is a value of the type given by the resolved class, interface, or array type is determined according to the rules given for checkcast.

aastore, checkcast, and instanceof use the same rules to interpret types. It's helpful to consolidate those rules in one place, so that readers can clearly see that the rules are the same, and so that future enhancements to the type system have fewer rules to maintain.

Linking Exceptions

During resolution of the symbolic reference to the class, array, or interface type, any of the exceptions documented in 5.4.3.1 can be thrown.

Notes

The instanceof instruction is very similar to the checkcast instruction (6.5.checkcast). It differs in its treatment of null, its behavior when its test fails (checkcast throws an exception, instanceof pushes a result code), and its effect on the operand stack.

new

Operation

Create new object

Format

new
indexbyte1
indexbyte2

Forms

new = 187 (0xbb)

Operand Stack

...

..., objectref

Description

The unsigned indexbyte1 and indexbyte2 are used to construct an index into the run-time constant pool of the current class (2.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The run-time constant pool entry at the index must be a symbolic reference to a class or interface type. The named class or interface type is resolved (5.4.3.1) and should result in a non-abstract class type. Memory for a new instance of that class is allocated from the garbage-collected heap, and the instance variables of the new object are initialized to their the default initial values of their types (2.3, 2.4). The objectref, a reference to the instance, is pushed onto the operand stack.

On successful resolution of the class, it is initialized if it has not already been initialized (5.5).

Linking Exceptions

During resolution of the symbolic reference to the class or interface type, any of the exceptions documented in 5.4.3.1 can be thrown.

Otherwise, if the symbolic reference to the class or interface type resolves to an interface or an abstract class, new throws an InstantiationError.

Run-time Exception

Otherwise, if execution of this new instruction causes initialization of the referenced class, new may throw an Error as detailed in JLS §15.9.4 5.5.

This is an unnecessary JLS reference, and also appears to be out of date: JLS 15.9.4 doesn't describe class initialization at all.

Notes

The new instruction does not completely create a new instance; instance creation is not completed until an instance initialization method (2.9.1) has been invoked on the uninitialized instance.

putfield

Operation

Set field in object

Format

putfield
indexbyte1
indexbyte2

Forms

putfield = 181 (0xb5)

Operand Stack

..., objectref, value

...

Description

The unsigned indexbyte1 and indexbyte2 are used to construct an index into the run-time constant pool of the current class (2.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The run-time constant pool entry at the index must be a symbolic reference to a field (5.1), which gives the name and descriptor of the field as well as a symbolic reference to the class in which the field is to be found. The referenced field is resolved (5.4.3.2).

The type of a value stored by a putfield instruction must be compatible with the descriptor of the referenced field (4.3.2). If the field descriptor type is boolean, byte, char, short, or int, then the value must be an int. If the field descriptor type is float, long, or double, then the value must be a float, long, or double, respectively. If the field descriptor type is a reference type, then the value must be a value of a type that is assignment compatible (JLS §5.2) with the field descriptor type. If the field is final, it must be declared in the current class, and the instruction must occur in an instance initialization method of the current class (2.9.1).

The value and objectref are popped from the operand stack.

The objectref must be of type reference but not an array type.

If the value is of type int and the field descriptor type is boolean, then the int value is narrowed by taking the bitwise AND of value and 1, resulting in value'. Otherwise, the value undergoes value set conversion (2.8.3), resulting in value'.

The referenced field in objectref is set to value'.

Linking Exceptions

During resolution of the symbolic reference to the field, any of the exceptions pertaining to field resolution (5.4.3.2) can be thrown.

Otherwise, if the resolved field is a static field, putfield throws an IncompatibleClassChangeError.

Otherwise, if the resolved field is final, it must be declared in the current class, and the instruction must occur in an instance initialization method of the current class. Otherwise, an IllegalAccessError is thrown.

Run-time Exception

Otherwise, if objectref is null, the putfield instruction throws a NullPointerException.

putstatic

Operation

Set static field in class

Format

putstatic
indexbyte1
indexbyte2

Forms

putstatic = 179 (0xb3)

Operand Stack

..., value

...

Description

The unsigned indexbyte1 and indexbyte2 are used to construct an index into the run-time constant pool of the current class (2.6), where the value of the index is (indexbyte1 << 8) | indexbyte2. The run-time constant pool entry at the index must be a symbolic reference to a field (5.1), which gives the name and descriptor of the field as well as a symbolic reference to the class or interface in which the field is to be found. The referenced field is resolved (5.4.3.2).

On successful resolution of the field, the class or interface that declared the resolved field is initialized if that class or interface has not already been initialized (5.5).

The type of a value stored by a putstatic instruction must be compatible with the descriptor of the referenced field (4.3.2). If the field descriptor type is boolean, byte, char, short, or int, then the value must be an int. If the field descriptor type is float, long, or double, then the value must be a float, long, or double, respectively. If the field descriptor type is a reference type, then the value must be a value of a type that is assignment compatible (JLS §5.2) with the field descriptor type. If the field is final, it must be declared in the current class or interface, and the instruction must occur in the class or interface initialization method of the current class or interface (2.9.2).

The value is popped from the operand stack.

If the value is of type int and the field descriptor type is boolean, then the int value is narrowed by taking the bitwise AND of value and 1, resulting in value'. Otherwise, the value undergoes value set conversion (2.8.3), resulting in value'.

The referenced field in the class or interface is set to value'.

Linking Exceptions

During resolution of the symbolic reference to the class or interface field, any of the exceptions pertaining to field resolution (5.4.3.2) can be thrown.

Otherwise, if the resolved field is not a static (class) field or an interface field, putstatic throws an IncompatibleClassChangeError.

Otherwise, if the resolved field is final, it must be declared in the current class or interface, and the instruction must occur in the class or interface initialization method of the current class or interface. Otherwise, an IllegalAccessError is thrown.

Run-time Exception

Otherwise, if execution of this putstatic instruction causes initialization of the referenced class or interface, putstatic may throw an Error as detailed in 5.5.

Notes

A putstatic instruction may be used only to set the value of an interface field on the initialization of that field. Interface fields may be assigned to only once, on execution of an interface variable initialization expression when the interface is initialized (5.5, JLS §9.3.1).