Motivation and Problem Statement

The bytecode verification is an important part of Java security and is checked by TCK. While modern compilers do not generate subroutines, to pass TCK, we need to support any aspect of the verification including the subroutine verification.

We created a modular subroutine inliner, which then reused the data flow analysis for programs without subroutines. Inlining approach allows supporting a bigger subset of type-safe programs [3], for example, the programs generated by bytecode optimizers. While our solution is compatible with specification, it can be easily tuned and extended to different safe program sets.

Definitions

Common Terms

Special Nodes in a Control Flow Graph

Graph Node Marks

Each graph node is either reachable from the first node or not. This is represented by a boolean flag vf_Node_s.reachable.

Also, nodes are either a part of subroutine or a top level code:

This marking separates subroutines from the rest of the code and provides enough information for a subsequent subroutine inlining.

Finding Subroutines

Here is an algorithm sketch.

[1] JVM specification.
[2] Leroy, X. Java Bytecode Verification: Algorithms and Formalizations.
[3] Coglio, A. Simple Verification Technique for Complex Java Bytecode Subroutines.

Subroutine_Verification (last edited 2009-09-20 21:55:28 by localhost)