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

Verification Cleanup

Changes to the Java® Virtual Machine Specification • Version 20-internal-adhoc.dlsmith.20220830

This document describes changes to the Java Virtual Machine Specification, as modified by Format Checking Cleanup, to clarify the process of validating the Code and StackMapTable attributes, and to address problems in the rules for bytecode verification.

The following changes to implementation behavior are proposed:

In addition, redundant verification rules for checking final classes and methods are eliminated, and the specification of various validation checks for Code and StackMapTable attributes is shifted to verification time (4.9, 4.10), consistent with longstanding behavior of the reference implementation. Verification rules better distinguish between class/interface types and loaded classes. Bugs in the subtyping rules, instruction encodings, and usage of interface methods (JDK-8122946) are addressed.

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 4: The class File Format

4.7 Attributes

4.7.3 The Code Attribute

The Code attribute is a variable-length attribute in the attributes table of a method_info structure (4.6). A Code attribute contains the Java Virtual Machine instructions and auxiliary information for a method, including an instance initialization method and a class or interface initialization method (2.9.1, 2.9.2).

If the method is either native or abstract, and is not a class or interface initialization method, then its method_info structure must not have a Code attribute in its attributes table. Otherwise, its method_info structure must have exactly one Code attribute in its attributes table.

The Code attribute has must have the following format:

Code_attribute {
    u2 attribute_name_index;
    u4 attribute_length;
    u2 max_stack;
    u2 max_locals;
    u4 code_length;
    u1 code[code_length];
    u2 exception_table_length;
    {   u2 start_pc;
        u2 end_pc;
        u2 handler_pc;
        u2 catch_type;
    } exception_table[exception_table_length];
    u2 attributes_count;
    attribute_info attributes[attributes_count];
}

The items of the Code_attribute structure are as follows:

attribute_name_index

The value of the attribute_name_index item must be a valid is an index into the constant_pool table. The constant_pool entry at that index must be is a CONSTANT_Utf8_info structure (4.4.7) representing the string "Code".

attribute_length

The value of the attribute_length item indicates the length of the attribute, excluding the initial six bytes.

max_stack

The value of the max_stack item gives the maximum depth of the operand stack of this method (2.6.2) at any point during execution of the method.

max_locals

The value of the max_locals item gives the number of local variables in the local variable array allocated upon invocation of this method (2.6.1), including the local variables used to pass parameters to the method on its invocation.

The greatest local variable index for a value of type long or double is max_locals - 2. The greatest local variable index for a value of any other type is max_locals - 1.

code_length

The value of the code_length item gives the number of bytes in the code array for this method.

The value of code_length must be greater than zero (as the code array must not be empty) and less than 65536.

code[]

The code array gives the actual bytes of Java Virtual Machine code that implement the method.

When the code array is read into memory on a byte-addressable machine, if the first byte of the array is aligned on a 4-byte boundary, the tableswitch and lookupswitch 32-bit offsets will be 4-byte aligned. (Refer to the descriptions of those instructions for more information on the consequences of code array alignment.)

The detailed constraints on the contents of the code array are extensive and are given in a separate section (4.9).

The contents of the code array are subject to extensive constraints during verification (5.4.1), as described in 4.9.

exception_table_length

The value of the exception_table_length item gives the number of entries in the exception_table array.

exception_table[]

Each entry in the exception_table array describes one exception handler in the code array. The order of the handlers in the exception_table array is significant (2.10).

The contents of the exception_table array are validated during verification, along with the code array.

Each exception_table entry contains the following four items:

start_pc, end_pc

The values of the two items start_pc and end_pc indicate the ranges in the code array at which the exception handler is active. The value of start_pc must should be a valid index into the code array of the opcode of an instruction. The value of end_pc either must should be a valid index into the code array of the opcode of an instruction or must should be equal to code_length, the length of the code array. The value of start_pc must should be less than the value of end_pc.

The start_pc is inclusive and end_pc is exclusive; that is, the exception handler must will be active while the program counter is within the interval [start_pc, end_pc).

The fact that end_pc is exclusive is a historical mistake in the design of the Java Virtual Machine: if the Java Virtual Machine code for a method is exactly 65535 bytes long and ends with an instruction that is 1 byte long, then that instruction cannot be protected by an exception handler. A compiler writer can work around this bug by limiting the maximum size of the generated Java Virtual Machine code for any method, instance initialization method, or static initializer (the size of any code array) to 65534 bytes.

handler_pc

The value of the handler_pc item indicates the start of the exception handler. The value of the item must should be a valid index into the code array and must should be the index of the opcode of an instruction.

catch_type

If the value of the catch_type item is nonzero, it must should be a valid index into the constant_pool table. The constant_pool entry at that index must should be a CONSTANT_Class_info structure (4.4.1) representing a class of exceptions that this exception handler is designated to catch. The exception handler will be called only if the thrown exception is an instance of the given class or one of its subclasses.

The verifier checks that the class is Throwable or a subclass of Throwable (4.9.2).

If the value of the catch_type item is zero, this exception handler is called for all exceptions.

This is used to implement finally (3.13).

In JDK 16, some of these assertions are checked during format checking, but assertions about opcode indices are delayed until verification. For simplicity, it makes more sense to perform all checks on the exception table during verification (see 4.9.1).

attributes_count

The value of the attributes_count item indicates the number of attributes of the Code attribute.

attributes[]

Each value of the attributes table must be an attribute_info structure (4.7).

A Code attribute can have any number of optional attributes associated with it.

A discussion about constraints on attributes is better left to 4.7.

The attributes defined by this specification as appearing in the attributes table of a Code attribute are listed in Table 4.7-C.

The rules concerning attributes defined to appear in the attributes table of a Code attribute are given in 4.7.

The rules concerning non-predefined nonstandard attributes in the attributes table of a Code attribute are given in 4.7.1.

4.7.4 The StackMapTable Attribute

The StackMapTable attribute is a variable-length attribute in the attributes table of a Code attribute (4.7.3) in a version 50.0 or later class file. A StackMapTable attribute is used during the process of verification by type checking (4.10.1).

There may be at most must be no more than one StackMapTable attribute in the attributes table of a Code attribute.

In a class file whose version number is 50.0 or above, if a method's Code attribute does not have a StackMapTable attribute, it has an implicit stack map attribute (4.10.1). This implicit stack map attribute is equivalent to a StackMapTable attribute with number_of_entries equal to zero.

The StackMapTable attribute has should have the following format:

StackMapTable_attribute {
    u2              attribute_name_index;
    u4              attribute_length;
    u2              number_of_entries;
    stack_map_frame entries[number_of_entries];
}

The contents of the StackMapTable attribute are validated during verification, along with the code and exception_table arrays of the Code attribute (4.7.3).

The items of the StackMapTable_attribute structure are as follows:

attribute_name_index

The value of the attribute_name_index item must be a valid is an index into the constant_pool table. The constant_pool entry at that index must be is a CONSTANT_Utf8_info structure (4.4.7) representing the string "StackMapTable".

attribute_length

The value of the attribute_length item indicates the length of the attribute, excluding the initial six bytes.

number_of_entries

The value of the number_of_entries item gives should give the number of stack_map_frame entries in the entries table.

entries[]

Each entry in the entries table describes should describe one stack map frame of the method. The order of the stack map frames in the entries table is significant.

A stack map frame specifies (either explicitly or implicitly) the bytecode offset at which it applies, and the verification types of local variables and operand stack entries for that offset.

Each stack map frame described in the entries table relies on the previous frame for some of its semantics. The first stack map frame of a method is implicit, and computed from the method descriptor by the type checker (4.10.1.6). The stack_map_frame structure at entries[0] therefore describes the second stack map frame of the method.

The bytecode offset at which a stack map frame applies is calculated by taking the value offset_delta specified in the frame (either explicitly or implicitly), and adding offset_delta + 1 to the bytecode offset of the previous frame, unless the previous frame is the initial frame of the method. In that case, the bytecode offset at which the stack map frame applies is the value offset_delta specified in the frame.

By using an offset delta rather than storing the actual bytecode offset, we ensure, by definition, that stack map frames are in the correctly sorted order. Furthermore, by consistently using the formula offset_delta + 1 for all explicit frames (as opposed to the implicit first frame), we guarantee the absence of duplicates.

We say that an instruction in the bytecode has a corresponding stack map frame if the instruction starts at offset i in the code array of a Code attribute, and the Code attribute has a StackMapTable attribute whose entries array contains a stack map frame that applies at bytecode offset i.

A verification type specifies the type of either one or two locations, where a location is either a single local variable or a single operand stack entry. A verification type is represented by a discriminated union, verification_type_info, that consists of a one-byte tag, indicating which item of the union is in use, followed by zero or more bytes, giving more information about the tag.

union verification_type_info {
    Top_variable_info;
    Integer_variable_info;
    Float_variable_info;
    Long_variable_info;
    Double_variable_info;
    Null_variable_info;
    UninitializedThis_variable_info;
    Object_variable_info;
    Uninitialized_variable_info;
}

A verification type that specifies one location in the local variable array or in the operand stack is represented by the following items of the verification_type_info union:

A verification type that specifies two locations in the local variable array or in the operand stack is represented by the following items of the verification_type_info union:

A stack map frame is represented by a discriminated union, stack_map_frame, which consists of a one-byte tag, indicating which item of the union is in use, followed by zero or more bytes, giving more information about the tag.

union stack_map_frame {
    same_frame;
    same_locals_1_stack_item_frame;
    same_locals_1_stack_item_frame_extended;
    chop_frame;
    same_frame_extended;
    append_frame;
    full_frame;
}

The tag indicates the frame type of the stack map frame:

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 and associated StackMapTable_attribute structures.

These constraints are enforced by verification (4.10). A class file may be considered valid ([4]) even if it violates these constraints, but an error will occur before the code can be executed (5.4.1).

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 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, and how exception_table and StackMapTable entries reference the code array and the constant pool.

The deleted sentences unhelpfully blur the distinction between format checking and verification.

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:

The static constraints on the entries in the exception_table array are as follows:

The static constraints on the entries in the the entries table of a StackMapTable attribute (4.7.4) are as follows:

In JDK 16, the constraints on exception_table are enforced both at class loading time and verification time. (Specifically, constraints that require parsing a code array are delayed until verification time.) This specification makes them all verification time checks.

All constraints on StackMapTable are enforced by JDK 16 at verification time, despite previously being specified as format checks (4.7.4).

The Uninitialized_variable_info constraint is treated by JDK 16 as a structural constraint—in version 50.0 class files, an invalid Object_variable_info causes a failure, but an invalid Uninitialized_variable_info can be recovered from by falling back to verification by type inference. There's not a strong argument for this discrepancy, so we propose changing the behavior, making both unrecoverable failures. (This occurs naturally when the checks are treated as static constraints—see 4.10 and 4.10.1 for details.)

4.9.2 Structural Constraints

The structural constraints structural constraints on the code array code in a class file specify constraints on relationships between Java Virtual Machine instructions, exception handlers, and stack maps. The structural constraints are as follows:

4.10 Verification of class Files

In this revision, static constraints (4.9.1) are explicitly checked as a first step of verification, before one of the two verification algorithms are invoked. Assertions related to static constraints can be removed from the typing algorithms.

Even though a compiler for the Java programming language must only produce class files that satisfy all the static and structural constraints in the previous sections of Section 4.9, the Java Virtual Machine has no guarantee that any file it is asked to load was generated by that compiler or is properly formed. Applications such as web browsers do not download source code, which they then compile; these applications download already-compiled class files. The browser needs to determine whether the class file was produced by a trustworthy compiler or by an adversary attempting to exploit the Java Virtual Machine.

For example, applications such as web browsers do not download source code, which they then compile; these applications download already-compiled class files. The browser needs to determine whether the class file was produced by a trustworthy compiler or by an adversary attempting to exploit the Java Virtual Machine.

This example is better treated as non-normative explanatory text.

An additional problem with compile-time checking is version skew. A user may have successfully compiled a class, say PurchaseStockOptions, to be a subclass of TradingClass. But the definition of TradingClass might have changed since the time the class was compiled in a way that is not compatible with pre-existing binaries. Methods might have been deleted or had their return types or modifiers changed. Fields might have changed types or changed from instance variables to class variables. The access modifiers of a method or variable may have changed from public to private. For a discussion of these issues, see Chapter 13, "Binary Compatibility," in The Java Language Specification, Java SE 16 Edition.

This example is not relevant to verification. If we don't want to delete it, perhaps it could be moved to 5.4.3?

Because of these potential problems, the Java Virtual Machine needs to verify for itself that the desired constraints are satisfied by the class files it attempts to incorporate. However, it may cause unwanted delays to check these constraints during format checking (4.8), which occurs as each class is loaded.

A Thus, a Java Virtual Machine implementation verifies that each class file satisfies the necessary constraints on Code attributes (4.7.3) and StackMapTable attributes (4.7.4) at linking time (5.4).

Link-time verification enhances the performance of the run-time interpreter. Expensive checks that would otherwise have to be performed to verify constraints at run time for each interpreted instruction can be eliminated. The Java Virtual Machine can assume that these checks have already been performed. For example, the Java Virtual Machine will already know the following:

Link-time verification enhances the performance of the run-time interpreter. Expensive checks that would otherwise have to be performed to verify constraints at run time for each interpreted instruction can be eliminated. The Java Virtual Machine can assume that these checks have already been performed. For example, the Java Virtual Machine will already know the following:

  • There are no operand stack overflows or underflows.

  • All local variable uses and stores are valid.

  • The arguments to all the Java Virtual Machine instructions are of valid types.

This performance discussion is better treated as non-normative explanatory text.

For each Code attribute in a class file, verification proceeds in two steps.

  1. The code and exception_table arrays are parsed and checked, according to the static constraints described in 4.9.1. If the attributes table contains a StackMapTable attribute, it is also parsed and checked, as described in 4.9.1.

    If any static constraints are violated, verification fails with a VerifyError.

    Historically, this step of verification has been overlooked, implicitly handled by, e.g., assumptions that a Prolog predicate will not succeed if it's impossible to encode an instruction.

    Note that a version 50.0 class file may fail verification due to a static constraint violation in a StackMapTable attribute, even if it would have succeeded verification by type inference if the attribute had been absent. The ability to recover from an error by falling back to verification by type inference is only available in step 2 (see 4.10.1).

  2. The structural constraints described in 4.9.2 are checked.

    There are two strategies that Java Virtual Machine implementations may use for structural constraint verification:

    • Verification by type checking must be used to verify class files whose version number is greater than or equal to 50.0.

    • Verification by type inference must be supported by all Java Virtual Machine implementations, except those conforming to the Java ME CLDC and Java Card profiles, in order to verify class files whose version number is less than 50.0.

      Verification on Java Virtual Machine implementations supporting the Java ME CLDC and Java Card profiles is governed by their respective specifications.

    In either case, if the specified algorithms are unable to prove that all structural constraints hold, verification fails with a VerifyError.

In JDK 16, constraint failures involving the exceptions table or the StackMapTable attribute result in a verification-time ClassFormatError. This behavior is confusing, and we propose throwing a VerifyError instead.

In both strategies, verification is mainly concerned with enforcing the static and structural constraints from 4.9 on the code array of the Code attribute (4.7.3). However, there are three additional checks outside the Code attribute which must be performed during verification:

Checks for subclassing of final classes and overriding of final methods are already specified as part of class derivation (5.3.5), which is where Hotspot and OpenJ9 actually perform the checks, before an instance of java.lang.Class can escape into user code.

As a result, verification is solely concerned with Code attributes. Rules that amount to a search for Code attributes can be deleted, including section 4.10.1.5.

4.10.1 Verification by Type Checking

A class file whose version number is 50.0 or above (4.1) must be verified verify structural constraints using the type checking rules given in this section.

If, and only if, a class file's version number equals 50.0, then if the type checking fails, a Java Virtual Machine implementation may choose to attempt to perform verification by type inference (4.10.2). In this case, structural constraints on the StackMapTable attribute are not enforced.

This is a pragmatic adjustment, designed to ease the transition to the new verification discipline. Many tools that manipulate class files may alter the bytecodes of a method in a manner that requires adjustment of the method's stack map frames. If a tool does not make the necessary adjustments to the stack map frames, type checking may fail even though the bytecode is in principle valid (and would consequently verify under the old type inference scheme). To allow implementors time to adapt their tools, Java Virtual Machine implementations may fall back to the older verification discipline, but only for a limited time.

In cases where type checking fails but type inference is invoked and succeeds, a certain performance penalty is expected. Such a penalty is unavoidable. It also should serve as a signal to tool vendors that their output needs to be adjusted, and provides vendors with additional incentive to make these adjustments.

In summary, failover to verification by type inference supports both the gradual addition of stack map frames to the Java SE Platform (if they are not present in a version 50.0 class file, failover is allowed) and the gradual removal of the jsr and jsr_w instructions from the Java SE Platform (if they are present in a version 50.0 class file, failover is allowed).

If a Java Virtual Machine implementation ever attempts to perform verification by type inference on version 50.0 class files, it must do so in all cases where verification by type checking fails.

This means that a Java Virtual Machine implementation cannot choose to resort to type inference in once case and not in another. It must either reject class files that do not verify via type checking, or else consistently failover to the type inferencing verifier whenever type checking fails.

The type checker enforces type rules that are specified by means of Prolog clauses. English language text is used to describe the type rules in an informal way, while the Prolog clauses provide a formal specification.

The type checker requires a list of stack map frames for each method with a Code attribute (4.7.3). A list of stack map frames is given by the StackMapTable attribute (4.7.4) of a Code attribute. The intent is that a stack map frame must appear at the beginning of each basic block in a method. The stack map frame specifies the verification type of each operand stack entry and of each local variable at the start of each basic block. The type checker reads the stack map frames for each method with a Code attribute and uses these maps to generate a proof of the type safety of the instructions in the Code attribute.

A class is type safe if all its methods are type safe, and it does not subclass a final class.

classIsTypeSafe(Class) :-
    classClassName(Class, Name), 
    classDefiningLoader(Class, L),
    superclassChain(Name, L, Chain),
    Chain \= [],
    classSuperClassName(Class, SuperclassName),
    loadedClass(SuperclassName, L, Superclass),
    classIsNotFinal(Superclass),     
    classMethods(Class, Methods), 
    checklist(methodIsTypeSafe(Class), Methods).
classIsTypeSafe(Class) :-
    classClassName(Class, 'java/lang/Object'),
    classDefiningLoader(Class, L),
    isBootstrapLoader(L),
    classMethods(Class, Methods), 
    checklist(methodIsTypeSafe(Class), Methods).

The Prolog predicate classIsTypeSafe assumes that Class is a Prolog term representing a binary class that has been successfully parsed and loaded. This specification does not mandate the precise structure of this term, but does require that certain predicates be defined upon it.

For example, we assume a predicate classMethods(Class, Methods) that, given a term representing a class as described above as its first argument, binds its second argument to a list comprising all the methods of the class, represented in a convenient form described later.

Iff the predicate classIsTypeSafe is not true, the type checker must throw the exception VerifyError to indicate that the class file is malformed. Otherwise, the class file has type checked successfully and bytecode verification has completed successfully.

The Prolog predicate methodIsTypeSafe (4.10.1.6) determines whether the Code attribute of a particular method of a particular class or interface conforms to the structural constraints described in 4.9.2. The structural constraints are satisfied by the method if and only if the methodIsTypeSafe predicate is true.

The rest of this section explains the process of type checking in detail:

4.10.1.1 Accessors for Java Virtual Machine Artifacts

The Prolog term Class represents a binary class or interface that has been successfully loaded (5.3). This specification does not mandate the precise structure of this term.

Similarly, the Prolog term Method represents a method of a Class, and the Prolog term Loader represents a class loader of a Class. We do not specify the structure of the method or class loader.

This expands on the notation discussion that was deleted from 4.10.1.

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

A number of predicates can be removed because they are not used anywhere. (In most cases, this is because section 4.10.1.5 has been deleted.)

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.

Clarifying that, like classSuperClassName, this predicate extracts names, not loaded interfaces.

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.

If a StackMapTable attribute is absent, the implicit stack map attribute is used (4.7.4).

If an entry in the stack map table violates structural constraints (4.9.2) because of an invalid Code array offset, an invalid stack type array size, or an invalid local variable type array size, the parseCodeAttribute predicate fails.

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').

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.

Here, and throughout the verification rules, we use the name java/lang/Object as an unambiguous indication that the class is the Object class. Only the bootstrap loader is allowed to define a class named java/lang/Object (see 5.3.5).

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).

This predicate was previously, unnecessarily, defined in terms of a class type (see below).

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).

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.

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)).

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.

There are a number of technical problems and redundancies in these subtyping rules. These problems are pointed out and addressed below.

As a stylistic move, a number of references to the Java programming language are also removed. The verification type system stands on its own, independent of the Java language.

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).

Rephrased this rule as isAssignable(null, X) :- isAssignable(reference, X), above.

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)) :-
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 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).

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 this rule addresses it.

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

In the case in which two class types have the same name and the same initiating class loader, neither of these rules apply. That's an identity, not a widening; the reflexive isAssignable rule applies (and the class need 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', _)).

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.

Covered by the reflexive isAssignable rule.

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 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:

No change to these items, just rearranging to combine the two lists of constant forms into one. Because CONSTANT_Class_info is relevant to both lists, it's awkward to keep the two lists separate. The example of the int constant 91 was moved to the discussion below.

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.

This isn't workable: int is a legal class name. Anyway, 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.5 Type Checking Abstract and Native Methods

This section purports to enforce the final keyword. But these checks never need to be performed, because they already occur during class derivation (5.3.5).

An empty section is left behind, creating a section renumbering problem. 4.10.1.6 is quite long, and perhaps could be split...

abstract methods and native methods are considered to be type safe if they do not override a final method.

methodIsTypeSafe(Class, Method) :-
    doesNotOverrideFinalMethod(Class, Method),
    methodAccessFlags(Method, AccessFlags),
    member(abstract, AccessFlags).

methodIsTypeSafe(Class, Method) :-
    doesNotOverrideFinalMethod(Class, Method),
    methodAccessFlags(Method, AccessFlags),
    member(native, AccessFlags).

private methods and static methods are orthogonal to dynamic method dispatch, so they never override other methods (5.4.5).

doesNotOverrideFinalMethod(class('java/lang/Object', L), Method) :-
    isBootstrapLoader(L).

doesNotOverrideFinalMethod(Class, Method) :-
    isPrivate(Method, Class).

doesNotOverrideFinalMethod(Class, Method) :-
    isStatic(Method, Class).

doesNotOverrideFinalMethod(Class, Method) :-
    isNotPrivate(Method, Class),
    isNotStatic(Method, Class),
    doesNotOverrideFinalMethodOfSuperclass(Class, Method).

doesNotOverrideFinalMethodOfSuperclass(Class, Method) :-
    classSuperClassName(Class, SuperclassName),
    classDefiningLoader(Class, L),
    loadedClass(SuperclassName, L, Superclass),
    classMethods(Superclass, SuperMethodList),
    finalMethodNotOverridden(Method, Superclass, SuperMethodList).

final methods that are private and/or static are unusual, as private methods and static methods cannot be overridden per se. Therefore, if a final private method or a final static method is found, it was logically not overridden by another method.

finalMethodNotOverridden(Method, Superclass, SuperMethodList) :-
    methodName(Method, Name),
    methodDescriptor(Method, Descriptor),
    member(method(_, Name, Descriptor), SuperMethodList),
    isFinal(Method, Superclass),
    isPrivate(Method, Superclass).

finalMethodNotOverridden(Method, Superclass, SuperMethodList) :-
    methodName(Method, Name),
    methodDescriptor(Method, Descriptor),
    member(method(_, Name, Descriptor), SuperMethodList),
    isFinal(Method, Superclass),
    isStatic(Method, Superclass).

If a non-final private method or a non-final static method is found, skip over it because it is orthogonal to overriding.

finalMethodNotOverridden(Method, Superclass, SuperMethodList) :-
    methodName(Method, Name),
    methodDescriptor(Method, Descriptor),
    member(method(_, Name, Descriptor), SuperMethodList),
    isNotFinal(Method, Superclass),
    isPrivate(Method, Superclass),
    doesNotOverrideFinalMethodOfSuperclass(Superclass, Method).

finalMethodNotOverridden(Method, Superclass, SuperMethodList) :-
    methodName(Method, Name),
    methodDescriptor(Method, Descriptor),
    member(method(_, Name, Descriptor), SuperMethodList),
    isNotFinal(Method, Superclass),
    isStatic(Method, Superclass),
    doesNotOverrideFinalMethodOfSuperclass(Superclass, Method).

If a non-final, non-private, non-static method is found, then indeed a final method was not overridden. Otherwise, recurse upwards.

finalMethodNotOverridden(Method, Superclass, SuperMethodList) :-
    methodName(Method, Name),
    methodDescriptor(Method, Descriptor),
    member(method(_, Name, Descriptor), SuperMethodList),
    isNotFinal(Method, Superclass),
    isNotStatic(Method, Superclass),
    isNotPrivate(Method, Superclass).

finalMethodNotOverridden(Method, Superclass, SuperMethodList) :-
    methodName(Method, Name),
    methodDescriptor(Method, Descriptor),
    notMember(method(_, Name, Descriptor), SuperMethodList),
    doesNotOverrideFinalMethodOfSuperclass(Superclass, Method).
4.10.1.6 Type Checking Methods with Code

Non-abstract, non-native methods are type correct if they have code and the code is type correct.

methodIsTypeSafe(Class, Method) :-
    doesNotOverrideFinalMethod(Class, Method),
    methodAccessFlags(Method, AccessFlags),
    methodAttributes(Method, Attributes),
    notMember(native, AccessFlags),
    notMember(abstract, AccessFlags),
    member(attribute('Code', _), Attributes),
    methodWithCodeIsTypeSafe(Class, Method).

A method with code a Code attribute is type safe if it is possible to merge the code and the stack map frames into a single stream such that each stack map frame precedes the instruction it corresponds to, and the merged stream is type correct. The method's exception handlers, if any, must also be legal.

methodWithCodeIsTypeSafe(Class, Method) :-
methodIsTypeSafe(Class, Method) :-
    parseCodeAttribute(Class, Method, FrameSize, MaxStack,
                       ParsedCode, Handlers, StackMap),
    mergeStackMapAndCode(StackMap, ParsedCode, MergedCode),
    methodInitialStackFrame(Class, Method, FrameSize, StackFrame, ReturnType),
    Environment = environment(Class, Method, ReturnType, MergedCode,
                              MaxStack, Handlers),
    handlersAreLegal(Environment),
    mergedCodeIsTypeSafe(Environment, MergedCode, StackFrame).

Let us consider exception handlers first.

An exception handler is represented by a functor application of the form:

handler(Start, End, Target, ClassName)

whose arguments are, respectively, the start and end of the range of instructions covered by the handler, the first instruction of the handler code, and the name of the exception class that this handler is designed to handle.

An exception handler is legal if its start (Start) is less than its end (End), there exists an instruction whose offset is equal to Start, there exists an instruction whose offset equals End, there is a stack frame at the start of the handler code (Target) and the handler's exception class is assignable to the class Throwable. The exception class of a handler is Throwable if the handler's class entry is 0, otherwise it is the class named in the handler.

The constraints on Start and End are already checked as static constraints (4.9.1, 4.10).

An additional requirement exists for a handler inside an <init> method if one of the instructions covered by the handler is invokespecial of an <init> method. In this case, the fact that a handler is running means the object under construction is likely broken, so it is important that the handler does not swallow the exception and allow the enclosing <init> method to return normally to the caller. Accordingly, the handler is required to either complete abruptly by throwing an exception to the caller of the enclosing <init> method, or to loop forever.

handlersAreLegal(Environment) :-
    exceptionHandlers(Environment, Handlers),
    checklist(handlerIsLegal(Environment), Handlers).
handlerIsLegal(Environment, Handler) :-
    Handler = handler(Start, End, Target, _),
    Start < End,
    allInstructions(Environment, Instructions),
    member(instruction(Start, _), Instructions),
    offsetStackFrame(Environment, Target, _),
    instructionsIncludeEnd(Instructions, End),
    currentClassLoader(Environment, CurrentLoader),
    handlerExceptionClass(Handler, ExceptionClass, CurrentLoader),
    isBootstrapLoader(BL),
    isAssignable(ExceptionClass, class('java/lang/Throwable', BL)),
    initHandlerIsLegal(Environment, Handler).
instructionsIncludeEnd(Instructions, End) :-
    member(instruction(End, _), Instructions).
instructionsIncludeEnd(Instructions, End) :-
    member(endOfCode(End), Instructions).
handlerExceptionClass(handler(_, _, _, 0),
                      class('java/lang/Throwable', BL), _) :-
    isBootstrapLoader(BL).

handlerExceptionClass(handler(_, _, _, Name),
                      class(Name, L), L) :-
    Name \= 0.
initHandlerIsLegal(Environment, Handler) :-
    notInitHandler(Environment, Handler).

notInitHandler(Environment, Handler) :-
    Environment = environment(_Class, Method, _, Instructions, _, _),
    isNotInit(Method).

notInitHandler(Environment, Handler) :-
    Environment = environment(_Class, Method, _, Instructions, _, _),
    isInit(Method),
    member(instruction(_, invokespecial(CP)), Instructions),
    CP = method(MethodClassName, MethodName, Descriptor),
    MethodName \= '`<init>`'.

initHandlerIsLegal(Environment, Handler) :-
    isInitHandler(Environment, Handler),
    sublist(isApplicableInstruction(Target), Instructions,
            HandlerInstructions),
    noAttemptToReturnNormally(HandlerInstructions).

isInitHandler(Environment, Handler) :-
    Environment = environment(_Class, Method, _, Instructions, _, _),
    isInit(Method).
    member(instruction(_, invokespecial(CP)), Instructions),
    CP = method(MethodClassName, '`<init>`', Descriptor).

isApplicableInstruction(HandlerStart, instruction(Offset, _)) :-
    Offset >= HandlerStart.

noAttemptToReturnNormally(Instructions) :-
    notMember(instruction(_, return), Instructions).

noAttemptToReturnNormally(Instructions) :-
    member(instruction(_, athrow), Instructions).

Let us now turn to the stream of instructions and stack map frames.

Merging instructions and stack map frames into a single stream involves four cases:

To determine if the merged stream for a method is type correct, we first infer the method's initial type state.

The initial type state of a method consists of an empty operand stack and local variable types derived from the type of this and the arguments, as well as the appropriate flag, depending on whether this is an <init> method.

methodInitialStackFrame(Class, Method, FrameSize, frame(Locals, [], Flags),
                        ReturnType):-
    methodDescriptor(Method, Descriptor),
    parseMethodDescriptor(Descriptor, RawArgs, ReturnType),
    expandTypeList(RawArgs, Args),
    methodInitialThisType(Class, Method, ThisList),
    flags(ThisList, Flags),
    append(ThisList, Args, ThisArgs),
    expandToLength(ThisArgs, FrameSize, top, Locals).

Given a list of types, the following clause produces a list where every type of size 2 has been substituted by two entries: one for itself, and one top entry. The result then corresponds to the representation of the list as 32-bit words in the Java Virtual Machine.

expandTypeList([], []).
expandTypeList([Item | List], [Item | Result]) :-
    sizeOf(Item, 1),
    expandTypeList(List, Result).
expandTypeList([Item | List], [Item, top | Result]) :-
    sizeOf(Item, 2),
    expandTypeList(List, Result).
flags([uninitializedThis], [flagThisUninit]).
flags(X, []) :- X \= [uninitializedThis].

expandToLength(List, Size, _Filler, List) :-
    length(List, Size).
expandToLength(List, Size, Filler, Result) :-
    length(List, ListLength),
    ListLength < Size,
    Delta is Size - ListLength,
    length(Extra, Delta),
    checklist(=(Filler), Extra),
    append(List, Extra, Result).

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, [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').

As observed in 4.10.1.1, only the bootstrap loader is permitted to define a class named java/lang/Object.

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

We now compute whether the merged stream for a method is type correct, using the method's initial type state:

Branching to a target is type safe if the target has an associated stack frame, Frame, and the current stack frame, StackFrame, is assignable to Frame.

targetIsTypeSafe(Environment, StackFrame, Target) :-
    offsetStackFrame(Environment, Target, Frame),
    frameIsAssignable(StackFrame, Frame).

An instruction satisfies its exception handlers if it satisfies every exception handler that is applicable to the instruction.

instructionSatisfiesHandlers(Environment, Offset, ExceptionStackFrame) :-
    exceptionHandlers(Environment, Handlers),
    sublist(isApplicableHandler(Offset), Handlers, ApplicableHandlers),
    checklist(instructionSatisfiesHandler(Environment, ExceptionStackFrame),
              ApplicableHandlers).

An exception handler is applicable to an instruction if the offset of the instruction is greater or equal to the start of the handler's range and less than the end of the handler's range.

isApplicableHandler(Offset, handler(Start, End, _Target, _ClassName)) :-
    Offset >= Start,
    Offset < End.

An instruction satisfies an exception handler if the instructions's outgoing type state is ExcStackFrame, and the handler's target (the initial instruction of the handler code) is type safe assuming an incoming type state T. The type state T is derived from ExcStackFrame by replacing the operand stack with a stack whose sole element is the handler's exception class.

instructionSatisfiesHandler(Environment, ExcStackFrame, Handler) :-
    Handler = handler(_, _, Target, _),
    currentClassLoader(Environment, CurrentLoader),
    handlerExceptionClass(Handler, ExceptionClass, CurrentLoader), 
    /* The stack consists of just the exception. */
    ExcStackFrame = frame(Locals, _, Flags),
    TrueExcStackFrame = frame(Locals, [ ExceptionClass ], Flags),
    operandStackHasLegalLength(Environment, TrueExcStackFrame),
    targetIsTypeSafe(Environment, TrueExcStackFrame, Target).
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),
classesInOtherPkgWithProtectedMember(Class, MemberName,
                                     MemberDescriptor, MemberClassName,
                                     [Super | Tail],
                                     [Super | T]) :-
    classClassName(Super, MemberClassName),
    \+ sameRuntimePackage(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),
classesInOtherPkgWithProtectedMember(Class, MemberName,
                                     MemberDescriptor, MemberClassName,
                                     [Super | Tail],
                                     T) :-
    classClassName(Super, MemberClassName),
    \+ sameRuntimePackage(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,
                                     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).

The negation operator (\+) is a simpler way to test that a predicate does not hold.

4.10.1.9 Type Checking Instructions
anewarray

An anewarray instruction with operand CP is type safe iff CP refers to a constant pool entry denoting a class, interface, or array type, and one can legally replace a type matching int on the incoming operand stack with an array with component type CP yielding the outgoing type state.

instructionIsTypeSafe(anewarray(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    (CP = class(_, _) ; CP = arrayOf(_)),
    validTypeTransition(Environment, [int], arrayOf(CP),
                        StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

The form of the constant pool entry is checked by static constraints (4.9.1, 4.10).

checkcast

A checkcast instruction with operand CP is type safe iff CP refers to a constant pool entry denoting either a class or an array, and one can validly replace the type Object on top of the incoming operand stack with the type denoted by CP yielding the outgoing type state.

instructionIsTypeSafe(checkcast(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    (CP = class(_, _) ; CP = arrayOf(_)),
    isBootstrapLoader(BL),
    validTypeTransition(Environment, [class('java/lang/Object', BL)], CP,
                        StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

The form of the constant pool entry is checked by static constraints (4.9.1, 4.10).

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).
instanceof

An instanceof instruction with operand CP is type safe iff CP refers to a constant pool entry denoting either a class or an array, and one can validly replace the type Object on top of the incoming operand stack with type int yielding the outgoing type state.

instructionIsTypeSafe(instanceof(CP), Environment, _Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    (CP = class(_, _) ; CP = arrayOf(_)),
    isBootstrapLoader(BL),
    validTypeTransition(Environment, [class('java/lang/Object', BL)], int,
                        StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

The form of the constant pool entry is checked by static constraints (4.9.1, 4.10).

invokedynamic

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

instructionIsTypeSafe(invokedynamic(CP,0,0), Environment, _Offset,
                      StackFrame, NextStackFrame, ExceptionStackFrame) :-
    CP = dmethod(CallSiteName, Descriptor),
    CallSiteName \= '`<init>`',
    CallSiteName \= '`<clinit>`',
    CP = dmethod(_CallSiteName, Descriptor),
    parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
    reverse(OperandArgList, StackArgList),
    validTypeTransition(Environment, StackArgList, ReturnType,
                        StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

Method names are checked by format checking (4.4.10).

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),
    MethodName \= '`<init>`',
    MethodName \= '`<clinit>`',
instructionIsTypeSafe(invokeinterface(CP, _Count, 0), Environment, _Offset,
                      StackFrame, NextStackFrame, ExceptionStackFrame) :-
    CP = imethod(MethodClassType, _MethodName, Descriptor),
    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 <clinit> method name is prohibited by format checking (4.4.2). The <init> method name is prohibited by static constraints (4.9.1, 4.10).

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.

The Count operand is checked by static constraints (4.9.1, 4.10).

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)) :-
    thisClass(Environment, ThisClass),
    classClassName(ThisClass, MethodClassName).

validSpecialMethodClassType(Environment, class(MethodClassName, L)) :-
    thisClass(Environment, ThisClass),
    loadedSuperclasses(ThisClass, Supers),
    member(Super, Supers),
    classClassName(Super, MethodClassName),
    loadedClass(MethodClassName, L, Super).

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

The <clinit> method name is prohibited by format checking (4.4.2).

Interface methods are allowed here (4.9.1).

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

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.

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.

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)),
    CP = method(MethodClassName, '`<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).

The return type must be void, per 4.4.2.

Interface methods are allowed here (4.9.1). (While useless, HotSpot allows them in verification and delays errors until resolution/run time.)

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

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),
    MethodName \= '`<init>`',
    MethodName \= '`<clinit>`',
    (CP = method(_MethodClassType, _MethodName, Descriptor) ;
     CP = imethod(_MethodClassType, _MethodName, Descriptor)),
    parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
    reverse(OperandArgList, StackArgList),
    validTypeTransition(Environment, StackArgList, ReturnType,
                        StackFrame, NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

The <clinit> method name is prohibited by format checking (4.4.2). The <init> method name is prohibited by static constraints (4.9.1, 4.10).

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),
    MethodName \= '`<init>`',
    MethodName \= '`<clinit>`',
    CP = method(MethodClassType, MethodName, Descriptor)
    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).

The <clinit> method name is prohibited by format checking (4.4.2). The <init> method name is prohibited by static constraints (4.9.1, 4.10).

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 or ldc2_w instruction is type safe iff the equivalent ldc instruction is type safe.

instructionHasEquivalentTypeRule(ldc_w(CP), ldc(CP))
instructionHasEquivalentTypeRule(ldc2_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).

The types of constants are checked by static constraints (4.9.1, 4.10).

lookupswitch

A lookupswitch instruction is type safe if its keys are sorted, one can validly pop int off the incoming operand stack yielding a new type state BranchStackFrame, and all of the instruction's targets are valid branch targets assuming BranchStackFrame as their incoming type state.

instructionIsTypeSafe(lookupswitch(Targets, Keys), Environment, _, StackFrame,
                      afterGoto, ExceptionStackFrame) :-
    sort(Keys, Keys),
    canPop(StackFrame, [int], BranchStackFrame),
    checklist(targetIsTypeSafe(Environment, BranchStackFrame), Targets),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

The order of keys is checked by static constraints (4.9.1, 4.10).

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 form of the constant pool entry is checked by static constraints (4.9.1, 4.10).

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.

new

A new instruction with operand CP at offset Offset is type safe iff CP refers to a constant pool entry denoting a class or interface type, the type uninitialized(Offset) does not appear in the incoming operand stack, and one can validly push uninitialized(Offset) onto the incoming operand stack and replace uninitialized(Offset) with top in the incoming local variables yielding the outgoing type state.

instructionIsTypeSafe(new(CP), Environment, Offset, StackFrame,
                      NextStackFrame, ExceptionStackFrame) :-
    StackFrame = frame(Locals, OperandStack, Flags),
    CP = class(_, _),
    NewItem = uninitialized(Offset),
    notMember(NewItem, OperandStack),
    substitute(NewItem, top, Locals, NewLocals),
    validTypeTransition(Environment, [], NewItem,
                        frame(NewLocals, OperandStack, Flags),
                        NextStackFrame),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

The substitute predicate is defined in the rule for invokespecial (4.10.1.9.invokespecial).

The form of the constant pool entry is checked by static constraints (4.9.1, 4.10).

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).
tableswitch

A tableswitch instruction is type safe if its keys are sorted, one can validly pop int off the incoming operand stack yielding a new type state BranchStackFrame, and all of the instruction's targets are valid branch targets assuming BranchStackFrame as their incoming type state.

instructionIsTypeSafe(tableswitch(Targets, Keys), Environment, _Offset,
                      StackFrame, afterGoto, ExceptionStackFrame) :-
    sort(Keys, Keys),
    canPop(StackFrame, [int], BranchStackFrame),
    checklist(targetIsTypeSafe(Environment, BranchStackFrame), Targets),
    exceptionStackFrame(StackFrame, ExceptionStackFrame).

The keys are implicit, and so are guaranteed to be sorted.

4.10.2 Verification by Type Inference

A class file that does not contain a StackMapTable attribute (which necessarily has a version number of 49.0 or below) must be verified have its structural constraints verified using type inference.

4.10.2.1 The Process of Verification by Type Inference

During linking, the verifier checks the code array of the Code attribute for each method of the class file by performing data-flow analysis on each method. The verifier ensures that at any given point in the program, no matter what code path is taken to reach that point, all of the following are true:

For efficiency reasons, certain tests that could in principle be performed by the verifier are delayed until the first time the code for the method is actually invoked. In so doing, the verifier avoids loading class files unless it has to.

For example, if a method invokes another method that returns an instance of class A, and that instance is assigned only to a field of the same type, the verifier does not bother to check if the class A actually exists. However, if it is assigned to a field of the type B, the definitions of both A and B must be loaded in to ensure that A is a subclass of B.

This discussion doesn't belong here; it's covered by 5.4.

4.10.2.2 The Bytecode Verifier

The code for each method is verified independently. First, the bytes that make up the code are broken up into a sequence of instructions, and the index into the code array of the start of each instruction is placed in an array. The verifier then goes through the code a second time and parses the instructions. During this pass a data structure is built to hold information about each Java Virtual Machine instruction in the method. The operands, if any, of each instruction are checked to make sure they are valid. For instance:

These restrictions are enforced by static constraints (4.9.1) before attempting verification by type inference (4.10).

For each instruction of the method, the verifier records the contents of the operand stack and the contents of the local variable array prior to the execution of that instruction. For the operand stack, it needs to know the stack height and the type of each value on it. For each local variable, it needs to know either the type of the contents of that local variable or that the local variable contains an unusable or unknown value (it might be uninitialized). The bytecode verifier does not need to distinguish between the integral types (e.g., byte, short, char) when determining the value types on the operand stack.

Next, a data-flow analyzer is initialized. For the first instruction of the method, the local variables that represent parameters initially contain values of the types indicated by the method's type descriptor; the operand stack is empty. All other local variables contain an illegal value. For the other instructions, which have not been examined yet, no information is available regarding the operand stack or local variables.

Finally, the data-flow analyzer is run. For each instruction, a "changed" bit indicates whether this instruction needs to be looked at. Initially, the "changed" bit is set only for the first instruction. The data-flow analyzer executes the following loop:

  1. Select a Java Virtual Machine instruction whose "changed" bit is set. If no instruction remains whose "changed" bit is set, the method has successfully been verified. Otherwise, turn off the "changed" bit of the selected instruction.

  2. Model the effect of the instruction on the operand stack and local variable array by doing the following:

    • If the instruction uses values from the operand stack, ensure that there are a sufficient number of values on the stack and that the top values on the stack are of an appropriate type. Otherwise, verification fails.

    • If the instruction uses a local variable, ensure that the specified local variable contains a value of the appropriate type. Otherwise, verification fails.

    • If the instruction pushes values onto the operand stack, ensure that there is sufficient room on the operand stack for the new values. Add the indicated types to the top of the modeled operand stack.

    • If the instruction modifies a local variable, record that the local variable now contains the new type.

  3. Determine the instructions that can follow the current instruction. Successor instructions can be one of the following:

    • The next instruction, if the current instruction is not an unconditional control transfer instruction (for instance, goto, return, or athrow). Verification fails if it is possible to "fall off" the last instruction of the method.

    • The target(s) of a conditional or unconditional branch or switch.

    • Any exception handlers for this instruction.

  4. Merge the state of the operand stack and local variable array at the end of the execution of the current instruction into each of the successor instructions, as follows:

    • If this is the first time the successor instruction has been visited, record that the operand stack and local variable values calculated in step 2 are the state of the operand stack and local variable array prior to executing the successor instruction. Set the "changed" bit for the successor instruction.

    • If the successor instruction has been seen before, merge the operand stack and local variable values calculated in step 2 into the values already there. Set the "changed" bit if there is any modification to the values.

    In the special case of control transfer to an exception handler:

    • Record that a single object, of the exception type indicated by the exception handler, is the state of the operand stack prior to executing the successor instruction. There must be sufficient room on the operand stack for this single value, as if an instruction had pushed it.

    • Record that the local variable values from immediately before step 2 are the state of the local variable array prior to executing the successor instruction. The local variable values calculated in step 2 are irrelevant.

  5. Continue at step 1.

To merge two operand stacks, the number of values on each stack must be identical. Then, corresponding values on the two stacks are compared and the value on the merged stack is computed, as follows:

If the operand stacks cannot be merged, verification of the method fails.

To merge two local variable array states, corresponding pairs of local variables are compared. The value of the merged local variable is computed using the rules above, except that the corresponding values are permitted to be different primitive types. In that case, the verifier records that the merged local variable contains an unusable value.

If the data-flow analyzer runs on a method without reporting a verification failure, then the method has been successfully verified by the class file verifier.

Certain instructions and data types complicate the data-flow analyzer. We now examine each of these in more detail.