Principal bytecode type assignments - JVM

Bytecode type assignments can be compared in the obvious way. We say that a type assignment (regVi ; opdVi )i2V is more speci_c than the type assignment (regTi ; opdTi )i2D, if the following three conditions are satis_ed:

Hence a more speci_c type assignment assigns type frames to less code indices.
It assigns more speci_c types to more local variables and it assigns more speci_c types to an operand stack of the same size. A most speci_c type assignment to bytecode is called a principal type assignment.

Let _ be the method which has to be veri_ed. The bytecode veri_er attempts to compute a bytecode type assignment (regVi ; opdVi )i2V for the method. At the beginning the set V consists of code index zero only. More indices are added to V whenever they can be reached by the computation which tries to propagate the already computed type frames to the possible successor indices. It can happen that during this process an index is revisited and the type frame for the index has to be changed. In this case the index is added to a set C of changed indices whereby it becomes subject to yet another veri_cation step, namely the attempt to propagate its new type frame. The bytecode veri_er proceeds until the set C is empty. It can be shown that the veri_er always terminates. During the veri_cation the following invariants are satis_ed which correspond exactly to the seven conditions for bytecode type assignments in Def. We formulate the invariants as a theorem which will be proved later.

Theorem (Soundness of the veri_er). Let _ be the method to be veri_ed. During the veri_cation process the following invariants are satis_ed where C = dom(changed)

and V = dom(visited):
I1. C _ V and V is a set of valid code indices of the method _.
I2. Code index 0 belongs to V.
I3. Let [_1; : : : ; _n] = argTypes(_) and c = classNm(_). If _ is a
a) class initialization method: regV0 = ;.
b) class method: f0 7! _1; : : : ; n 1 7! _ng vreg regV0.
c) instance method: f0 7! c; 1 7! _1; : : : ; n 7! _ng vreg regV0.
d) constructor: f0 7! InInit; 1 7! _1; : : : ; n 7! _ng vreg regV0.
(The constructor of class Object is treated as an instance method.)
I4. The list opdV0 is empty.
I5. If i 2 V n C, then check(_; i; regVi ; opdVi ) is true.
I6. If i 2 V n C and (j ; regS; opdS) 2 succ(_; i; regVi ; opdVi ), then
j 2 V, regS vreg regVj and opdS vseq opdVj .
I7. If i 2 V n C, code(i) = Ret(x ) and regVi (x ) = retAddr(s), then for all
reachable j 2 V n C with code(j ) = Jsr(s):
a) j + 1 2 V,
b) regVi vreg mod(s) _ regVj+1,
c) opdVi vseq opdVj+1,
d) regVj vreg mod(s) _ regVj+1,
e) if retAddr(`) occurs in mod(s) _ regVj+1, then each code index
which belongs to s belongs to l ,
f) neither (c; k)new nor InInit occur in mod(s) _ regVj+1.
I8. If i 2 V and retAddr(s) occurs in regVi , then i belongs to s.
If i 2 V and retAddr(s) occurs in opdVi , then i = s.

If the set C of changed code indices is empty, then I1{I8 are equivalent to the conditions T1{T8 of Def. and the veri_er has computed a bytecode type assignment. Conversely, if the method to be veri_ed has a bytecode type assignment, then the bytecode type assignment computed by the veri_er will be more speci_c. In other words, the veri_er is complete.

Theorem (Completeness of the veri_er). If the method _ has a bytecode type assignment (regTi ; opdTi )i2D, then during the veri_cation process (regVi ; opdVi )i2V will always be more speci_c than (regTi ; opdTi )i2D and no VerifyError will occur.

We are going now to de_ne a sequence of four diligent virtual machines and to prove soundness and completeness for their veri_er.


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

JVM Topics