Magic-sets for localised analysis of Java bytecode

Static analyses based on denotational semantics can naturally modelfunctional behaviours of the code in a compositionaland completely context and flow sensitive way. But theyonly model the functional, ie., input/output behaviour of a program P,not enough if one needs P's internal behaviours,ie., from the input to some internal program points.This is, however, a frequent requirement for a useful staticanalysis. In this paper, weovercome this limitation, for the case of mono-threaded Java bytecode,with a technique used up to nowfor logic programs only. Namely, we define a programtransformation that adds new "magic" blocks of code to theprogram P, whose functional behaviours are the internal behaviours of P.We prove the transformation correct wrt. an operationalsemantics and define an equivalent denotational semantics, devised forabstract interpretation, whosedenotations for the magic blocks are hence the internal behavioursof P. We implement our transformationand instantiate it with abstract domains modellingsharing of two variables, non-cyclicity of variables,nullness of variables, class initialisation informationand size of the values bound to program variables.We get a static analyser for full mono-threaded Java bytecode that is faster andscales better than another operational pair-sharing analyser.It has the same speed but is more precisethan a constraint-based nullness analyser. It makes a polyhedralsize analysis of Java bytecode scale up to 1300 methods in a coupleof minutes and a zone-based size analysis scale to still largerapplications.