A class file whose version number is 50.0 or above (§4.1) must be verified 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).
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.
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.
We stipulate the existence of 28 Prolog predicates ("accessors") that have certain expected behavior but whose formal definitions are not given in this specification.
Extracts the name, SuperClassName, of the superclass of class Class.
Extracts a list, Interfaces, of the direct superinterfaces of the class Class.
Extracts a list, Methods, of the methods declared in the class Class.
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.
Extracts the defining class loader, Loader, of the class Class.
True iff the class loader Loader is the bootstrap class loader.
True iff there exists a class named Name whose representation (in accordance with this specification) when loaded by the class loader InitiatingLoader is ClassDefinition.
Extracts the access flags, AccessFlags, of the method Method.
Extracts a list, Attributes, of the attributes of the method Method.
True iff there is a member named MemberName with descriptor MemberDescriptor in the class MemberClass and it is protected.
True iff there is a member named MemberName with descriptor MemberDescriptor in the class MemberClass and it is not protected.
Converts a field descriptor, Descriptor, into the corresponding verification type Type (§4.10.1.2).
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.
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.
True iff the package names of Class1 and Class2 are the same.
True iff the package names of Class1 and Class2 are different.
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:
a class
a method
the declared return type of the method
the instructions in a method
the maximal size of the operand stack
a list of exception handlers
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).
thisClass(Environment, class(ClassName, L)) :-
Environment = environment(Class, _Method, _ReturnType,
_Instructions, _, _),
classDefiningLoader(Class, L),
classClassName(Class, ClassName).
thisMethodReturnType(Environment, ReturnType) :-
Environment = environment(_Class, _Method, ReturnType,
_Instructions, _, _).
We specify additional predicates to extract higher-level information from the environment.
offsetStackFrame(Environment, Offset, StackFrame) :-
allInstructions(Environment, Instructions),
member(stackMap(Offset, StackFrame), Instructions).
currentClassLoader(Environment, Loader) :-
thisClass(Environment, class(_, Loader)).
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.
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 |
/ \ | type hierarchy |
uninitializedThis uninitialized(Offset) +------------------+
|
|
null
Most verification types have a direct correspondence with the primitive and reference types represented by field descriptors in Table 4.3-A:
The primitive types double, float, int, and long (field descriptors D, F, I, J) each correspond to the verification type of the same name.
The primitive types byte, char, short, and boolean (field descriptors B, C, S, Z) all correspond to the verification type int.
Class and interface types correspond to verification types that use the functor class. The verification type class(N, L) represents the class whose binary name is N as loaded by the loader L. Note that L is an initiating loader (§5.3) of the class represented by class(N, L) and may, or may not, be the class's defining loader.
For example, the class type Object would be represented as class('java/lang/Object', BL), where BL is the bootstrap loader.
Array types correspond to verification types that use the functor arrayOf. The verification type arrayOf(T) represents the array type whose component type is the verification type T.
For example, the types int[] and Object[] would be represented by arrayOf(int) and arrayOf(class('java/lang/Object', BL)) respectively.
The verification type uninitialized(Offset) is represented by applying the functor uninitialized to an argument representing the numerical value of the Offset.
Other verification types are represented in Prolog as atoms whose name denotes the verification type in question.
The subtyping rules for verification types are as follows.
Subtyping is reflexive.
isAssignable(X, X).
The verification types which are not reference types in the Java programming language have subtype rules of the form:
isAssignable(v, X) :- isAssignable(the_direct_supertype_of_v, X).
That is, v is a subtype of X if the direct supertype of v is a subtype of X. The rules are:
isAssignable(oneWord, top).
isAssignable(twoWord, top).
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(uninitialized, X) :- isAssignable(reference, X).
isAssignable(uninitializedThis, X) :- isAssignable(uninitialized, X).
isAssignable(uninitialized(_), X) :- isAssignable(uninitialized, X).
isAssignable(null, class(_, _)).
isAssignable(null, arrayOf(_)).
isAssignable(null, X) :- isAssignable(class('java/lang/Object', BL), X),
isBootstrapLoader(BL).
These subtype rules are not necessarily the most obvious formulation of subtyping. There is a clear split between subtyping rules for reference types in the Java programming language, 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.
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)).
For assignments, interfaces are treated like Object.
isJavaAssignable(class(_, _), class(To, L)) :-
loadedClass(To, L, ToClass),
classIsInterface(ToClass).
isJavaAssignable(From, To) :-
isJavaSubclassOf(From, To).
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).
Subtyping between arrays of primitive type is the identity relation.
isJavaAssignable(arrayOf(X), arrayOf(Y)) :-
atom(X),
atom(Y),
X = Y.
Subtyping between arrays of reference type is covariant.
isJavaAssignable(arrayOf(X), arrayOf(Y)) :-
compound(X), compound(Y), isJavaAssignable(X, Y).
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).
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).
4.10.1.3. Instruction Representation
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.
A few instructions have operands that are constant pool entries representing fields, methods, and dynamic call sites. In the constant pool, a field is represented by a CONSTANT_Fieldref_info structure, a method is represented by a CONSTANT_InterfaceMethodref_info structure (for an interface's method) or a CONSTANT_Methodref_info structure (for a class's method), and a dynamic call site is represented by a CONSTANT_InvokeDynamic_info structure (§4.4.2, §4.4.10). Such structures are represented as functor applications of the form:
field(FieldClassName, FieldName, FieldDescriptor) for a field, where FieldClassName is the name of the class referenced by the class_index item in the CONSTANT_Fieldref_info structure, and FieldName and FieldDescriptor correspond to the name and field descriptor referenced by the name_and_type_index item of the CONSTANT_Fieldref_info structure.
imethod(MethodIntfName, MethodName, MethodDescriptor) for an interface's method, where MethodIntfName is the name of the interface referenced by the class_index item of the CONSTANT_InterfaceMethodref_info structure, and MethodName and MethodDescriptor correspond to the name and method descriptor referenced by the name_and_type_index item of the CONSTANT_InterfaceMethodref_info structure;
method(MethodClassName, MethodName, MethodDescriptor) for a class's method, where MethodClassName is the name of the class referenced by the class_index item of the CONSTANT_Methodref_info structure, and MethodName and MethodDescriptor correspond to the name and method descriptor referenced by the name_and_type_index item of the CONSTANT_Methodref_info structure; and
dmethod(CallSiteName, MethodDescriptor) for a dynamic call site, where CallSiteName and MethodDescriptor correspond to the name and method descriptor referenced by the name_and_type_index item of the CONSTANT_InvokeDynamic_info structure.
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.
For example, a getfield instruction whose operand was an index into the constant pool that refers to a field foo of type F in class Bar would be represented as getfield(field('Bar', 'foo', 'F')).
Constant pool entries that refer to constant values, such as CONSTANT_String, CONSTANT_Integer, CONSTANT_Float, CONSTANT_Long, CONSTANT_Double, and CONSTANT_Class, are encoded via the functors whose names are string, int, float, long, double, and classConstant respectively.
For example, an ldc instruction for loading the integer 91 would be encoded as ldc(int(91)).
Stack map frames are represented in Prolog as a list of terms of the form:
stackMap(Offset, TypeState)
Offset is an integer indicating the bytecode offset at which the stack map frame applies (§4.7.4).
The order of bytecode offsets in this list must be the same as in the class file.
TypeState is the expected incoming type state for the instruction at Offset.
A type state is a mapping from locations in the operand stack and local variables of a method to verification types. It has the form:
frame(Locals, OperandStack, Flags)
Locals is a list of verification types, such that the i'th element of the list (with 0-based indexing) represents the type of local variable i.
OperandStack is a list of verification types, such that the first element of the list represents the type of the top of the operand stack, and the types of stack entries below the top follow in the list in the appropriate order.
Types of size 2 (long and double) are represented by two stack entries, with the first entry being top and the second entry being the type itself.
For example, a stack with a double value, an int value, and a long value is represented in a type state as a stack with five entries: top and double entries for the double value, an int entry for the int value, and top and long entries for the long value. Accordingly, OperandStack is the list [top, double, int, top, long].
Flags is a list which may either be empty or have the single element flagThisUninit.
If any local variable in Locals has the type uninitializedThis, then Flags has the single element flagThisUninit, otherwise Flags is an empty list.
flagThisUninit is used in constructors to mark type states where initialization of this has not yet been completed. In such type states, it is illegal to return from the method.
Subtyping of verification types is extended pointwise to type states.
The local variable array of a method has a fixed length by construction (see methodInitialStackFrame in §4.10.1.6) while the operand stack grows and shrinks. Therefore, we require an explicit check on the length of the operand stacks whose assignability is desired.
frameIsAssignable(frame(Locals1, StackMap1, Flags1),
frame(Locals2, StackMap2, Flags2)) :-
length(StackMap1, StackMapLength),
length(StackMap2, StackMapLength),
maplist(isAssignable, Locals1, Locals2),
maplist(isAssignable, StackMap1, StackMap2),
subset(Flags1, Flags2).
The length of the operand stack must not exceed the declared maximum stack length.
operandStackHasLegalLength(Environment, OperandStack) :-
length(OperandStack, Length),
maxOperandStackLength(Environment, MaxStack),
Length =< MaxStack.
Certain array instructions (§aaload, §arraylength, §baload, §bastore) peek at the types of values on the operand stack in order to check they are array types. The following clause accesses the i'th element of the operand stack from a type state.
nth1OperandStackIs(i, frame(_Locals, OperandStack, _Flags), Element) :-
nth1(i, OperandStack, Element).
Manipulation of the operand stack by load and store instructions (§4.10.1.7) is complicated by the fact that some types occupy two entries on the stack. The predicates given below take this into account, allowing the rest of the specification to abstract from this issue.
Pop a list of types off the stack.
canPop(frame(Locals, OperandStack, Flags), Types,
frame(Locals, PoppedOperandStack, Flags)) :-
popMatchingList(OperandStack, Types, PoppedOperandStack).
popMatchingList(OperandStack, [], OperandStack).
popMatchingList(OperandStack, [P | Rest], NewOperandStack) :-
popMatchingType(OperandStack, P, TempOperandStack, _ActualType),
popMatchingList(TempOperandStack, Rest, NewOperandStack).
Pop an individual type off the stack. More precisely, if the logical top of the stack is some subtype of the specified type, Type, then pop it. If a type occupies two stack entries, then the logical top of the stack is really the type just below the top, and the top of the stack is the unusable type top.
popMatchingType([ActualType | OperandStack],
Type, OperandStack, ActualType) :-
sizeOf(Type, 1),
isAssignable(ActualType, Type).
popMatchingType([top, ActualType | OperandStack],
Type, OperandStack, ActualType) :-
sizeOf(Type, 2),
isAssignable(ActualType, Type).
sizeOf(X, 2) :- isAssignable(X, twoWord).
sizeOf(X, 1) :- isAssignable(X, oneWord).
sizeOf(top, 1).
Push a logical type onto the stack. The exact behavior varies with the size of the type. If the pushed type is of size 1, we just push it onto the stack. If the pushed type is of size 2, we push it, and then push top.
pushOperandStack(OperandStack, 'void', OperandStack).
pushOperandStack(OperandStack, Type, [Type | OperandStack]) :-
sizeOf(Type, 1).
pushOperandStack(OperandStack, Type, [top, Type | OperandStack]) :-
sizeOf(Type, 2).
Push a list of types onto the stack if there is space.
canSafelyPush(Environment, InputOperandStack, Type, OutputOperandStack) :-
pushOperandStack(InputOperandStack, Type, OutputOperandStack),
operandStackHasLegalLength(Environment, OutputOperandStack).
canSafelyPushList(Environment, InputOperandStack, Types,
OutputOperandStack) :-
canPushList(InputOperandStack, Types, OutputOperandStack),
operandStackHasLegalLength(Environment, OutputOperandStack).
canPushList(InputOperandStack, [], InputOperandStack).
canPushList(InputOperandStack, [Type | Rest], OutputOperandStack) :-
pushOperandStack(InputOperandStack, Type, InterimOperandStack),
canPushList(InterimOperandStack, Rest, OutputOperandStack).
Manipulation of the operand stack by the dup instructions is specified entirely in terms of the category of types for values on the stack (§2.11.1).
Category 1 types occupy a single stack entry. Popping a logical type of category 1, Type, off the stack is possible if the top of the stack is Type and Type is not top (otherwise it could denote the upper half of a category 2 type). The result is the incoming stack, with the top entry popped off.
popCategory1([Type | Rest], Type, Rest) :-
Type \= top,
sizeOf(Type, 1).
Category 2 types occupy two stack entries. Popping a logical type of category 2, Type, off the stack is possible if the top of the stack is type top, and the entry directly below it is Type. The result is the incoming stack, with the top two entries popped off.
popCategory2([top, Type | Rest], Type, Rest) :-
sizeOf(Type, 2).
Most of the type rules for individual instructions (§4.10.1.9) depend on the notion of a valid type transition. A type transition is valid if one can pop a list of expected types off the incoming type state's operand stack and replace them with an expected result type, resulting in a new valid type state. In particular, the size of the operand stack in the new type state must not exceed its maximum declared size.
validTypeTransition(Environment, ExpectedTypesOnStack, ResultType,
frame(Locals, InputOperandStack, Flags),
frame(Locals, NextOperandStack, Flags)) :-
popMatchingList(InputOperandStack, ExpectedTypesOnStack,
InterimOperandStack),
pushOperandStack(InterimOperandStack, ResultType, NextOperandStack),
operandStackHasLegalLength(Environment, NextOperandStack).
4.10.1.5. Type Checking Abstract and Native Methods
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 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) :-
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, 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.
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:
Merging an empty StackMap and a list of instructions yields the original list of instructions.
mergeStackMapAndCode([], CodeList, CodeList).
Given a list of stack map frames beginning with the type state for the instruction at Offset, and a list of instructions beginning at Offset, the merged list is the head of the stack map frame list, followed by the head of the instruction list, followed by the merge of the tails of the two lists.
mergeStackMapAndCode([stackMap(Offset, Map) | RestMap],
[instruction(Offset, Parse) | RestCode],
[stackMap(Offset, Map),
instruction(Offset, Parse) | RestMerge]) :-
mergeStackMapAndCode(RestMap, RestCode, RestMerge).
Otherwise, given a list of stack map frames beginning with the type state for the instruction at OffsetM, and a list of instructions beginning at OffsetP, then, if OffsetP < OffsetM, the merged list consists of the head of the instruction list, followed by the merge of the stack map frame list and the tail of the instruction list.
mergeStackMapAndCode([stackMap(OffsetM, Map) | RestMap],
[instruction(OffsetP, Parse) | RestCode],
[instruction(OffsetP, Parse) | RestMerge]) :-
OffsetP < OffsetM,
mergeStackMapAndCode([stackMap(OffsetM, Map) | RestMap],
RestCode, RestMerge).
Otherwise, the merge of the two lists is undefined. Since the instruction list has monotonically increasing offsets, the merge of the two lists is not defined unless every stack map frame offset has a corresponding instruction offset and the stack map frames are in monotonically increasing order.
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').
instanceMethodInitialThisType(Class, Method, uninitializedThis) :-
methodName(Method, '<init>'),
classClassName(Class, ClassName),
classDefiningLoader(Class, CurrentLoader),
superclassChain(ClassName, CurrentLoader, Chain),
Chain \= [].
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:
If we have a stack map frame and an incoming type state, the type state must be assignable to the one in the stack map frame. We may then proceed to type check the rest of the stream with the type state given in the stack map frame.
mergedCodeIsTypeSafe(Environment, [stackMap(Offset, MapFrame) | MoreCode],
frame(Locals, OperandStack, Flags)) :-
frameIsAssignable(frame(Locals, OperandStack, Flags), MapFrame),
mergedCodeIsTypeSafe(Environment, MoreCode, MapFrame).
A merged code stream is type safe relative to an incoming type state T if it begins with an instruction I that is type safe relative to T, and I satisfies its exception handlers (see below), and the tail of the stream is type safe given the type state following that execution of I.
NextStackFrame indicates what falls through to the following instruction. For an unconditional branch instruction, it will have the special value afterGoto. ExceptionStackFrame indicates what is passed to exception handlers.
mergedCodeIsTypeSafe(Environment, [instruction(Offset, Parse) | MoreCode],
frame(Locals, OperandStack, Flags)) :-
instructionIsTypeSafe(Parse, Environment, Offset,
frame(Locals, OperandStack, Flags),
NextStackFrame, ExceptionStackFrame),
instructionSatisfiesHandlers(Environment, Offset, ExceptionStackFrame),
mergedCodeIsTypeSafe(Environment, MoreCode, NextStackFrame).
After an unconditional branch (indicated by an incoming type state of afterGoto), if we have a stack map frame giving the type state for the following instructions, we can proceed and type check them using the type state provided by the stack map frame.
mergedCodeIsTypeSafe(Environment, [stackMap(Offset, MapFrame) | MoreCode],
afterGoto) :-
mergedCodeIsTypeSafe(Environment, MoreCode, MapFrame).
It is illegal to have code after an unconditional branch without a stack map frame being provided for it.
mergedCodeIsTypeSafe(_Environment, [instruction(_, _) | _MoreCode],
afterGoto) :-
write_ln('No stack frame after unconditional branch'),
fail.
If we have an unconditional branch at the end of the code, stop.
mergedCodeIsTypeSafe(_Environment, [endOfCode(Offset)],
afterGoto).
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.7. Type Checking Load and Store Instructions
All load instructions are variations on a common pattern, varying the type of the value that the instruction loads.
Loading a value of type Type from local variable Index is type safe, if the type of that local variable is ActualType, ActualType is assignable to Type, and pushing ActualType onto the incoming operand stack is a valid type transition (§4.10.1.4) that yields a new type state NextStackFrame. After execution of the load instruction, the type state will be NextStackFrame.
loadIsTypeSafe(Environment, Index, Type, StackFrame, NextStackFrame) :-
StackFrame = frame(Locals, _OperandStack, _Flags),
nth0(Index, Locals, ActualType),
isAssignable(ActualType, Type),
validTypeTransition(Environment, [], ActualType, StackFrame,
NextStackFrame).
All store instructions are variations on a common pattern, varying the type of the value that the instruction stores.
In general, a store instruction is type safe if the local variable it references is of a type that is a supertype of Type, and the top of the operand stack is of a subtype of Type, where Type is the type the instruction is designed to store.
More precisely, the store is type safe if one can pop a type ActualType that "matches" Type (that is, is a subtype of Type) off the operand stack (§4.10.1.4), and then legally assign that type the local variable LIndex.
storeIsTypeSafe(_Environment, Index, Type,
frame(Locals, OperandStack, Flags),
frame(NextLocals, NextOperandStack, Flags)) :-
popMatchingType(OperandStack, Type, NextOperandStack, ActualType),
modifyLocalVariable(Index, ActualType, Locals, NextLocals).
Given local variables Locals, modifying Index to have type Type results in the local variable list NewLocals. The modifications are somewhat involved, because some values (and their corresponding types) occupy two local variables. Hence, modifying LN may require modifying LN+1 (because the type will occupy both the N and N+1 slots) or LN-1 (because local N used to be the upper half of the two word value/type starting at local N-1, and so local N-1 must be invalidated), or both. This is described further below. We start at L0 and count up.
modifyLocalVariable(Index, Type, Locals, NewLocals) :-
modifyLocalVariable(0, Index, Type, Locals, NewLocals).
Given LocalsRest, the suffix of the local variable list starting at index I, modifying local variable Index to have type Type results in the local variable list suffix NextLocalsRest.
If I < Index-1, just copy the input to the output and recurse forward. If I = Index-1, the type of local I may change. This can occur if LI has a type of size 2. Once we set LI+1 to the new type (and the corresponding value), the type/value of LI will be invalidated, as its upper half will be trashed. Then we recurse forward.
modifyLocalVariable(I, Index, Type,
[Locals1 | LocalsRest],
[Locals1 | NextLocalsRest] ) :-
I < Index - 1,
I1 is I + 1,
modifyLocalVariable(I1, Index, Type, LocalsRest, NextLocalsRest).
modifyLocalVariable(I, Index, Type,
[Locals1 | LocalsRest],
[NextLocals1 | NextLocalsRest] ) :-
I =:= Index - 1,
modifyPreIndexVariable(Locals1, NextLocals1),
modifyLocalVariable(Index, Index, Type, LocalsRest, NextLocalsRest).
When we find the variable, and it only occupies one word, we change it to Type and we're done. When we find the variable, and it occupies two words, we change its type to Type and the next word to top.
modifyLocalVariable(Index, Index, Type,
[_ | LocalsRest], [Type | LocalsRest]) :-
sizeOf(Type, 1).
modifyLocalVariable(Index, Index, Type,
[_, _ | LocalsRest], [Type, top | LocalsRest]) :-
sizeOf(Type, 2).
We refer to a local whose index immediately precedes a local whose type will be modified as a pre-index variable. The future type of a pre-index variable of type InputType is Result. If the type, Type, of the pre-index local is of size 1, it doesn't change. If the type of the pre-index local, Type, is 2, we need to mark the lower half of its two word value as unusable, by setting its type to top.
modifyPreIndexVariable(Type, Type) :- sizeOf(Type, 1). modifyPreIndexVariable(Type, top) :- sizeOf(Type, 2).4.10.1.8. Type Checking for
protected Members
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:
If the name of a class is not the name of any superclass, it cannot be a superclass, and so it can safely be ignored.
passesProtectedCheck(Environment, MemberClassName, MemberName,
MemberDescriptor, StackFrame) :-
thisClass(Environment, class(CurrentClassName, CurrentLoader)),
superclassChain(CurrentClassName, CurrentLoader, Chain),
notMember(class(MemberClassName, _), Chain).
If the MemberClassName is the same as the name of a superclass, the class being resolved may indeed be a superclass. In this case, if no superclass named MemberClassName in a different run-time package has a protected member named MemberName with descriptor MemberDescriptor, the protected check does not apply.
This is because the actual class being resolved will either be one of these superclasses, in which case we know that it is either in the same run-time package, and the access is legal; or the member in question is not protected and the check does not apply; or it will be a subclass, in which case the check would succeed anyway; or it will be some other class in the same run-time package, in which case the access is legal and the check need not take place; or the verifier need not flag this as a problem, since it will be caught anyway because resolution will per force fail.
passesProtectedCheck(Environment, MemberClassName, MemberName,
MemberDescriptor, StackFrame) :-
thisClass(Environment, class(CurrentClassName, CurrentLoader)),
superclassChain(CurrentClassName, CurrentLoader, Chain),
member(class(MemberClassName, _), Chain),
classesInOtherPkgWithProtectedMember(
class(CurrentClassName, CurrentLoader),
MemberName, MemberDescriptor, MemberClassName, Chain, []).
If there does exist a protected superclass member in a different run-time package, then load MemberClassName; if the member in question is not protected, the check does not apply. (Using a superclass member that is not protected is trivially correct.)
passesProtectedCheck(Environment, MemberClassName, MemberName,
MemberDescriptor,
frame(_Locals, [Target | Rest], _Flags)) :-
thisClass(Environment, class(CurrentClassName, CurrentLoader)),
superclassChain(CurrentClassName, CurrentLoader, Chain),
member(class(MemberClassName, _), Chain),
classesInOtherPkgWithProtectedMember(
class(CurrentClassName, CurrentLoader),
MemberName, MemberDescriptor, MemberClassName, Chain, List),
List /= [],
loadedClass(MemberClassName, CurrentLoader, ReferencedClass),
isNotProtected(ReferencedClass, MemberName, MemberDescriptor).
Otherwise, use of a member of an object of type Target requires that Target be assignable to the type of the current class.
passesProtectedCheck(Environment, MemberClassName, MemberName,
MemberDescriptor,
frame(_Locals, [Target | Rest], _Flags)) :-
thisClass(Environment, class(CurrentClassName, CurrentLoader)),
superclassChain(CurrentClassName, CurrentLoader, Chain),
member(class(MemberClassName, _), Chain),
classesInOtherPkgWithProtectedMember(
class(CurrentClassName, CurrentLoader),
MemberName, MemberDescriptor, MemberClassName, Chain, List),
List /= [],
loadedClass(MemberClassName, CurrentLoader, ReferencedClass),
isProtected(ReferencedClass, MemberName, MemberDescriptor),
isAssignable(Target, class(CurrentClassName, CurrentLoader)).
The predicate classesInOtherPkgWithProtectedMember(Class, MemberName, MemberDescriptor, MemberClassName, Chain, List) is true if List is the set of classes in Chain with name MemberClassName that are in a different run-time package than Class which have a protected member named MemberName with descriptor MemberDescriptor.
classesInOtherPkgWithProtectedMember(_, _, _, _, [], []).
classesInOtherPkgWithProtectedMember(Class, MemberName,
MemberDescriptor, MemberClassName,
[class(MemberClassName, L) | Tail],
[class(MemberClassName, L) | T]) :-
differentRuntimePackage(Class, class(MemberClassName, L)),
loadedClass(MemberClassName, L, Super),
isProtected(Super, MemberName, MemberDescriptor),
classesInOtherPkgWithProtectedMember(
Class, MemberName, MemberDescriptor, MemberClassName, Tail, T).
classesInOtherPkgWithProtectedMember(Class, MemberName,
MemberDescriptor, MemberClassName,
[class(MemberClassName, L) | Tail],
T) :-
differentRuntimePackage(Class, class(MemberClassName, L)),
loadedClass(MemberClassName, L, Super),
isNotProtected(Super, MemberName, MemberDescriptor),
classesInOtherPkgWithProtectedMember(
Class, MemberName, MemberDescriptor, MemberClassName, Tail, T).
classesInOtherPkgWithProtectedMember(Class, MemberName,
MemberDescriptor, MemberClassName,
[class(MemberClassName, L) | Tail],
T] :-
sameRuntimePackage(Class, class(MemberClassName, L)),
classesInOtherPkgWithProtectedMember(
Class, MemberName, MemberDescriptor, MemberClassName, Tail, T).
sameRuntimePackage(Class1, Class2) :-
classDefiningLoader(Class1, L),
classDefiningLoader(Class2, L),
samePackageName(Class1, Class2).
differentRuntimePackage(Class1, Class2) :-
classDefiningLoader(Class1, L1),
classDefiningLoader(Class2, L2),
L1 \= L2.
differentRuntimePackage(Class1, Class2) :-
differentPackageName(Class1, Class2).
4.10.1.9. Type Checking Instructions
In general, the type rule for an instruction is given relative to an environment Environment that defines the class and method in which the instruction occurs (§4.10.1.1), and the offset Offset within the method at which the instruction occurs. The rule states that if the incoming type state StackFrame fulfills certain requirements, then:
It is provable that the type state after the instruction completes normally has a particular form given by NextStackFrame, and that the type state after the instruction completes abruptly is given by ExceptionStackFrame.
The type state after an instruction completes abruptly is the same as the incoming type state, except that the operand stack is empty.
exceptionStackFrame(StackFrame, ExceptionStackFrame) :-
StackFrame = frame(Locals, _OperandStack, Flags),
ExceptionStackFrame = frame(Locals, [], Flags).
Many instructions have type rules that are completely isomorphic to the rules for other instructions. If an instruction b1 is isomorphic to another instruction b2, then the type rule for b1 is the same as the type rule for b2.
instructionIsTypeSafe(Instruction, Environment, Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
instructionHasEquivalentTypeRule(Instruction, IsomorphicInstruction),
instructionIsTypeSafe(IsomorphicInstruction, Environment, Offset,
StackFrame, NextStackFrame,
ExceptionStackFrame).
The English language description of each rule is intended to be readable, intuitive, and concise. As such, the description avoids repeating all the contextual assumptions given above. In particular:
The description does not explicitly mention the environment.
When the description speaks of the operand stack or local variables in the following, it is referring to the operand stack and local variable components of a type state: either the incoming type state or the outgoing one.
The type state after the instruction completes abruptly is almost always identical to the incoming type state. The description only discusses the type state after the instruction completes abruptly when that is not the case.
The description speaks of popping and pushing types onto the operand stack, and does not explicitly discuss issues of stack underflow or overflow. The description assumes these operations can be completed successfully, but the Prolog clauses for operand stack manipulation ensure that the necessary checks are made.
The description discusses only the manipulation of logical types. In practice, some types take more than one word. The description abstracts from these representation details, but the Prolog clauses that manipulate data do not.
Any ambiguities can be resolved by referring to the formal Prolog clauses.
An aaload instruction is type safe iff one can validly replace types matching int and an array type with component type ComponentType where ComponentType is a subtype of Object, with ComponentType yielding the outgoing type state.
instructionIsTypeSafe(aaload, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
nth1OperandStackIs(2, StackFrame, ArrayType),
arrayComponentType(ArrayType, ComponentType),
isBootstrapLoader(BL),
validTypeTransition(Environment,
[int, arrayOf(class('java/lang/Object', BL))],
ComponentType, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The component type of an array of X is X. We define the component type of null to be null.
arrayComponentType(arrayOf(X), X). arrayComponentType(null, null).
An aastore instruction is type safe iff one can validly pop types matching Object, int, and an array of Object off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(aastore, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
isBootstrapLoader(BL),
canPop(StackFrame,
[class('java/lang/Object', BL),
int,
arrayOf(class('java/lang/Object', BL))],
NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An aconst_null instruction is type safe if one can validly push the type null onto the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(aconst_null, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [], null, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An aload instruction with operand Index is type safe and yields an outgoing type state NextStackFrame, if a load instruction with operand Index and type reference is type safe and yields an outgoing type state NextStackFrame.
instructionIsTypeSafe(aload(Index), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
loadIsTypeSafe(Environment, Index, reference, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The instructions aload_<n>, for 0 ≤ n ≤ 3, are type safe iff the equivalent aload instruction is type safe.
instructionHasEquivalentTypeRule(aload_0, aload(0)). instructionHasEquivalentTypeRule(aload_1, aload(1)). instructionHasEquivalentTypeRule(aload_2, aload(2)). instructionHasEquivalentTypeRule(aload_3, aload(3)).
An anewarray instruction with operand CP is type safe iff CP refers to a constant pool entry denoting either a class type or an 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).
An areturn instruction is type safe iff the enclosing method has a declared return type, ReturnType, that is a reference type, and one can validly pop a type matching ReturnType off the incoming operand stack.
instructionIsTypeSafe(areturn, Environment, _Offset, StackFrame,
afterGoto, ExceptionStackFrame) :-
thisMethodReturnType(Environment, ReturnType),
isAssignable(ReturnType, reference),
canPop(StackFrame, [ReturnType], _PoppedStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An arraylength instruction is type safe iff one can validly replace an array type on the incoming operand stack with the type int yielding the outgoing type state.
instructionIsTypeSafe(arraylength, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
nth1OperandStackIs(1, StackFrame, ArrayType),
arrayComponentType(ArrayType, _),
validTypeTransition(Environment, [top], int, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An astore instruction with operand Index is type safe and yields an outgoing type state NextStackFrame, if a store instruction with operand Index and type reference is type safe and yields an outgoing type state NextStackFrame.
instructionIsTypeSafe(astore(Index), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
storeIsTypeSafe(Environment, Index, reference, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The instructions astore_<n>, for 0 ≤ n ≤ 3, are type safe iff the equivalent astore instruction is type safe.
instructionHasEquivalentTypeRule(astore_0, astore(0)). instructionHasEquivalentTypeRule(astore_1, astore(1)). instructionHasEquivalentTypeRule(astore_2, astore(2)). instructionHasEquivalentTypeRule(astore_3, astore(3)).
An athrow instruction is type safe iff the top of the operand stack matches Throwable.
instructionIsTypeSafe(athrow, _Environment, _Offset, StackFrame,
afterGoto, ExceptionStackFrame) :-
isBootstrapLoader(BL),
canPop(StackFrame, [class('java/lang/Throwable', BL)], _PoppedStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A baload instruction is type safe iff one can validly replace types matching int and a small array type on the incoming operand stack with int yielding the outgoing type state.
instructionIsTypeSafe(baload, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :
nth1OperandStackIs(2, StackFrame, ArrayType),
isSmallArray(ArrayType),
validTypeTransition(Environment, [int, top], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An array type is a small array type if it is an array of byte, an array of boolean, or a subtype thereof (null).
isSmallArray(arrayOf(byte)). isSmallArray(arrayOf(boolean)). isSmallArray(null).
A bastore instruction is type safe iff one can validly pop types matching int, int and a small array type off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(bastore, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
nth1OperandStackIs(3, StackFrame, ArrayType),
isSmallArray(ArrayType),
canPop(StackFrame, [int, int, top], NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A bipush instruction is type safe iff the equivalent sipush instruction is type safe.
instructionHasEquivalentTypeRule(bipush(Value), sipush(Value)).
A caload instruction is type safe iff one can validly replace types matching int and array of char on the incoming operand stack with int yielding the outgoing type state.
instructionIsTypeSafe(caload, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int, arrayOf(char)], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A castore instruction is type safe iff one can validly pop types matching int, int and array of char off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(castore, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [int, int, arrayOf(char)], NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
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).
A d2f instruction is type safe if one can validly pop double off the incoming operand stack and replace it with float, yielding the outgoing type state.
instructionIsTypeSafe(d2f, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [double], float,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A d2i instruction is type safe if one can validly pop double off the incoming operand stack and replace it with int, yielding the outgoing type state.
instructionIsTypeSafe(d2i, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [double], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A d2l instruction is type safe if one can validly pop double off the incoming operand stack and replace it with long, yielding the outgoing type state.
instructionIsTypeSafe(d2l, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [double], long,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dadd instruction is type safe iff one can validly replace types matching double and double on the incoming operand stack with double yielding the outgoing type state.
instructionIsTypeSafe(dadd, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [double, double], double,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A daload instruction is type safe iff one can validly replace types matching int and array of double on the incoming operand stack with double yielding the outgoing type state.
instructionIsTypeSafe(daload, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int, arrayOf(double)], double,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dastore instruction is type safe iff one can validly pop types matching double, int and array of double off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(dastore, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [double, int, arrayOf(double)], NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dcmpg instruction is type safe iff one can validly replace types matching double and double on the incoming operand stack with int yielding the outgoing type state.
instructionIsTypeSafe(dcmpg, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [double, double], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dcmpl instruction is type safe iff the equivalent dcmpg instruction is type safe.
instructionHasEquivalentTypeRule(dcmpl, dcmpg).
A dconst_0 instruction is type safe if one can validly push the type double onto the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(dconst_0, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [], double, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dconst_1 instruction is type safe iff the equivalent dconst_0 instruction is type safe.
instructionHasEquivalentTypeRule(dconst_1, dconst_0).
A ddiv instruction is type safe iff the equivalent dadd instruction is type safe.
instructionHasEquivalentTypeRule(ddiv, dadd).
A dload instruction with operand Index is type safe and yields an outgoing type state NextStackFrame, if a load instruction with operand Index and type double is type safe and yields an outgoing type state NextStackFrame.
instructionIsTypeSafe(dload(Index), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
loadIsTypeSafe(Environment, Index, double, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The instructions dload_<n>, for 0 ≤ n ≤ 3, are typesafe iff the equivalent dload instruction is type safe.
instructionHasEquivalentTypeRule(dload_0, dload(0)). instructionHasEquivalentTypeRule(dload_1, dload(1)). instructionHasEquivalentTypeRule(dload_2, dload(2)). instructionHasEquivalentTypeRule(dload_3, dload(3)).
A dmul instruction is type safe iff the equivalent dadd instruction is type safe.
instructionHasEquivalentTypeRule(dmul, dadd).
A dneg instruction is type safe iff there is a type matching double on the incoming operand stack. The dneg instruction does not alter the type state.
instructionIsTypeSafe(dneg, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [double], double,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A drem instruction is type safe iff the equivalent dadd instruction is type safe.
instructionHasEquivalentTypeRule(drem, dadd).
A dreturn instruction is type safe if the enclosing method has a declared return type of double, and one can validly pop a type matching double off the incoming operand stack.
instructionIsTypeSafe(dreturn, Environment, _Offset, StackFrame,
afterGoto, ExceptionStackFrame) :-
thisMethodReturnType(Environment, double),
canPop(StackFrame, [double], _PoppedStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dstore instruction with operand Index is type safe and yields an outgoing type state NextStackFrame, if a store instruction with operand Index and type double is type safe and yields an outgoing type state NextStackFrame.
instructionIsTypeSafe(dstore(Index), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
storeIsTypeSafe(Environment, Index, double, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The instructions dstore_<n>, for 0 ≤ n ≤ 3, are type safe iff the equivalent dstore instruction is type safe.
instructionHasEquivalentTypeRule(dstore_0, dstore(0)). instructionHasEquivalentTypeRule(dstore_1, dstore(1)). instructionHasEquivalentTypeRule(dstore_2, dstore(2)). instructionHasEquivalentTypeRule(dstore_3, dstore(3)).
A dsub instruction is type safe iff the equivalent dadd instruction is type safe.
instructionHasEquivalentTypeRule(dsub, dadd).
A dup instruction is type safe iff one can validly replace a category 1 type, Type, with the types Type, Type, yielding the outgoing type state.
instructionIsTypeSafe(dup, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
StackFrame = frame(Locals, InputOperandStack, Flags),
popCategory1(InputOperandStack, Type, _),
canSafelyPush(Environment, InputOperandStack, Type, OutputOperandStack),
NextStackFrame = frame(Locals, OutputOperandStack, Flags),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dup_x1 instruction is type safe iff one can validly replace two category 1 types, Type1, and Type2, on the incoming operand stack with the types Type1, Type2, Type1, yielding the outgoing type state.
instructionIsTypeSafe(dup_x1, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
StackFrame = frame(Locals, InputOperandStack, Flags),
popCategory1(InputOperandStack, Type1, Stack1),
popCategory1(Stack1, Type2, Rest),
canSafelyPushList(Environment, Rest, [Type1, Type2, Type1],
OutputOperandStack),
NextStackFrame = frame(Locals, OutputOperandStack, Flags),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dup_x2 instruction is type safe iff it is a type safe form of the dup_x2 instruction.
instructionIsTypeSafe(dup_x2, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
StackFrame = frame(Locals, InputOperandStack, Flags),
dup_x2FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack),
NextStackFrame = frame(Locals, OutputOperandStack, Flags),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dup_x2 instruction is a type safe form of the dup_x2 instruction iff it is a type safe form 1 dup_x2 instruction or a type safe form 2 dup_x2 instruction.
dup_x2FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
dup_x2Form1IsTypeSafe(Environment, InputOperandStack, OutputOperandStack).
dup_x2FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
dup_x2Form2IsTypeSafe(Environment, InputOperandStack, OutputOperandStack).
A dup_x2 instruction is a type safe form 1 dup_x2 instruction iff one can validly replace three category 1 types, Type1, Type2, Type3 on the incoming operand stack with the types Type1, Type2, Type3, Type1, yielding the outgoing type state.
dup_x2Form1IsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
popCategory1(InputOperandStack, Type1, Stack1),
popCategory1(Stack1, Type2, Stack2),
popCategory1(Stack2, Type3, Rest),
canSafelyPushList(Environment, Rest, [Type1, Type3, Type2, Type1],
OutputOperandStack).
A dup_x2 instruction is a type safe form 2 dup_x2 instruction iff one can validly replace a category 1 type, Type1, and a category 2 type, Type2, on the incoming operand stack with the types Type1, Type2, Type1, yielding the outgoing type state.
dup_x2Form2IsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
popCategory1(InputOperandStack, Type1, Stack1),
popCategory2(Stack1, Type2, Rest),
canSafelyPushList(Environment, Rest, [Type1, Type2, Type1],
OutputOperandStack).
A dup2 instruction is type safe iff it is a type safe form of the dup2 instruction.
instructionIsTypeSafe(dup2, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
StackFrame = frame(Locals, InputOperandStack, Flags),
dup2FormIsTypeSafe(Environment,InputOperandStack, OutputOperandStack),
NextStackFrame = frame(Locals, OutputOperandStack, Flags),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dup2 instruction is a type safe form of the dup2 instruction iff it is a type safe form 1 dup2 instruction or a type safe form 2 dup2 instruction.
dup2FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
dup2Form1IsTypeSafe(Environment,InputOperandStack, OutputOperandStack).
dup2FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
dup2Form2IsTypeSafe(Environment,InputOperandStack, OutputOperandStack).
A dup2 instruction is a type safe form 1 dup2 instruction iff one can validly replace two category 1 types, Type1 and Type2 on the incoming operand stack with the types Type1, Type2, Type1, Type2, yielding the outgoing type state.
dup2Form1IsTypeSafe(Environment, InputOperandStack, OutputOperandStack):-
popCategory1(InputOperandStack, Type1, TempStack),
popCategory1(TempStack, Type2, _),
canSafelyPushList(Environment, InputOperandStack, [Type1, Type2],
OutputOperandStack).
A dup2 instruction is a type safe form 2 dup2 instruction iff one can validly replace a category 2 type, Type on the incoming operand stack with the types Type, Type, yielding the outgoing type state.
dup2Form2IsTypeSafe(Environment, InputOperandStack, OutputOperandStack):-
popCategory2(InputOperandStack, Type, _),
canSafelyPush(Environment, InputOperandStack, Type, OutputOperandStack).
A dup2_x1 instruction is type safe iff it is a type safe form of the dup2_x1 instruction.
instructionIsTypeSafe(dup2_x1, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
StackFrame = frame(Locals, InputOperandStack, Flags),
dup2_x1FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack),
NextStackFrame = frame(Locals, OutputOperandStack, Flags),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dup2_x1 instruction is a type safe form of the dup2_x1 instruction iff it is a type safe form 1 dup2_x1 instruction or a type safe form 2 dup_x2 instruction.
dup2_x1FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
dup2_x1Form1IsTypeSafe(Environment, InputOperandStack, OutputOperandStack).
dup2_x1FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
dup2_x1Form2IsTypeSafe(Environment, InputOperandStack, OutputOperandStack).
A dup2_x1 instruction is a type safe form 1 dup2_x1 instruction iff one can validly replace three category 1 types, Type1, Type2, Type3, on the incoming operand stack with the types Type1, Type2, Type3, Type1, Type2, yielding the outgoing type state.
dup2_x1Form1IsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
popCategory1(InputOperandStack, Type1, Stack1),
popCategory1(Stack1, Type2, Stack2),
popCategory1(Stack2, Type3, Rest),
canSafelyPushList(Environment, Rest, [Type2, Type1, Type3, Type2, Type1],
OutputOperandStack).
A dup2_x1 instruction is a type safe form 2 dup2_x1 instruction iff one can validly replace a category 2 type, Type1, and a category 1 type, Type2, on the incoming operand stack with the types Type1, Type2, Type1, yielding the outgoing type state.
dup2_x1Form2IsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
popCategory2(InputOperandStack, Type1, Stack1),
popCategory1(Stack1, Type2, Rest),
canSafelyPushList(Environment, Rest, [Type1, Type2, Type1],
OutputOperandStack).
A dup2_x2 instruction is type safe iff it is a type safe form of the dup2_x2 instruction.
instructionIsTypeSafe(dup2_x2, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
StackFrame = frame(Locals, InputOperandStack, Flags),
dup2_x2FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack),
NextStackFrame = frame(Locals, OutputOperandStack, Flags),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A dup2_x2 instruction is a type safe form of the dup2_x2 instruction iff one of the following holds:
dup2_x2FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
dup2_x2Form1IsTypeSafe(Environment, InputOperandStack, OutputOperandStack).
dup2_x2FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
dup2_x2Form2IsTypeSafe(Environment, InputOperandStack, OutputOperandStack).
dup2_x2FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
dup2_x2Form3IsTypeSafe(Environment, InputOperandStack, OutputOperandStack).
dup2_x2FormIsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
dup2_x2Form4IsTypeSafe(Environment, InputOperandStack, OutputOperandStack).
A dup2_x2 instruction is a type safe form 1 dup2_x2 instruction iff one can validly replace four category 1 types, Type1, Type2, Type3, Type4, on the incoming operand stack with the types Type1, Type2, Type3, Type4, Type1, Type2, yielding the outgoing type state.
dup2_x2Form1IsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
popCategory1(InputOperandStack, Type1, Stack1),
popCategory1(Stack1, Type2, Stack2),
popCategory1(Stack2, Type3, Stack3),
popCategory1(Stack3, Type4, Rest),
canSafelyPushList(Environment, Rest,
[Type2, Type1, Type4, Type3, Type2, Type1],
OutputOperandStack).
A dup2_x2 instruction is a type safe form 2 dup2_x2 instruction iff one can validly replace a category 2 type, Type1, and two category 1 types, Type2, Type3, on the incoming operand stack with the types Type1, Type2, Type3, Type1, yielding the outgoing type state.
dup2_x2Form2IsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
popCategory2(InputOperandStack, Type1, Stack1),
popCategory1(Stack1, Type2, Stack2),
popCategory1(Stack2, Type3, Rest),
canSafelyPushList(Environment, Rest,
[Type1, Type3, Type2, Type1],
OutputOperandStack).
A dup2_x2 instruction is a type safe form 3 dup2_x2 instruction iff one can validly replace two category 1 types, Type1, Type2, and a category 2 type, Type3, on the incoming operand stack with the types Type1, Type2, Type3, Type1, Type2, yielding the outgoing type state.
dup2_x2Form3IsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
popCategory1(InputOperandStack, Type1, Stack1),
popCategory1(Stack1, Type2, Stack2),
popCategory2(Stack2, Type3, Rest),
canSafelyPushList(Environment, Rest,
[Type2, Type1, Type3, Type2, Type1],
OutputOperandStack).
A dup2_x2 instruction is a type safe form 4 dup2_x2 instruction iff one can validly replace two category 2 types, Type1, Type2, on the incoming operand stack with the types Type1, Type2, Type1, yielding the outgoing type state.
dup2_x2Form4IsTypeSafe(Environment, InputOperandStack, OutputOperandStack) :-
popCategory2(InputOperandStack, Type1, Stack1),
popCategory2(Stack1, Type2, Rest),
canSafelyPushList(Environment, Rest, [Type1, Type2, Type1],
OutputOperandStack).
An f2d instruction is type safe if one can validly pop float off the incoming operand stack and replace it with double, yielding the outgoing type state.
instructionIsTypeSafe(f2d, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [float], double,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An f2i instruction is type safe if one can validly pop float off the incoming operand stack and replace it with int, yielding the outgoing type state.
instructionIsTypeSafe(f2i, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [float], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An f2l instruction is type safe if one can validly pop float off the incoming operand stack and replace it with long, yielding the outgoing type state.
instructionIsTypeSafe(f2l, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [float], long,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An fadd instruction is type safe iff one can validly replace types matching float and float on the incoming operand stack with float yielding the outgoing type state.
instructionIsTypeSafe(fadd, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [float, float], float,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An faload instruction is type safe iff one can validly replace types matching int and array of float on the incoming operand stack with float yielding the outgoing type state.
instructionIsTypeSafe(faload, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int, arrayOf(float)], float,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An fastore instruction is type safe iff one can validly pop types matching float, int and array of float off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(fastore, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [float, int, arrayOf(float)], NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An fcmpg instruction is type safe iff one can validly replace types matching float and float on the incoming operand stack with int yielding the outgoing type state.
instructionIsTypeSafe(fcmpg, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [float, float], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An fcmpl instruction is type safe iff the equivalent fcmpg instruction is type safe.
instructionHasEquivalentTypeRule(fcmpl, fcmpg).
An fconst_0 instruction is type safe if one can validly push the type float onto the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(fconst_0, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [], float, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The rules for the other variants of fconst are equivalent.
instructionHasEquivalentTypeRule(fconst_1, fconst_0). instructionHasEquivalentTypeRule(fconst_2, fconst_0).
An fdiv instruction is type safe iff the equivalent fadd instruction is type safe.
instructionHasEquivalentTypeRule(fdiv, fadd).
An fload instruction with operand Index is type safe and yields an outgoing type state NextStackFrame, if a load instruction with operand Index and type float is type safe and yields an outgoing type state NextStackFrame.
instructionIsTypeSafe(fload(Index), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
loadIsTypeSafe(Environment, Index, float, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The instructions fload_<n>, for 0 ≤ n ≤ 3, are typesafe iff the equivalent fload instruction is type safe.
instructionHasEquivalentTypeRule(fload_0, fload(0)). instructionHasEquivalentTypeRule(fload_1, fload(1)). instructionHasEquivalentTypeRule(fload_2, fload(2)). instructionHasEquivalentTypeRule(fload_3, fload(3)).
An fmul instruction is type safe iff the equivalent fadd instruction is type safe.
instructionHasEquivalentTypeRule(fmul, fadd).
An fneg instruction is type safe iff there is a type matching float on the incoming operand stack. The fneg instruction does not alter the type state.
instructionIsTypeSafe(fneg, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [float], float,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An frem instruction is type safe iff the equivalent fadd instruction is type safe.
instructionHasEquivalentTypeRule(frem, fadd).
An freturn instruction is type safe if the enclosing method has a declared return type of float, and one can validly pop a type matching float off the incoming operand stack.
instructionIsTypeSafe(freturn, Environment, _Offset, StackFrame,
afterGoto, ExceptionStackFrame) :-
thisMethodReturnType(Environment, float),
canPop(StackFrame, [float], _PoppedStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An fstore instruction with operand Index is type safe and yields an outgoing type state NextStackFrame, if a store instruction with operand Index and type float is type safe and yields an outgoing type state NextStackFrame.
instructionIsTypeSafe(fstore(Index), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
storeIsTypeSafe(Environment, Index, float, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The instructions fstore_<n>, for 0 ≤ n ≤ 3, are typesafe iff the equivalent fstore instruction is type safe.
instructionHasEquivalentTypeRule(fstore_0, fstore(0)). instructionHasEquivalentTypeRule(fstore_1, fstore(1)). instructionHasEquivalentTypeRule(fstore_2, fstore(2)). instructionHasEquivalentTypeRule(fstore_3, fstore(3)).
An fsub instruction is type safe iff the equivalent fadd instruction is type safe.
instructionHasEquivalentTypeRule(fsub, fadd).
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 FieldClass, and one can validly replace a type matching FieldClass with type FieldType on the incoming operand stack yielding the outgoing type state. FieldClass must not be an array type. protected fields are subject to additional checks (§4.10.1.8).
instructionIsTypeSafe(getfield(CP), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
CP = field(FieldClass, FieldName, FieldDescriptor),
parseFieldDescriptor(FieldDescriptor, FieldType),
passesProtectedCheck(Environment, FieldClass, FieldName,
FieldDescriptor, StackFrame),
validTypeTransition(Environment, [class(FieldClass)], FieldType,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
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(_FieldClass, _FieldName, FieldDescriptor),
parseFieldDescriptor(FieldDescriptor, FieldType),
validTypeTransition(Environment, [], FieldType,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A goto instruction is type safe iff its target operand is a valid branch target.
instructionIsTypeSafe(goto(Target), Environment, _Offset, StackFrame,
afterGoto, ExceptionStackFrame) :-
targetIsTypeSafe(Environment, StackFrame, Target),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A goto_w instruction is type safe iff the equivalent goto instruction is type safe.
instructionHasEquivalentTypeRule(goto_w(Target), goto(Target)).i2b, i2c, i2d, i2f, i2l, i2s
An i2b instruction is type safe iff the equivalent ineg instruction is type safe.
instructionHasEquivalentTypeRule(i2b, ineg).
An i2c instruction is type safe iff the equivalent ineg instruction is type safe.
instructionHasEquivalentTypeRule(i2c, ineg).
An i2d instruction is type safe if one can validly pop int off the incoming operand stack and replace it with double, yielding the outgoing type state.
instructionIsTypeSafe(i2d, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int], double,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An i2f instruction is type safe if one can validly pop int off the incoming operand stack and replace it with float, yielding the outgoing type state.
instructionIsTypeSafe(i2f, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int], float,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An i2l instruction is type safe if one can validly pop int off the incoming operand stack and replace it with long, yielding the outgoing type state.
instructionIsTypeSafe(i2l, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int], long,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An i2s instruction is type safe iff the equivalent ineg instruction is type safe.
instructionHasEquivalentTypeRule(i2s, ineg).
An iadd instruction is type safe iff one can validly replace types matching int and int on the incoming operand stack with int yielding the outgoing type state.
instructionIsTypeSafe(iadd, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int, int], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An iaload instruction is type safe iff one can validly replace types matching int and array of int on the incoming operand stack with int yielding the outgoing type state.
instructionIsTypeSafe(iaload, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int, arrayOf(int)], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An iand instruction is type safe iff the equivalent iadd instruction is type safe.
instructionHasEquivalentTypeRule(iand, iadd).
An iastore instruction is type safe iff one can validly pop types matching int, int and array of int off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(iastore, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [int, int, arrayOf(int)], NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An if_acmpeq instruction is type safe iff one can validly pop types matching reference and reference on the incoming operand stack yielding the outgoing type state NextStackFrame, and the operand of the instruction, Target, is a valid branch target assuming an incoming type state of NextStackFrame.
instructionIsTypeSafe(if_acmpeq(Target), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [reference, reference], NextStackFrame),
targetIsTypeSafe(Environment, NextStackFrame, Target),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The rule for if_acmpne is identical.
instructionHasEquivalentTypeRule(if_acmpne(Target), if_acmpeq(Target)).
An if_icmpeq instruction is type safe iff one can validly pop types matching int and int on the incoming operand stack yielding the outgoing type state NextStackFrame, and the operand of the instruction, Target, is a valid branch target assuming an incoming type state of NextStackFrame.
instructionIsTypeSafe(if_icmpeq(Target), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [int, int], NextStackFrame),
targetIsTypeSafe(Environment, NextStackFrame, Target),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The rules for all other variants of the if_icmp<cond> instruction are identical.
instructionHasEquivalentTypeRule(if_icmpge(Target), if_icmpeq(Target)). instructionHasEquivalentTypeRule(if_icmpgt(Target), if_icmpeq(Target)). instructionHasEquivalentTypeRule(if_icmple(Target), if_icmpeq(Target)). instructionHasEquivalentTypeRule(if_icmplt(Target), if_icmpeq(Target)). instructionHasEquivalentTypeRule(if_icmpne(Target), if_icmpeq(Target)).
An ifeq instruction is type safe iff one can validly pop a type matching int off the incoming operand stack yielding the outgoing type state NextStackFrame, and the operand of the instruction, Target, is a valid branch target assuming an incoming type state of NextStackFrame.
instructionIsTypeSafe(ifeq(Target), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [int], NextStackFrame),
targetIsTypeSafe(Environment, NextStackFrame, Target),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The rules for all other variations of the if<cond> instruction are identical.
instructionHasEquivalentTypeRule(ifge(Target), ifeq(Target)). instructionHasEquivalentTypeRule(ifgt(Target), ifeq(Target)). instructionHasEquivalentTypeRule(ifle(Target), ifeq(Target)). instructionHasEquivalentTypeRule(iflt(Target), ifeq(Target)). instructionHasEquivalentTypeRule(ifne(Target), ifeq(Target)).
An ifnonnull instruction is type safe iff one can validly pop a type matching reference off the incoming operand stack yielding the outgoing type state NextStackFrame, and the operand of the instruction, Target, is a valid branch target assuming an incoming type state of NextStackFrame.
instructionIsTypeSafe(ifnonnull(Target), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [reference], NextStackFrame),
targetIsTypeSafe(Environment, NextStackFrame, Target),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An ifnull instruction is type safe iff the equivalent ifnonnull instruction is type safe.
instructionHasEquivalentTypeRule(ifnull(Target), ifnonnull(Target)).
An iinc instruction with first operand Index is type safe iff LIndex has type int. The iinc instruction does not change the type state.
instructionIsTypeSafe(iinc(Index, _Value), _Environment, _Offset,
StackFrame, StackFrame, ExceptionStackFrame) :-
StackFrame = frame(Locals, _OperandStack, _Flags),
nth0(Index, Locals, int),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An iload instruction with operand Index is type safe and yields an outgoing type state NextStackFrame, if a load instruction with operand Index and type int is type safe and yields an outgoing type state NextStackFrame.
instructionIsTypeSafe(iload(Index), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
loadIsTypeSafe(Environment, Index, int, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The instructions iload_<n>, for 0 ≤ n ≤ 3, are typesafe iff the equivalent iload instruction is type safe.
instructionHasEquivalentTypeRule(iload_0, iload(0)). instructionHasEquivalentTypeRule(iload_1, iload(1)). instructionHasEquivalentTypeRule(iload_2, iload(2)). instructionHasEquivalentTypeRule(iload_3, iload(3)).
An imul instruction is type safe iff the equivalent iadd instruction is type safe.
instructionHasEquivalentTypeRule(imul, iadd).
An ineg instruction is type safe iff there is a type matching int on the incoming operand stack. The ineg instruction does not alter the type state.
instructionIsTypeSafe(ineg, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int], int, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
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).
An invokedynamic instruction is type safe iff all of the following are true:
Its first operand, CP, refers to a constant pool entry denoting an dynamic call site with name CallSiteName with descriptor Descriptor.
One can validly replace types matching the argument types given in Descriptor on the incoming operand stack with the return type given in Descriptor, yielding the outgoing type state.
instructionIsTypeSafe(invokedynamic(CP,0,0), Environment, _Offset,
StackFrame, NextStackFrame, ExceptionStackFrame) :-
CP = dmethod(CallSiteName, Descriptor),
CallSiteName \= '<init>',
CallSiteName \= '<clinit>',
parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
reverse(OperandArgList, StackArgList),
validTypeTransition(Environment, StackArgList, ReturnType,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An invokeinterface instruction is type safe iff all of the following are true:
Its first operand, CP, refers to a constant pool entry denoting an interface method named MethodName with descriptor Descriptor that is a member of an interface MethodIntfName.
Its second operand, Count, is a valid count operand (see below).
One can validly replace types matching the type MethodIntfName and the argument types given in Descriptor on the incoming operand stack with the return type given in Descriptor, yielding the outgoing type state.
instructionIsTypeSafe(invokeinterface(CP, Count, 0), Environment, _Offset,
StackFrame, NextStackFrame, ExceptionStackFrame) :-
CP = imethod(MethodIntfName, MethodName, Descriptor),
MethodName \= '<init>',
MethodName \= '<clinit>',
parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
currentClassLoader(Environment, CurrentLoader),
reverse([class(MethodIntfName, CurrentLoader) | OperandArgList],
StackArgList),
canPop(StackFrame, StackArgList, TempFrame),
validTypeTransition(Environment, [], ReturnType, TempFrame, NextStackFrame),
countIsValid(Count, StackFrame, TempFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
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.
An invokespecial instruction is type safe iff all of the following are true:
Its first operand, CP, refers to a constant pool entry denoting a method named MethodName with descriptor Descriptor that is a member of a class MethodClassName.
One can validly replace types matching the current class and the argument types given in Descriptor on the incoming operand stack with the return type given in Descriptor, yielding the outgoing type state.
One can validly replace types matching the class MethodClassName and the argument types given in Descriptor on the incoming operand stack with the return type given in Descriptor.
instructionIsTypeSafe(invokespecial(CP), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
CP = method(MethodClassName, MethodName, Descriptor),
MethodName \= '<init>',
MethodName \= '<clinit>',
parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
thisClass(Environment, class(CurrentClassName, CurrentLoader)),
reverse([class(CurrentClassName, CurrentLoader) | OperandArgList],
StackArgList),
validTypeTransition(Environment, StackArgList, ReturnType,
StackFrame, NextStackFrame),
reverse([class(MethodClassName, CurrentLoader) | OperandArgList],
StackArgList2),
validTypeTransition(Environment, StackArgList2, ReturnType,
StackFrame, _ResultStackFrame),
isAssignable(class(CurrentClassName, CurrentLoader),
class(MethodClassName, CurrentLoader)).
exceptionStackFrame(StackFrame, ExceptionStackFrame).
One can validly pop types matching the argument types given in Descriptor and an uninitialized type, UninitializedArg, off the incoming operand stack, yielding OperandStack.
The outgoing type state is derived from the incoming type state by first replacing the incoming operand stack with OperandStack and then replacing all instances of UninitializedArg with the type of instance being initialized.
instructionIsTypeSafe(invokespecial(CP), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
CP = method(MethodClassName, '<init>', Descriptor),
parseMethodDescriptor(Descriptor, OperandArgList, void),
reverse(OperandArgList, StackArgList),
canPop(StackFrame, StackArgList, TempFrame),
TempFrame = frame(Locals, FullOperandStack, Flags),
FullOperandStack = [UninitializedArg | OperandStack],
currentClassLoader(Environment, CurrentLoader),
rewrittenUninitializedType(UninitializedArg, Environment,
class(MethodClassName, CurrentLoader), This),
rewrittenInitializationFlags(UninitializedArg, Flags, NextFlags),
substitute(UninitializedArg, This, OperandStack, NextOperandStack),
substitute(UninitializedArg, This, Locals, NextLocals),
NextStackFrame = frame(NextLocals, NextOperandStack, NextFlags),
ExceptionStackFrame = frame(Locals, [], Flags),
passesProtectedCheck(Environment, MethodClassName, '<init>',
Descriptor, NextStackFrame).
To compute what type the uninitialized argument's type needs to be rewritten to, there are two cases:
If we are initializing an object within its constructor, its type is initially uninitializedThis. This type will be rewritten to the type of the class of the <init> method.
The second case arises from initialization of an object created by new. The uninitialized arg type is rewritten to MethodClass, the type of the method holder of <init>. We check whether there really is a new instruction at Address.
rewrittenUninitializedType(uninitializedThis, Environment,
MethodClass, MethodClass) :-
MethodClass = class(MethodClassName, CurrentLoader),
thisClass(Environment, MethodClass).
rewrittenUninitializedType(uninitializedThis, Environment,
MethodClass, MethodClass) :-
MethodClass = class(MethodClassName, CurrentLoader),
thisClass(Environment, class(thisClassName, thisLoader)),
superclassChain(thisClassName, thisLoader, [MethodClass | Rest]).
rewrittenUninitializedType(uninitialized(Address), Environment,
MethodClass, MethodClass) :-
allInstructions(Environment, Instructions),
member(instruction(Address, new(MethodClass)), 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.
An invokestatic instruction is type safe iff all of the following are true:
Its first operand, CP, refers to a constant pool entry denoting a method named MethodName with descriptor Descriptor.
One can validly replace types matching the argument types given in Descriptor on the incoming operand stack with the return type given in Descriptor, yielding the outgoing type state.
instructionIsTypeSafe(invokestatic(CP), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
CP = method(_MethodClassName, MethodName, Descriptor),
MethodName \= '<init>',
MethodName \= '<clinit>',
parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
reverse(OperandArgList, StackArgList),
validTypeTransition(Environment, StackArgList, ReturnType,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An invokevirtual instruction is type safe iff all of the following are true:
Its first operand, CP, refers to a constant pool entry denoting a method named MethodName with descriptor Descriptor that is a member of a class MethodClassName.
One can validly replace types matching the class MethodClassName and the argument types given in Descriptor on the incoming operand stack with the return type given in Descriptor, yielding the outgoing type state.
If the method is protected, the usage conforms to the special rules governing access to protected members (§4.10.1.8).
instructionIsTypeSafe(invokevirtual(CP), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
CP = method(MethodClassName, MethodName, Descriptor),
MethodName \= '<init>',
MethodName \= '<clinit>',
parseMethodDescriptor(Descriptor, OperandArgList, ReturnType),
reverse(OperandArgList, ArgList),
currentClassLoader(Environment, CurrentLoader),
reverse([class(MethodClassName, CurrentLoader) | OperandArgList],
StackArgList),
validTypeTransition(Environment, StackArgList, ReturnType,
StackFrame, NextStackFrame),
canPop(StackFrame, ArgList, PoppedFrame),
passesProtectedCheck(Environment, MethodClassName, MethodName,
Descriptor, PoppedFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An ior instruction is type safe iff the equivalent iadd instruction is type safe.
instructionHasEquivalentTypeRule(ior, iadd).
An irem instruction is type safe iff the equivalent iadd instruction is type safe.
instructionHasEquivalentTypeRule(irem, iadd).
An ireturn instruction is type safe if the enclosing method has a declared return type of int, and one can validly pop a type matching int off the incoming operand stack.
instructionIsTypeSafe(ireturn, Environment, _Offset, StackFrame,
afterGoto, ExceptionStackFrame) :-
thisMethodReturnType(Environment, int),
canPop(StackFrame, [int], _PoppedStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An ishl instruction is type safe iff the equivalent iadd instruction is type safe.
instructionHasEquivalentTypeRule(ishl, iadd).
An ishr instruction is type safe iff the equivalent iadd instruction is type safe.
instructionHasEquivalentTypeRule(ishr, iadd).
An iushr instruction is type safe iff the equivalent iadd instruction is type safe.
instructionHasEquivalentTypeRule(iushr, iadd).
An istore instruction with operand Index is type safe and yields an outgoing type state NextStackFrame, if a store instruction with operand Index and type int is type safe and yields an outgoing type state NextStackFrame.
instructionIsTypeSafe(istore(Index), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
storeIsTypeSafe(Environment, Index, int, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The instructions istore_<n>, for 0 ≤ n ≤ 3, are type safe iff the equivalent istore instruction is type safe.
instructionHasEquivalentTypeRule(istore_0, istore(0)). instructionHasEquivalentTypeRule(istore_1, istore(1)). instructionHasEquivalentTypeRule(istore_2, istore(2)). instructionHasEquivalentTypeRule(istore_3, istore(3)).
An isub instruction is type safe iff the equivalent iadd instruction is type safe.
instructionHasEquivalentTypeRule(isub, iadd).
An ixor instruction is type safe iff the equivalent iadd instruction is type safe.
instructionHasEquivalentTypeRule(ixor, iadd).
An l2d instruction is type safe if one can validly pop long off the incoming operand stack and replace it with double, yielding the outgoing type state.
instructionIsTypeSafe(l2d, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [long], double,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An l2f instruction is type safe if one can validly pop long off the incoming operand stack and replace it with float, yielding the outgoing type state.
instructionIsTypeSafe(l2f, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [long], float,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An l2i instruction is type safe if one can validly pop long off the incoming operand stack and replace it with int, yielding the outgoing type state.
instructionIsTypeSafe(l2i, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [long], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An ladd instruction is type safe iff one can validly replace types matching long and long on the incoming operand stack with long yielding the outgoing type state.
instructionIsTypeSafe(ladd, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [long, long], long,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An laload instruction is type safe iff one can validly replace types matching int and array of long on the incoming operand stack with long yielding the outgoing type state.
instructionIsTypeSafe(laload, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int, arrayOf(long)], long,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An land instruction is type safe iff the equivalent ladd instruction is type safe.
instructionHasEquivalentTypeRule(land, ladd).
An lastore instruction is type safe iff one can validly pop types matching long, int and array of long off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(lastore, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [long, int, arrayOf(long)], NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A lcmp instruction is type safe iff one can validly replace types matching long and long on the incoming operand stack with int yielding the outgoing type state.
instructionIsTypeSafe(lcmp, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [long, long], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An lconst_0 instruction is type safe if one can validly push the type long onto the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(lconst_0, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [], long, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An lconst_1 instruction is type safe iff the equivalent lconst_0 instruction is type safe.
instructionHasEquivalentTypeRule(lconst_1, lconst_0).
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 either int, float, String, Class, java.lang.invoke.MethodType, or java.lang.invoke.MethodHandle, and one can validly push Type onto the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(ldc(CP), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
functor(CP, Tag, _),
isBootstrapLoader(BL),
member([Tag, Type], [
[int, int],
[float, float],
[string, class('java/lang/String', BL)],
[classConst, class('java/lang/Class', BL)],
[methodTypeConst, class('java/lang/invoke/MethodType', BL)],
[methodHandleConst, class('java/lang/invoke/MethodHandle', BL)],
]),
validTypeTransition(Environment, [], Type, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An ldc_w instruction is type safe iff the equivalent ldc instruction is type safe.
instructionHasEquivalentTypeRule(ldc_w(CP), ldc(CP))
An ldc2_w instruction with operand CP is type safe iff CP refers to a constant pool entry denoting an entity of type Tag, where Tag is either long or double, and one can validly push Tag onto the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(ldc2_w(CP), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
functor(CP, Tag, _),
member(Tag, [long, double]),
validTypeTransition(Environment, [], Tag, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An ldiv instruction is type safe iff the equivalent ladd instruction is type safe.
instructionHasEquivalentTypeRule(ldiv, ladd).
An lload instruction with operand Index is type safe and yields an outgoing type state NextStackFrame, if a load instruction with operand Index and type long is type safe and yields an outgoing type state NextStackFrame.
instructionIsTypeSafe(lload(Index), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
loadIsTypeSafe(Environment, Index, long, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The instructions lload_<n>, for 0 ≤ n ≤ 3, are type safe iff the equivalent lload instruction is type safe.
instructionHasEquivalentTypeRule(lload_0, lload(0)). instructionHasEquivalentTypeRule(lload_1, lload(1)). instructionHasEquivalentTypeRule(lload_2, lload(2)). instructionHasEquivalentTypeRule(lload_3, lload(3)).
An lmul instruction is type safe iff the equivalent ladd instruction is type safe.
instructionHasEquivalentTypeRule(lmul, ladd).
An lneg instruction is type safe iff there is a type matching long on the incoming operand stack. The lneg instruction does not alter the type state.
instructionIsTypeSafe(lneg, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [long], long,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
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).
A lor instruction is type safe iff the equivalent ladd instruction is type safe.
instructionHasEquivalentTypeRule(lor, ladd).
An lrem instruction is type safe iff the equivalent ladd instruction is type safe.
instructionHasEquivalentTypeRule(lrem, ladd).
An lreturn instruction is type safe if the enclosing method has a declared return type of long, and one can validly pop a type matching long off the incoming operand stack.
instructionIsTypeSafe(lreturn, Environment, _Offset, StackFrame,
afterGoto, ExceptionStackFrame) :-
thisMethodReturnType(Environment, long),
canPop(StackFrame, [long], _PoppedStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An lshl instruction is type safe if one can validly replace the types int and long on the incoming operand stack with the type long yielding the outgoing type state.
instructionIsTypeSafe(lshl, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int, long], long,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An lshr instruction is type safe iff the equivalent lshl instruction is type safe.
instructionHasEquivalentTypeRule(lshr, lshl).
An lushr instruction is type safe iff the equivalent lshl instruction is type safe.
instructionHasEquivalentTypeRule(lushr, lshl).
An lstore instruction with operand Index is type safe and yields an outgoing type state NextStackFrame, if a store instruction with operand Index and type long is type safe and yields an outgoing type state NextStackFrame.
instructionIsTypeSafe(lstore(Index), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
storeIsTypeSafe(Environment, Index, long, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The instructions lstore_<n>, for 0 ≤ n ≤ 3, are type safe iff the equivalent lstore instruction is type safe.
instructionHasEquivalentTypeRule(lstore_0, lstore(0)). instructionHasEquivalentTypeRule(lstore_1, lstore(1)). instructionHasEquivalentTypeRule(lstore_2, lstore(2)). instructionHasEquivalentTypeRule(lstore_3, lstore(3)).
An lsub instruction is type safe iff the equivalent ladd instruction is type safe.
instructionHasEquivalentTypeRule(lsub, ladd).
An lxor instruction is type safe iff the equivalent ladd instruction is type safe.
instructionHasEquivalentTypeRule(lxor, ladd).
A monitorenter instruction is type safe iff one can validly pop a type matching reference off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(monitorenter, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [reference], NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A monitorexit instruction is type safe iff the equivalent monitorenter instruction is type safe.
instructionHasEquivalentTypeRule(monitorexit, monitorenter).
A multianewarray instruction with operands CP and Dim is type safe iff CP refers to a constant pool entry denoting an array type whose dimension is greater or equal to Dim, Dim is strictly positive, and one can validly replace Dim int types on the incoming operand stack with the type denoted by CP yielding the outgoing type state.
instructionIsTypeSafe(multianewarray(CP, Dim), Environment, _Offset,
StackFrame, NextStackFrame, ExceptionStackFrame) :-
CP = arrayOf(_),
classDimension(CP, Dimension),
Dimension >= Dim,
Dim > 0,
/* Make a list of Dim ints */
findall(int, between(1, Dim, _), IntList),
validTypeTransition(Environment, IntList, CP,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The dimension of an array type whose component type is also an array type is one more than the dimension of its component type.
classDimension(arrayOf(X), Dimension) :-
classDimension(X, Dimension1),
Dimension is Dimension1 + 1.
classDimension(_, Dimension) :-
Dimension = 0.
A new instruction with operand CP at offset Offset is type safe iff CP refers to a constant pool entry denoting a class 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 (§invokespecial).
A newarray instruction with operand TypeCode is type safe iff TypeCode corresponds to the primitive type ElementType, and one can validly replace the type int on the incoming operand stack with the type 'array of ElementType', yielding the outgoing type state.
instructionIsTypeSafe(newarray(TypeCode), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
primitiveArrayInfo(TypeCode, _TypeChar, ElementType, _VerifierType),
validTypeTransition(Environment, [int], arrayOf(ElementType),
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
The correspondence between type codes and primitive types is specified by the following predicate:
primitiveArrayInfo(4, 0'Z, boolean, int). primitiveArrayInfo(5, 0'C, char, int). primitiveArrayInfo(6, 0'F, float, float). primitiveArrayInfo(7, 0'D, double, double). primitiveArrayInfo(8, 0'B, byte, int). primitiveArrayInfo(9, 0'S, short, int). primitiveArrayInfo(10, 0'I, int, int). primitiveArrayInfo(11, 0'J, long, long).
A nop instruction is always type safe. The nop instruction does not affect the type state.
instructionIsTypeSafe(nop, _Environment, _Offset, StackFrame,
StackFrame, ExceptionStackFrame) :-
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A pop instruction is type safe iff one can validly pop a category 1 type off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(pop, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
StackFrame = frame(Locals, [Type | Rest], Flags),
Type \= top,
sizeOf(Type, 1),
NextStackFrame = frame(Locals, Rest, Flags),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A pop2 instruction is type safe iff it is a type safe form of the pop2 instruction.
instructionIsTypeSafe(pop2, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
StackFrame = frame(Locals, InputOperandStack, Flags),
pop2SomeFormIsTypeSafe(InputOperandStack, OutputOperandStack),
NextStackFrame = frame(Locals, OutputOperandStack, Flags),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A pop2 instruction is a type safe form of the pop2 instruction iff it is a type safe form 1 pop2 instruction or a type safe form 2 pop2 instruction.
pop2SomeFormIsTypeSafe(InputOperandStack, OutputOperandStack) :-
pop2Form1IsTypeSafe(InputOperandStack, OutputOperandStack).
pop2SomeFormIsTypeSafe(InputOperandStack, OutputOperandStack) :-
pop2Form2IsTypeSafe(InputOperandStack, OutputOperandStack).
A pop2 instruction is a type safe form 1 pop2 instruction iff one can validly pop two types of size 1 off the incoming operand stack yielding the outgoing type state.
pop2Form1IsTypeSafe([Type1, Type2 | Rest], Rest) :-
sizeOf(Type1, 1),
sizeOf(Type2, 1).
A pop2 instruction is a type safe form 2 pop2 instruction iff one can validly pop a type of size 2 off the incoming operand stack yielding the outgoing type state.
pop2Form2IsTypeSafe([top, Type | Rest], Rest) :- sizeOf(Type, 2).
A putfield 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 FieldClass, and one can validly pop types matching FieldType and FieldClass off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(putfield(CP), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
CP = field(FieldClass, FieldName, FieldDescriptor),
parseFieldDescriptor(FieldDescriptor, FieldType),
canPop(StackFrame, [FieldType], PoppedFrame),
passesProtectedCheck(Environment, FieldClass, FieldName,
FieldDescriptor, PoppedFrame),
currentClassLoader(Environment, CurrentLoader),
canPop(StackFrame, [FieldType, class(FieldClass, CurrentLoader)],
NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
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(_FieldClass, _FieldName, FieldDescriptor),
parseFieldDescriptor(FieldDescriptor, FieldType),
canPop(StackFrame, [FieldType], NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A return instruction is type safe if the enclosing method declares a void return type, and either:
instructionIsTypeSafe(return, Environment, _Offset, StackFrame,
afterGoto, ExceptionStackFrame) :-
thisMethodReturnType(Environment, void),
StackFrame = frame(_Locals, _OperandStack, Flags),
notMember(flagThisUninit, Flags),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An saload instruction is type safe iff one can validly replace types matching int and array of short on the incoming operand stack with int yielding the outgoing type state.
instructionIsTypeSafe(saload, Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [int, arrayOf(short)], int,
StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An sastore instruction is type safe iff one can validly pop types matching int, int, and array of short off the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(sastore, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
canPop(StackFrame, [int, int, arrayOf(short)], NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
An sipush instruction is type safe iff one can validly push the type int onto the incoming operand stack yielding the outgoing type state.
instructionIsTypeSafe(sipush(_Value), Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
validTypeTransition(Environment, [], int, StackFrame, NextStackFrame),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
A swap instruction is type safe iff one can validly replace two category 1 types, Type1 and Type2, on the incoming operand stack with the types Type2 and Type1 yielding the outgoing type state.
instructionIsTypeSafe(swap, _Environment, _Offset, StackFrame,
NextStackFrame, ExceptionStackFrame) :-
StackFrame = frame(_Locals, [Type1, Type2 | Rest], _Flags),
sizeOf(Type1, 1),
sizeOf(Type2, 1),
NextStackFrame = frame(_Locals, [Type2, Type1 | Rest], _Flags),
exceptionStackFrame(StackFrame, ExceptionStackFrame).
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 wide instructions follow the same rules as the instructions they widen.
instructionHasEquivalentTypeRule(wide(WidenedInstruction),
WidenedInstruction).
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.3