Magic-sets for localised analysis of Java bytecode - Université de La Réunion
Journal Articles Higher-Order and Symbolic Computation Year : 2010

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.
Fichier principal
Vignette du fichier
Magic_sets_for_localised_analysis_of_java_bytecode.pdf (1.53 Mo) Télécharger le fichier
Loading...

Dates and versions

hal-01186160 , version 1 (12-11-2018)

Identifiers

Cite

Fausto Spoto, Etienne Payet. Magic-sets for localised analysis of Java bytecode. Higher-Order and Symbolic Computation, 2010, 23 (1), pp.29-86. ⟨10.1007/s10990-010-9063-7⟩. ⟨hal-01186160⟩
68 View
215 Download

Altmetric

Share

More