A Provably Correct Stackless Intermediate Representation For Java Bytecode

The Java virtual machine executes stack-based bytecode. The intensive use of an operand stack has been identified as a major obstacle for static analysis and it is now common for static analysis tools to manipulate a stackless intermediate representation (IR) of bytecode programs. Several algorithms have been proposed to achieve such a transformation, whereas only little attention has been paid to their formal semantic properties. This work specifies such a bytecode transformation and provides the semantic foundations for proving that an initial program and its IR behave similarly, in particular with respect to object creation and throwing of exceptions. The transformation is based on a symbolic execution of the bytecode, using a symbolic operand stack. Each bytecode instruction modifies the abstract stack and gives rise to the generation of IR instructions. We formalize a notion of semantics preservation: an initial program and its IR have similar execution traces. Since the transformation does not preserve the object allocation order, the similarity between traces is defined using a relation over the two heaps. Finally, we prove the correctness of this transformation with respect to this semantic criterion and present a prototype implementation