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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download

http://hal.univ-reunion.fr/hal-01186160
Contributor : Nicolas Alarcon <>
Submitted on : Monday, November 12, 2018 - 11:05:01 AM
Last modification on : Monday, September 2, 2019 - 9:43:12 AM
Long-term archiving on : Wednesday, February 13, 2019 - 1:36:08 PM

Identifiers

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⟩

Share

Metrics

Record views

21

Files downloads

69