Skip to Main content Skip to Navigation
Conference papers

Magic-sets transformation for the analysis of Java bytecode

Abstract : 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/out-put 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 denota-tional semantics, 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 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-based pointer analyser.
Document type :
Conference papers
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.univ-reunion.fr/hal-01916204
Contributor : Réunion Univ <>
Submitted on : Thursday, November 8, 2018 - 12:19:34 PM
Last modification on : Thursday, March 28, 2019 - 11:24:11 AM
Long-term archiving on: : Saturday, February 9, 2019 - 1:50:41 PM

File

Magic_sets_transformation_for_...
Explicit agreement for this submission

Identifiers

  • HAL Id : hal-01916204, version 1

Collections

Citation

Etienne Payet, Fausto Spoto. Magic-sets transformation for the analysis of Java bytecode. 14th International Static Analysis Symposium (SAS 2007), Aug 2007, Kongens Lyngby, Denmark. pp.452-467. ⟨hal-01916204⟩

Share

Metrics

Record views

84

Files downloads

139