# Verifying JVME - JVM

This extends the veri_er for the object-oriented machine to verify also the constraints which are related to exceptions and embedded subroutines.

The diligentVME is obtained by instantiating the diligentScheme with a re_nement propagateVME of propagateVMI by rules for Jsr and Ret instructions, and with succE, checkE and trustfulVME instead of succO, checkO and trustfulVMO.

diligentVME = diligentScheme(verifyVM ; trustfulVME) where verifyVM = verifySchemeC (propagateVME; succE; checkE) The extended rule propagateVME completes the de_nition of the function succE in Fig. 16.15 by propagating type frames also to the successors of Ret instructions, namely to the direct successors j + 1 of all code indices j from where the corresponding subroutine may possibly have been called. As we will prove below, this is done in such a way that the invariant I7 from Theorem 17.1.1 is satis_ed for indices in V n C, where V = dom(visited) and C = dom(changed).

The rule propagateVME takes also care that during the veri_cation process, the set enterJsr(s) contains exactly the code indices of visited instructions Jsr(s), i.e.,

Similarly propagateVME computes the set leaveJsr(s), a superset of the following set:

The equality does not hold, because the type of a local register can disappear in a merge.

Except for the initialization of the new functions when the veri_cation of a method starts, which will be given below, this completes the de_nition of the diligentVME. It remains to show that the additional propagation rule propagateVME is sound and complete.

Proof. Assume the rule propagateJsr(code; j ; s; i) has been applied without producing a failure. Then we know that i and j are in V n C and

We have to show that the type frame propagation to the successor j + 1 satis_es conditions (a){(f) of I7.

j + 1 2 V holds because the validCodeIndex test was passed successfully.

PropagateJsr propagates the new stack from i to j +1, simulating a possible return from the subroutine. In this way we ensure condition (c) of invariant I7.

The types for the registers which are propagated to j + 1 are a combination of the types at j where the subroutine has been called and the types at I where the subroutine returns.

Let us call a type invalid, if it is a return address type retAddr() such that the subroutine s is not contained in. If a register is modi_ed by the subroutine, then its type from i is propagated.

Otherwise the register disappears at j + 1. This implies condition (b) of invariant I7. If a register is not modi_ed by the subroutine, then its type from j is propagated if this type is valid and di_erent from ( ; )new and InInit. Otherwise the register disappears at j +1. This implies conditions (d){(f) of invariant I7. ut

Proof. Assume that the method we are verifying has a bytecode type assignment (regTi ; opdTi )i2D. When propagateJsr(code; j ; s; i ) is called we know by the induction hypothesis that

We have to show that in the next step of the veri_cation, after the successors have been propagated to j + 1, the following holds:

Then x is also de_ned in regVj , regVj (x ) is a valid jump for s and di_erent from ( ; )new and InInit, because otherwise condition T7 (e) or (f) of Def. would be violated. Hence, the local variable x is de_ned in regJ and regJ (x ) = regVj (x ), therefore regJ (x ) v regTj+1(x ). ut At the beginning of the veri_cation of a method the new functions enterJsr and leaveJsr have to be initialized, so that we re_ne the initVerify rule as follows:

In the retrospective it is con_rmed that verifying embedded subroutines is not trivial, whereas checking embedded subroutines posed no particular problems. This is the reason why we started with the checking machine before developing the veri_er by imposing necessary and su_cient conditions which are checkable at link-time on the code.

Proof. (Main Theorem) Let any well-formed and well-typed Java program P be given, let PC = compile(P) for the compiler. By Theorem 16.5.2 PC has a bytecode type assignment. Therefore by Theorem 17.1.2, PC passes successfully the bytecode veri_er in the diligent VM, so that it will be trustfully executed by the submachine trustfulVM of diligent VM without violating any run-time checks (by Theorem 16.4.1) and by Theorem 14.1.1 with the same semantical e_ect as P has on the machine execJava de_ned ut