Magic-sets for localised analysis of Java bytecode

Abstract : Static analyses based on denotational semantics can naturally model functional behaviours of the code in a compositional and completely context and flow sensitive way. But they only model the functional i.e., input/output behaviour of a program P, not enough if one needs P’s internal behaviours i.e., from the input to some internal program points. This is, however, a frequent requirement for a useful static analysis. In this paper, we overcome this limitation, for the case of mono-threaded Java bytecode, with a technique used up to now for logic programs only. Namely, we define a program transformation that adds new magic blocks of code to the program P, whose functional behaviours are the internal behaviours of P. We prove the transformation correct w.r.t. an operational semantics and define an equivalent denotational semantics, devised for abstract interpretation, whose denotations for the magic blocks are hence the internal behaviours of P. We implement our transformation and instantiate it with abstract domains modelling sharing of two variables, non-cyclicity of variables, nullness of variables, class initialisation information and size of the values bound to program variables. We get a static analyser for full mono-threaded Java bytecode that is faster and scales better than another operational pair-sharing analyser. It has the same speed but is more precise than a constraint-based nullness analyser. It makes a polyhedral size analysis of Java bytecode scale up to 1300 methods in a couple of minutes and a zone-based size analysis scale to still larger applications.
Type de document :
Article dans une revue
Higher-Order and Symbolic Computation, Springer Verlag, 2010, 23 (1), pp.29-86. 〈10.1007/s10990-010-9063-7〉
Liste complète des métadonnées

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

http://hal.univ-reunion.fr/hal-01186160
Contributeur : Nicolas Alarcon <>
Soumis le : lundi 12 novembre 2018 - 11:05:01
Dernière modification le : mardi 13 novembre 2018 - 10:46:47

Identifiants

Collections

Citation

Fausto Spoto, Etienne Payet. Magic-sets for localised analysis of Java bytecode. Higher-Order and Symbolic Computation, Springer Verlag, 2010, 23 (1), pp.29-86. 〈10.1007/s10990-010-9063-7〉. 〈hal-01186160〉

Partager

Métriques

Consultations de la notice

2

Téléchargements de fichiers

4