Sciweavers

SAS
2007
Springer

Magic-Sets Transformation for the Analysis of Java Bytecode

13 years 11 months ago
Magic-Sets Transformation for the Analysis of Java Bytecode
Denotational static analysis of Java bytecode has a nice and clean compositional definition and an efficient implementation with binary decision diagrams. But it models only 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. We overcome this limitation with a technique used up to now for logic programs only. It adds new magic blocks of code to P, whose functional behaviours are the internal behaviours of P. We prove this transformation correct with an operational semantics. We define an equivalent denotational semantics, whose denotations for the magic blocks are hence the internal behaviours of P. We implement our transformation and instanwith abstract domains modelling sharing of two variables and non-cyclicity of variables. We get a static analyser for full Java bytecode that is faster and scales better than another operational pair-sharing analyser and a constraint-bas...
Étienne Payet, Fausto Spoto
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where SAS
Authors Étienne Payet, Fausto Spoto
Comments (0)