Dynamic semantics of the JVMI - JVM

The basic machine JVMI is an untyped word-oriented stack-machine supporting all instructions for implementing a while-language. JVMI provides instructions to load constants, to apply various unary and binary operators, to load and store a variable, to duplicate and to remove values, and to jump unconditionally or conditionally to a label. A JVMI program is a sequence of instructions.

The universe PrimOp contains literals, unary and binary functions and relations. O_set and Size denote code o_sets and the amount of words to move.

These universes are synonyms for the universe of natural numbers Nat. And so is the universe RegNo, which stands in for variable locations in the JVM.

Load and Store instructions are also parametrized by the types they move. Possible types of values in JVMI are:

data MoveType = int j long j float j double

Real JVM instructions can be obtained by expanding the (parameter) universes PrimOp, Size, and MoveType. In fact the abstract instructions above already comprise about 150 of the 200 bytecode instructions of the JVM.

Environment. JVMI's static environment consists only of the bytecode for the currently executed method. code: Code type Code = Instr_

We assume for simplicity of exposition and without loss of generality that the last instruction of code is Halt. Later we will write this function more precisely as parametrized (namely by the current method).

Values. JVMI supports integers, oats, longs and doubles. Integers are 32- bit, longs are 64-bit signed two complement values. Floats are 32-bit, doubles are 64-bit IEEE 754 oating point numbers. The universe of Words is supposed to hold 32-bit values.2 64-bit values are mapped to sequences of length two of words in an implementation dependent way. Thus JVM values are sequences of length one or two of words. The Size of a value is its length in words. The function size can also be applied on MoveTypes, in which case it returns the number of words to move.

JVMI implements values and operations on the introduced data types in the usual way, the only exception being boolean. Booleans are represented as integers: 0 is used for False, and 1 for True. We denote by JVMS(s) the semantic value corresponding to syntactic arguments s.

State. JVMI's dynamic state consists of a single frame, containing a program counter pc, registers reg (i.e., a local variable environment), and an operand stack opd. In the declaration below, the _rst column de_nes the state, and the second column de_nes the condition on the initial state.

Trustful execution of JVMI instructions

Trustful execution of JVMI instructions

Rules. speci_es the dynamic semantics of JVMI instructions by ASM rules. The trustfulVMI halts, if the pc points to Halt where we update the dynamic function halt. In the defensive VM and the diligent VM there are other reasons for halting. As long as the trustfulVMI does not halt, it _res execVMI rules.

trustfulVMI = execVMI (code(pc))

Remark For the sake of brevity, we suppress notationally the main guard of all our machines, namely halt = undef. As soon as halt gets a de_ned value (e.g. Halt, Verification failed, etc.) the machines stop executing, as do their executable versions.

The execVMI rules de_ne the e_ect of executing a single instruction. The Prim(p)instruction takes n values from the top of the operand stack,where n is determined using argSize(p) that returns the sum of the sizes of the parameters of p, e.g. argSize(iadd) = 2 and argSize(dadd) = 4. If p is an element of the divMod operator set (that denotes integer and long division and modulo operators) and the right operand is 0, then the execution of the instruction is unde_ned. Otherwise, the result of the semantic function JVMS(p; ws) applied on the popped values ws is pushed onto the operand stack. For instance the value of JVMS(iadd; [1; 2]) is 3. The function JVMS takes care of the semantic e_ect of all arithmetic and type conversion instructions of the real JVM. The instruction Pop removes the top stack value. A Dupx instruction duplicates the top value ws2 and inserts the duplicate below the second value ws1 on the stack. For example, the instruction Dupx(0; 1) is the dup instruction of the real JVM. A Load instruction loads the value stored under the location x on top of the stack. If x denotes a double word, the next two locations are pushed on top of the stack. A Store instruction stores the top (double) word of the operand stack in the registers x (and x + 1). A Goto instruction causes execution to jump to the next instruction determined by the provided parameter. The Cond instruction is a conditional goto. If the relation for the values on top of the operand stack holds, execution continues at the speci_ed instruction, otherwise execution proceeds with the next instruction.

All rights reserved © 2020 Wisdom IT Services India Pvt. Ltd DMCA.com Protection Status

JVM Topics