Magic-Sets Transformation for the Analysis of Java Bytecode

Denotational static analysis of Java bytecode has anice and clean compositional definition and an efficientimplementation with binary decision diagrams.But it models only the functionalie input/output behaviour of a program P,not enough if one needs P's internal behavioursie from the input to some internal program points.We overcome this limitation with a technique used up to nowfor logic programs only. It adds new magic blocks of codeto P, whose functional behaviours are the internal behaviours of P.We prove this transformation correct with an operationalsemantics. We define an equivalent denotational semantics, whosedenotations for the magic blocks are hence the internal behavioursof P. We implement our transformationand instantiate it with abstract domains modelling sharingof two variables and non-cyclicity of variables.We get a static analyser for full Java bytecode that is faster andscales better than another operational pair-sharing analyserand a constraint-based pointer analyser.