Структура element_value — это различающееся объединение, представляющее значение пары «элемент-значение». Она используется для представления значений элементов во всех атрибутах, описывающих аннотации (RuntimeVisibleAnnotations, RuntimeInvisibleAnnotations, RuntimeVisibleParameterAnnotations и RuntimeInvisibleParameterAnnotations).

Структура element_value имеет следующий формат:

element_value {
    u1 tag;
    union {
        u2 const_value_index;

        {   u2 type_name_index;
            u2 const_name_index;
        } enum_const_value;

        u2 class_info_index;

        annotation annotation_value;

        {   u2            num_values;
            element_value values[num_values];
        } array_value;
    } value;
}

Элементы структуры element_value следующие:

Мы постулируем существование 22 предикат Prolog («аксессоров»), которые обладают определённым ожидаемым поведением, но формальные определения которых не приводятся в данном спецификации.

При проверке типа тела метода удобно обращаться к информации о методе. Для этой цели мы определяем среду — шестёрку, состоящую из:

Мы определяем аксессоры для извлечения информации из среды.

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

Мы определяем дополнительные предикаты для извлечения информации более высокого уровня из среды.

offsetStackFrame(Environment, Offset, StackFrame) :-
    allInstructions(Environment, Instructions),
    member(stackMap(Offset, StackFrame), Instructions).

currentClassLoader(Environment, Loader) :-
    thisClass(Environment, class(_, Loader)).

Наконец, мы определяем общий предикат, используемый во всех правилах типов:

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

Принцип, определяющий, какие аксессоры постулируются, а какие полностью специфицируются, заключается в том, чтобы не переопределять представление файла class. Предоставление конкретных аксессоров для термина Class или Method заставило бы нас полностью определить формат термина Prolog, представляющего файл class.

Проверяющий тип использует систему типов, основанную на иерархии типов проверки, проиллюстрированной ниже.

Большинство типов проверки имеют непосредственное соответствие с типами, представленными дескрипторами полей (§4.3.2) в таблице 4.2. Исключение составляют дескрипторы полей B, C, S и Z, все из которых соответствуют типу проверки int.

Verification type hierarchy:

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

Подтипизация рефлексивна.

isAssignable(X, X).

Типы проверки, которые не являются ссылочными типами в языке программирования Java, имеют правила подтипизации следующего вида:

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

То есть, v является подтипом X, если непосредственный супертип v является подтипом X. Правила следующие:

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

Эти правила подтипизации не обязательно являются наиболее очевидной формулировкой подтипизации. Существует явное разделение между правилами подтипизации для ссылочных типов в языке программирования Java и правилами для остальных типов проверки. Разделение позволяет нам устанавливать общие отношения подтипизации между ссылочными типами языка программирования Java и другими типами проверки. Эти отношения сохраняются независимо от положения ссылочного типа Java в иерархии типов и помогают предотвратить избыточную загрузку классов реализацией виртуальной машины Java. Например, мы не хотим начинать подниматься по иерархии суперклассов Java в ответ на запрос вида class(foo, L) <: twoWord.

У нас также есть правило, утверждающее, что подтипизация рефлексивна, так что вместе эти правила охватывают большинство типов проверки, которые не являются ссылочными типами в языке программирования Java.

Правила подтипизации для ссылочных типов в языке программирования Java определяются рекурсивно с помощью 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)).

При присваивании интерфейсы обрабатываются как Object.

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

isJavaAssignable(From, To) :-
    isJavaSubclassOf(From, To).

Типы массивов являются подтипами Object. Цель также состоит в том, чтобы типы массивов являлись подтипами Cloneable и 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).

Подтипизация между массивами примитивных типов — это отношение тождества.

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

Подтипизация между массивами ссылочных типов ковариантна.

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

Наследование рефлексивно.

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

Индивидуальные инструкции байткода представляются в Прологе в виде термов, функтор которых является именем инструкции, а аргументы — её распарсенными операндами.

Например, инструкция aload представлена в виде терма aload(N), который включает индекс N, являющийся операндом инструкции.

Инструкции в целом представляются в виде списка термов следующего формата:

instruction(Offset, AnInstruction)

Например, instruction(21, aload(1)).

Порядок инструкций в этом списке должен совпадать с порядком в файле class.

Несколько инструкций имеют операнды, являющиеся записями пула констант, представляющими поля, методы и динамические места вызова. В пуле констант поле представлено структурой CONSTANT_Fieldref_info, метод — структурой CONSTANT_InterfaceMethodref_info (для метода интерфейса) или структурой CONSTANT_Methodref_info (для метода класса), а динамическое место вызова — структурой CONSTANT_InvokeDynamic_info (§4.4.2, §4.4.10). Такие структуры представляются как применения функтора в виде:

Для ясности мы предполагаем, что описатели полей и методов (§4.3.2) отображаются на более читаемые имена: начальные L и конечные ; удаляются из имён классов, а символы BaseType, используемые для примитивных типов, отображаются на имена этих типов.

Например, инструкция getfield, операндом которой был индекс в пуле констант, ссылающийся на поле foo типа F в классе Bar, будет представлена как getfield(field('Bar', 'foo', 'F')).

Записи пула констант, которые ссылаются на константные значения, такие как CONSTANT_String, CONSTANT_Integer, CONSTANT_Float, CONSTANT_Long, CONSTANT_Double и CONSTANT_Class, кодируются с помощью функторов с именами string, int, float, long, double и classConstant соответственно.

Например, инструкция ldc для загрузки целого числа 91 будет закодирована как ldc(int(91)).

Кадры карты стека представляются в Прологе в виде списка терминов следующего вида:

stackMap(Offset, TypeState)

где Offset — целое число, указывающее смещение инструкции, к которой относится кадр карты, а TypeState — ожидаемое состояние входного типа (§4.7.4) для этой инструкции.

Порядок кадров карты стека в этом списке должен совпадать с порядком в файле class.

TypeState имеет вид:

frame(Locals, OperandStack, Flags)

где:

Подтипирование (§4.10.1.2) распространяется точечно на состояния типов.

Массив локальных переменных метода имеет фиксированную длину по построению (см. methodInitialStackFrame в §4.10.1.6), в то время как стек операндов увеличивается и уменьшается. Поэтому нам нужна явная проверка длины стеков операндов, применимость которых требуется.

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

Длина стека операндов не должна превышать объявленную максимальную длину стека.

operandStackHasLegalLength(Environment, OperandStack) :-
    length(OperandStack, Length),
    maxOperandStackLength(Environment, MaxStack),
    Length =< MaxStack.

Некоторые инструкции для массивов (§aaload, §arraylength, §baload, §bastore) проверяют типы значений в стеке операндов на предмет того, являются ли они типами массивов. Следующее предложение обращается к I-му элементу стека операндов из состояния типа.

nth1OperandStackIs(I, frame(_Locals, OperandStack, _Flags), Element) :-
    nth1(I, OperandStack, Element).

Обработка стека операндов инструкциями загрузки и сохранения (§4.10.1.7) усложняется тем, что некоторые типы занимают две ячейки в стеке. Приведённые ниже предикаты учитывают это, позволяя остальной части спецификации абстрагироваться от этой проблемы.

Извлечь из стека список типов.

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

Извлечь из стека отдельный тип. Точнее, если логическая вершина стека — это подтип указанного типа, 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).

Поместить логический тип на стек. Точное поведение зависит от размера типа. Если помещаемый тип имеет размер 1, мы просто помещаем его на стек. Если помещаемый тип имеет размер 2, мы помещаем его, а затем помещаем top.

pushOperandStack(OperandStack, 'void', OperandStack).
pushOperandStack(OperandStack, Type, [Type | OperandStack]) :-
    sizeOf(Type, 1).
pushOperandStack(OperandStack, Type, [top, Type | OperandStack]) :-
    sizeOf(Type, 2).

Поместить список типов на стек, если есть место.

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

Обработка стека операндов инструкциями dup полностью определяется категорией типов для значений на стеке (§2.11.1).

Типы категории 1 занимают одну ячейку стека. Извлечение логического типа категории 1, Type, из стека возможно, если вершина стека — Type, и Type не равно top (иначе это может обозначать верхнюю половину типа категории 2). Результатом является входной стек, с извлечённой верхней ячейкой.

popCategory1([Type | Rest], Type, Rest) :-
    Type \= top,
    sizeOf(Type, 1).

Типы категории 2 занимают две ячейки стека. Извлечение логического типа категории 2, Type, из стека возможно, если вершина стека — тип top, а ячейка непосредственно под ней — Type. Результатом является входной стек, с извлечёнными двумя верхними ячейками.

popCategory2([top, Type | Rest], Type, Rest) :-
    sizeOf(Type, 2).

Большинство правил типов для отдельных инструкций (§4.10.1.9) зависят от понятия допустимого перехода типов. Переход типов допустим, если можно извлечь список ожидаемых типов из стека операндов состояния входного типа и заменить их ожидаемым типом результата, получив новое допустимое состояние типа. В частности, размер стека операндов в новом состоянии типа не должен превышать его максимального объявленного размера.

validTypeTransition(Environment, ExpectedTypesOnStack, ResultType,
                    frame(Locals, InputOperandStack, Flags),
                    frame(Locals, NextOperandStack, Flags)) :-
    popMatchingList(InputOperandStack, ExpectedTypesOnStack,
                    InterimOperandStack),
    pushOperandStack(InterimOperandStack, ResultType, NextOperandStack),
    operandStackHasLegalLength(Environment, NextOperandStack).

Абстрактные и нативные методы считаются типобезопасными, если они не переопределяют финальный метод.

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

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

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

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

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

finalMethodNotOverridden(Method, Superclass, MethodList) :-
    methodName(Method, Name),
    methodDescriptor(Method, Descriptor),
    notMember(method(_, Name, Descriptor), MethodList),
    doesNotOverrideFinalMethod(Superclass, Method).

Неабстрактные, неродные методы являются корректными с точки зрения типов, если они имеют код, и этот код корректен с точки зрения типов.

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

Метод с кодом является типобезопасным, если возможно объединить код и кадры карты стека в один поток таким образом, что каждый кадр карты стека предшествует инструкции, которой он соответствует, и объединенный поток корректен с точки зрения типов. Обработчики исключений метода, если они есть, также должны быть допустимыми.

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

Рассмотрим сначала обработчики исключений.

Обработчик исключений представлен применением функтора в форме:

handler(Start, End, Target, ClassName)

где аргументы, соответственно, представляют собой начало и конец диапазона инструкций, покрываемого обработчиком, первую инструкцию кода обработчика и имя класса исключения, для обработки которого предназначен данный обработчик.

Обработчик исключений является допустимым, если его начало (Start) меньше его конца (End), существует инструкция, смещение которой равно Start, существует инструкция, смещение которой равно End, и класс исключения обработчика может быть присвоен классу Throwable. Класс исключения обработчика является Throwable, если запись класса обработчика равна 0, в противном случае это класс, указанный в обработчике.

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

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.

Теперь перейдем к потоку инструкций и кадрам карты стека.

Объединение инструкций и кадров карты стека в один поток включает четыре случая:

Чтобы определить, является ли объединенный поток для метода корректным с точки зрения типов, мы сначала выводим начальное состояние типа метода.

Начальное состояние типа метода состоит из пустого стека операндов и типов локальных переменных, полученных из типа this и аргументов, а также соответствующего флага, в зависимости от того, является ли это <init> методом.

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

Учитывая список типов, следующее предложение создает список, где каждый тип размера 2 заменяется двумя записями: одной для самого типа и одной top записью. Результат затем соответствует представлению списка в виде 32-битовых слов в виртуальной машине Java.

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

Для начального состояния типа метода экземпляра мы вычисляем тип this и помещаем его в список. Тип this в методе <init> класса Object равен Object; в других <init> методах тип this равен uninitializedThis; в противном случае, тип this в методе экземпляра равен class(N, L), где N — имя класса, содержащего метод, а L — его определяющий загрузчик классов.

Для начального состояния типа статического метода this не имеет значения, поэтому список пуст.

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

Теперь мы вычислим, является ли объединенный поток для метода корректным с точки зрения типов, используя начальное состояние типа метода:

Переход к целевому адресу является безопасным с точки зрения типов, если у целевого адреса есть связанный кадр карты стека, Frame, и текущий кадр карты стека, StackFrame, может быть присвоен Frame.

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

Инструкция удовлетворяет своим обработчикам исключений, если она удовлетворяет каждому применимому обработчику исключений.

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

Обработчик исключений является применимым к инструкции, если смещение инструкции больше или равно началу диапазона обработчика и меньше конца диапазона обработчика.

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

Инструкция удовлетворяет обработчику исключений, если ее входное состояние типа является StackFrame, и целевой адрес обработчика (начальная инструкция кода обработчика) является типобезопасной, предполагая входное состояние типа T. Состояние типа T получено из StackFrame путем замены стека операндов стеком, единственным элементом которого является класс исключения обработчика.

instructionSatisfiesHandler(Environment, StackFrame, Handler) :-
    Handler = handler(_, _, Target, _),
    currentClassLoader(Environment, CurrentLoader),
    handlerExceptionClass(Handler, ExceptionClass, CurrentLoader), 
    /* The stack consists of just the exception. */
    StackFrame = frame(Locals, _, Flags),
    ExcStackFrame = frame(Locals, [ ExceptionClass ], Flags),
    operandStackHasLegalLength(Environment, ExcStackFrame),
    targetIsTypeSafe(Environment, ExcStackFrame, Target).

Все инструкции загрузки являются вариациями общей схемы, отличаясь типом значения, которое загружает инструкция.

Загрузка значения типа Type из локальной переменной Index безопасна по типу, если тип этой локальной переменной является ActualType, ActualType присваиваемо Type, и помещение ActualType на входной стек операндов — это допустимый переход типов (§4.10.1.4), который приводит к новому состоянию типа NextStackFrame. После выполнения инструкции загрузки состояние типа будет NextStackFrame.

loadIsTypeSafe(Environment, Index, Type, StackFrame, NextStackFrame) :-
    StackFrame = frame(Locals, _OperandStack, _Flags),
    nth0(Index, Locals, ActualType),
    isAssignable(ActualType, Type),
    validTypeTransition(Environment, [], ActualType, StackFrame,
                        NextStackFrame).

Все инструкции сохранения являются вариациями общей схемы, отличаясь типом значения, которое сохраняет инструкция.

В общем случае инструкция сохранения безопасна по типу, если локальная переменная, на которую она ссылается, имеет тип, являющийся супертипом Type, а верхний элемент стека операндов — подтипом Type, где Type — тип, который инструкция предназначена для сохранения.

Более точно, сохранение безопасно по типу, если можно извлечь тип ActualType, который «соответствует» Type (то есть является подтипом Type), со стека операндов (§4.10.1.4), а затем корректно присвоить этот тип локальной переменной LIndex.

storeIsTypeSafe(_Environment, Index, Type,
                frame(Locals, OperandStack, Flags),
                frame(NextLocals, NextOperandStack, Flags)) :-
    popMatchingType(OperandStack, Type, NextOperandStack, ActualType),
    modifyLocalVariable(Index, ActualType, Locals, NextLocals).

Учитывая локальные переменные Locals, изменение типа Index на Type приводит к списку локальных переменных NewLocals. Изменения несколько сложны, поскольку некоторые значения (и соответствующие типы) занимают две локальные переменные. Следовательно, изменение LN может потребовать изменения LN+1 (поскольку тип будет занимать как слот N, так и N+1) или LN-1 (поскольку локальная переменная N ранее была верхней половиной значения/типа из двух слов, начиная с локальной переменной N-1, и поэтому локальная переменная N-1 должна быть аннулирована), или обоих. Это описано ниже. Мы начинаем с L0 и считаем вверх.

modifyLocalVariable(Index, Type, Locals, NewLocals) :-
    modifyLocalVariable(0, Index, Type, Locals, NewLocals).

Учитывая LocalsRest, суффикс списка локальных переменных, начиная с индекса I, изменение локальной переменной Index на тип Type приводит к суффиксу списка локальных переменных NextLocalsRest.

Если I < Index-1, просто скопируйте вход в выход и рекурсивно обработайте следующий элемент. Если I = Index-1, тип локальной переменной I может измениться. Это может произойти, если LI имеет тип размером 2. После того как мы установим LI+1 в новый тип (и соответствующее значение), тип/значение LI будет аннулировано, поскольку его верхняя половина будет уничтожена. Затем мы рекурсивно обрабатываем следующий элемент.

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

Когда мы находим переменную, которая занимает только одно слово, мы изменяем ее на Type, и всё. Когда мы находим переменную, которая занимает два слова, мы изменяем ее тип на Type, а тип следующего слова на top.

modifyLocalVariable(Index, Index, Type,
                    [_ | LocalsRest], [Type | LocalsRest]) :-
    sizeOf(Type, 1).

modifyLocalVariable(Index, Index, Type,
                    [_, _ | LocalsRest], [Type, top | LocalsRest]) :-
    sizeOf(Type, 2).

Мы ссылаемся на локальную переменную, индекс которой непосредственно предшествует локальной переменной, тип которой будет изменён, как на переменную с индексом перед. Будущий тип переменной с индексом перед, имеющей тип InputType, — это Result. Если тип локальной переменной с индексом перед, Type, имеет размер 1, он не изменяется. Если тип локальной переменной с индексом перед, Type, имеет размер 2, мы должны пометить нижнюю половину её значения из двух слов как недоступную, установив её тип на top.

modifyPreIndexVariable(Type, Type) :- sizeOf(Type, 1).
modifyPreIndexVariable(Type, top) :- sizeOf(Type, 2).

Все инструкции, которые обращаются к членам, должны учитывать правила, касающиеся protected членов. Этот раздел описывает проверку protected, соответствующую JLS §6.6.2.1.

Проверка protected применяется только к protected членам суперклассов текущего класса. protected члены в других классах будут обнаружены проверкой доступа при разрешении (§5.4.4). Существует четыре случая:

Предикату classesInOtherPkgWithProtectedMember(Class, MemberName, MemberDescriptor, MemberClassName, Chain, List) истинно, если List — это множество классов в Chain с именем MemberClassName, которые находятся в другом пакете выполнения, чем Class, и имеют protected член с именем MemberName и описанием 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).