A Provably Correct Stackless Intermediate Representation For Java Bytecode - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2010

A Provably Correct Stackless Intermediate Representation For Java Bytecode

Résumé

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.
Fichier principal
Vignette du fichier
rr7021.pdf (1.08 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00414099 , version 1 (07-09-2009)
inria-00414099 , version 2 (03-11-2009)
inria-00414099 , version 3 (19-11-2010)

Identifiants

  • HAL Id : inria-00414099 , version 3

Citer

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⟩
316 Consultations
369 Téléchargements

Partager

Gmail Facebook X LinkedIn More