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] RR-7021, INRIA. 2010, pp.59
Liste complète des métadonnées

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/inria-00414099
Contributor : Delphine Demange <>
Submitted on : Friday, November 19, 2010 - 5:52:35 PM
Last modification on : Friday, October 26, 2018 - 10:26:07 AM
Document(s) archivé(s) le : Friday, December 2, 2016 - 10:48:32 AM

File

rr7021.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00414099, version 3

Citation

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〉

Share

Metrics

Record views

608

Files downloads

120