Successors of bytecode instructions - JVM

Since the veri_er works at link-time, it operates only on the type components of the items stored in registers and on the operand stack, as introduced for the defensive VM. These type components constitute a type frame. For each instruction, the veri_er tries to simulate the e_ect for all possible successors.

To determine the successor type frame, in this section a function succ is de_ned by stepwise re_nement for each of the submachines.

Successors for JVMI instructions

Successors for JVMI instructions

Successors for JVMI instructions

Fig. above de_nes the succI function which computes for every JVMI instruction and given type frame the set of instructions together with the corresponding type frames which are possible successors of the given instruction and type frame in the given method. It simulates on the type frame all transitions an instruction can make. Successors which can be reached via an exception are listed below in the function succE. The argument instr of the function succI is the instruction at code index pc.

Successors for JVMC instructions

Fig. below de_nes the extension of succI to the function succC . In contrast to the registers and to the operand stack that are weakly typed, class _elds in JVMC are strongly typed: every _eld lways holds a single type. In contrast to the defensive VM, the veri_er therefore uses the declared type of the global _eld which is stored as _rst parameter in GetStatic and PutStatic instructions. Similarly, for method invocations the declared return type is propagated to the successor type frame. Since the e_ect of a return instruction is to leave the given method, such instructions generate no successors in that method.

Successors for JVMC instructions

Successors for JVMC instructions

Successors for JVMO instructions

Successors of JVMO instructions with given type frame are de_ned. For instructions which do not relate to object initialization, the successors are computed similarly to those for JVMC instructions in Fig. above, taking into account also the type of the target object. The linktime checkable requirements on object initialization pose several new problems.

The defensive VM keeps track of the initialization status of objects by adding information to the generated run-time reference via the dynamic function initState. For link-time veri_cation this run-time information has to be simulated in the type system.

At link-time, di_erent New instructions can be distinguished by their instruction index. However, this information does not denote uninitialized objects uniquely. For instance, it does not su_ce to distinguish di_erent runtime instances of New which is part of a loop body. But if we require that the uninitialized type that we generate when we simulate a New instruction is neither in any of the type registers nor in the type operand stack, then this assures uniqueness of the type description. The successor of New in Fig. below replaces the uninitialized type on the operand stack with the verify type unusable and _lters out all registers with the uninitialized type such that they are not available at the successor code index. We do not add this as a check to the function checkO in Fig. below, because that would violate the monotonicity property of Lemma.

By construction any execution of an instance initialization method initializes only a single object. As a consequence in any type frame of an initialization method there is the type descriptor InInit for only this object.

By de_nition, an object is regarded as fully initialized after execution of an instance initialized method. Hence in the successor of an InvokeSpecial instruction which invokes an initialization method, the uninitialized type of the object has to be replaced by the initialized type. In case of InInit the initialized type is equal to the class of the current initialization method.

Successors for JVMO instructions

Successors for JVMO instructions

Successors for JVME instructions

The function succE reects the consequences of exception handling and embedded subroutines. We _rst consider which handler frames have to be included as possible successors of JVME instructions. For Athrow instructions the control proceeds according to the exception table of the method. Therefore every possible handler of the thrown exception provides a candidate for a successor instruction. It would be wrong to restrict the successors of the Athrow instruction to those handlers (from; upto; handle; _) for which c v _ , where c is the topmost type on the operand stack. At run-time the topmost reference on the operand stack will be of a subtype of c and could be caught by a di_erent handler.

Several instructions might throw run-time exceptions. Therefore, the handlers which catch run-time exceptions have to be included in the successors, too. Moreover, the VM might throw a VirtualMachinError almost at any position in the bytecode. Therefore, for each code index and each instruction, except for Jsr, Goto, Return and Load, we include into the set of possible successors all handlers which protect the code index.

Successors for JVME instructions

Successors for JVME instructions

Some instructions do not throw exceptions (; CD)

Some instructions do not throw exceptions (; CD)

Successors are monotonic

Successors are monotonic

It seems that this simple de_nition is good enough for bytecode generated by a Java compiler. We assume that the instructions Jsr, Goto, Return and Load wich are used for the compilation of the continue, break and return statements do not throw exceptions. Therefore they do not have successors via the exception table. Otherwise, programs like the one in Fig. below would be rejected by our veri_er.

The instruction Jsr(s) pushes the type retAddr(s) on top of the operand stack indicating that this is a return address to a caller which has called subroutine s. The successor of a Ret instruction is not de_ned in the function succE. Instead, it is treated as a special case in the de_nition of bytecode type assignments in the next section, and also in the de_nition of type propagation in the bytecode veri_er. The reason for this is that a Ret instruction does not return all local registers, but only the registers the corresponding subroutine has modi_ed. The types of the other registers have to be propagated from the caller of the subroutine.

The following lemma says that the successors of an instruction with respect to a more speci_c type frame are more speci_c than some successors with respect to the more general type frame. We write succ(meth; pc; regT; opdT) for succE(meth)(code(meth)(pc); pc; regT; opdT);

similarly check(meth; pc; regT; opdT) for checkE(meth)(code(meth)(pc); maxOpd(meth); pc; regT; opdT):

Lemma 16.2.1 (Successors are monotonic). Assume that (regV ; opdV ) and (regT; opdT) are type frames with regV vreg regT and opdV vseq opdT. If check(meth; pc; regT; opdT) is true and (s; regS; opdS) is a successor in succ(meth; pc; regV ; opdV ), then there exists a successor (s; regU ; opdU ) in succ(meth; pc; regT; opdT) such that regS vreg regU and opdS vseq opdU Proof. The lemma follows by a case distinction along the JVM instructions from the transitivity of the compatibility relation v. ut


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

JVM Topics