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.
Type de document :
[Research Report] RR-7021, INRIA. 2010, pp.59
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

Contributeur : Delphine Demange <>
Soumis le : vendredi 19 novembre 2010 - 17:52:35
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : vendredi 2 décembre 2016 - 10:48:32


Fichiers produits par l'(les) auteur(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〉



Consultations de la notice


Téléchargements de fichiers