Skip to Main content Skip to Navigation
New interface
Reports (Research report)

A Provably Correct Stackless Intermediate Representation For Java Bytecode

Delphine Demange 1 Thomas Jensen 1 David Pichardie 1 
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : 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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Delphine Demange Connect in order to contact the contributor
Submitted on : Friday, November 19, 2010 - 5:52:35 PM
Last modification on : Thursday, October 27, 2022 - 3:44:51 AM
Long-term archiving on: : Friday, December 2, 2016 - 10:48:32 AM


Files produced by the author(s)


  • HAL Id : inria-00414099, version 3


Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation For Java Bytecode. [Research Report] RR-7021, INRIA. 2010, pp.59. ⟨inria-00414099v3⟩



Record views


Files downloads