Magic-sets for localised analysis of Java bytecode (Q656846)

This paper develops a program transformation technique that allows to nicely extend the scope of static analyses based on denotational semantics to the characterization of the internal behavior of Java bytecode. This overcomes the main limitation of such type of static analyses which traditionally enable only a functional modeling, i.e. input/output, of the code behavior. The proposed technique is based on a magic-set transformation, similar to those already employed for functional and logic languages, that adds new blocks of code to a program without altering its semantics (only the structure of the blocks of bytecode is transformed while the bytecode itself remains unchanged). The functional behaviors of such blocks capture the internal behavior of the program at the points where they are inserted. The correctness of the transformation is proven with respect to an operational semantics on the basis of which an equivalent denotational semantics for the transformed program is defined. The achieved semantics is then exploited for deriving five types of static analyses, i.e., pair-sharing, cyclicity, nullness, class initialization and size. The transformation and the derived analyses are implemented and experimented in the context of the JULIA denotational analyzer. Regarding the manuscript organization, it is almost self-contained. Section 2 and 3 present the proposed magic-set transformation. Section 4 describes in depth the operational semantics for the Java bytecode, on the basis of which the devised transformation is proven to be correct in Section 5. Section 6 details the denotational semantics and Section 7 proves its equivalence to the operational semantics of Section 4. Section 8 gives some details about a nullness abstraction for the denotational semantics. The reported material allows the reader to grasp how the denotational semantics is exploited in practice, even though I would have liked to see it applied on a small yet complete example. It is my opinion that this could have been done without impact on the length of the paper by sacrificing, for example, Section 6.1 which contains some Java-related technicalities. I also think that including a concrete example involving an abstract domain which does not satisfy the ascending chain condition and showing a suitable widening operator for it would have helped the understanding of such an issue. The results reported in Section 8 and the availability of a simple web interface to JULIA witness the validity of the approach and its efficiency. Overall, however, this is a well written, much worth reading paper. In particular, I appreciated its completeness and the gradual way with which such a complex subject is introduced, developed and discussed, making it quite accessible to non-specialist readers. The advantages derived from a denotational semantics for the Java bytecode, which enables one to conduct different types of static analyses, go beyond the bytecode obtained from compiling ``pure'' Java source code. In the last few years, other programming languages, whose source-code compilation targets Java bytecode, have been introduced, namely Clojure, Groovy and more recently Scala. The denotational semantics could be easily customized, with little or no effort, to cope also with these languages.