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.
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 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.
JVM Related Interview Questions
|Java Script Interview Questions||Adv Java Interview Questions|
|Core Java Interview Questions||AJAX Interview Questions|
|Android Interview Questions||Java applet Interview Questions|
|Java 8 Interview Questions||JBOSS Interview Questions|
|Advanced jQuery Interview Questions||Apache Tomcat Interview Questions|
|Application Virtualization Interview Questions||Java 9 Interview Questions|
The Imperative Core Javai Of Java
The Procedural Extension Javac Of Javai
The Object-oriented Extension Javao Of Javac
The Exception-handling Extension Javae Of Javao
The Concurrent Extension Javat Of Javae
Java Is Type Safe
The Jvmi Submachine
The Procedural Extension Jvmc Of Jvmi
The Object-oriented Extension Jvmo Of Jvmc
The Exception-handling Extension Jvme Of Jvmo
Correctness Of The Compiler
The Defensive Virtual Machine
Bytecode Type Assignments
The Diligent Virtual Machine
The Dynamic Virtual Machine
All rights reserved © 2018 Wisdom IT Services India Pvt. Ltd
Wisdomjobs.com is one of the best job search sites in India.