Checking JVMI - JVM

In this section we de_ne the defensive VM as an instantiation of the scheme in Figure, namely by defensiveVMI = defensiveSchemeI (checkI ; trustfulVMI )

The checking function checkI of this defensive JVMI guarantees the following safety properties, which can be made precise and be proved once we have de_ned the machine.

  1. Primitive operations are executed with the right number and types of the arguments.
  2. Local variables are used consistently and correctly, that is, the machine does not operate individually on words of double words; double words are not swapped, and local variables are assigned before they are accessed.
  3. The operand stack does not overow or underow.

Types. The_rst two conditions require the introduction of a type system.

The JVM is weakly typed: at di_erent times the same register can hold an integer, a oat, or a low or high word of a long or double. The same is true for the operand stack. Hence we trace the types of words in the registers and on the operand stack and check the types before executing an instruction.

The universe WordType denotes the types of words. The JVM speci_cation, on purpose, does not specify which part of a double word is its high or low word. This is up to the implementation. In JVMI two types are compatible (denoted by v) if they are syntactically equal. The relation v is re_ned to a subsort relation in JVMO. The relation vsuf takes as its arguments two sequences of types. It checks whether a su_x of the _rst argument is compatible to the second argument.

State. We keep track of the types of words in registers and on the operand stack tagging words with types.

type Word = (Int; WordType)

As a consequence, all dynamic functions that operate on words are re_ned to include type information. The function type selects the type component of the dynamic functions reg and opd, that is type applied on a type extended operand stack of the form [(w1; t1); : : : ; (wn; tn)] returns [t1; : : : ; tn]; type applied to a local environment f(x1; (w1; t1)); : : : ; (xn; (wn; tn))g returns f(x1; t1); : : : ; (xn; tn)g. The pair (regT; opdT) of the type components type(reg) and type(opd) is called a type frame.

Environment. The third of the above conditions requires the introduction of a constant maxOpd denoting the maximum number of words the operand stack can hold.

Rules. Lifting the execution rules of JVMI onto the new state representation is easily described: the semantic functions JVMS(p; ws) now take (and return) sequences of word/type pairs instead of sequences of words only. The other operations work on the components of the new representation in the standard way, like application, indexing or concatenation. Hence, it remains to specify the boolean valued function checkI for checking JVMI's dynamic constraints, see Figure below.

Checking JVMI instructions

Checking JVMI instructions

Checking a Prim instruction requires that the appropriate argument types appear on top of the stack and that the result type can be pushed on the operand stack without overow.

overow(maxOpd; opdT; s) = length(opdT) + s > maxOpd

The function argTypes returns the sequence of argument types of a primitive operation with the low type listed before the high type. For example, argTypes(dadd) = [lowDouble; highDouble; lowDouble; highDouble]:

Dupx and Pop are polymorphic. They do not require a particular type on the stack. Rather any type can be provided as long as its size equals the required size and it is a well-formed JVM type. For this purpose we de_ne the function validTypeSeq.

Following this de_nition also the sequence [int; float] is a valid type sequence of size 2.

A Load instruction loads the run types stored under the location(s) x (and possibly x + 1) onto the operand stack only if they match the move type and if enough space is left. The rule implicitly checks that registers are not accessed before they are assigned. Indeed for a register x to which no value has been assigned, regT(x ) yields undef which is not compatible to any de_ned type. Likewise, the rule checks that for double words the types stored under locations x and x+1 have the correct low and high types, otherwise the representation of the move type would not match the runtime-type according to the following de_nition of the compatibility relation between sequences of word types and move types:

Store and Cond require appropriate argument types on the stack. For Goto and Halt nothing has to be checked.

All rights reserved © 2018 Wisdom IT Services India Pvt. Ltd Protection Status

JVM Topics