Java Bytecode Verification is not possible (Extended Abstract

During an attempt to prove that our Java compiler in [6] generates code that is accepted by the Java Bytecode Verifier we found examples of legal Java programs which are rejected by any Bytecode Verifier. The examples show that Java Bytecode Verification as it has been introduced by Sun is not possible. We propose therefore to restrict the so-called rules of definite assignment for the try-finally statement as well as for the labeled statement such that our example programs are no longer allowed. Then we can prove, using the framework of Abstract State Machines (see [3, 1]), that each program from the restricted Java language is accepted by the Java Bytecode Verifier. The programs Test1 and Test2 in Table 1 are legal Java programs. When they are compiled using a standard Java compiler like Sun’s JDK 1.2 or 1.3 compiler, then the generated bytecode is rejected by any bytecode verifier we tried including JDK 1.2, JDK 1.3, Netscape 4.73–4.76, Microsoft VM for Java 5.0 and 5.5 and the Kimera Verifier [5]. The problem is that in the eyes of the verifier the variable i is unusable at the end of the method at the return i instruction, whereas according to the JLS [2, §16.2.14] the variable i is definitely assigned after the try-finally statement. The two programs Test1 and Test2 cannot be verified, because the class of valid Java programs is too large for verifiers. Our solution to the problem is to restrict the so-called “rules of definite assignment” for the try-finally and the labeled statement [2, §16.2.14 and §16.2.5]. The two restrictions of the rules of definite assignment are sufficient to prove the following theorem: Theorem 1 If a Java compiler satisfies the constraints of Part II in [6], then the bytecode it generates from valid Java programs of the restricted Java language will be accepted by a correct bytecode verifier. A compiler satisfying the constraints of Part II in [6] must compile boolean test expressions in a special way taking care of the boolean literals true and false. It must compile try-finally statements as it is described in [4, §7.13]. class Test1 { int m1(boolean b) { int i; try { if (b) return 1; i = 2;} finally { if (b) i = 3; return i