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 functionalie 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. 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 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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers, Principles Techniques and Tools. Addison Wesley Publishing Company, Reading (1986)
Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems. Quaderno 457, Dipartimento di Matematica, Università di Parma, Italy (2006), www.cs.unipr.it/Publications
Bancilhon, F., Maier, D., Sagiv, Y., Ullman, J.: Magic Sets and Other Strange Ways to Implement Logic Programs. In: Proc. of the 5th ACM Symposium on Principles of Database Systems, pp. 1–15. ACM Press, New York (1986)
Beeri, C., Ramakrishnan, R.: On the Power of Magic. The Journal of Logic Programming 10(3 & 4), 255–300 (1991)
Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Codish, M.: Efficient Goal Directed Bottom-Up Evaluation of Logic Programs. Journal of Logic Programming 38(3), 355–370 (1999)
Codish, M., Dams, D., Yardeni, E.: Bottom-up Abstract Interpretation of Logic Programs. Journal of Theoretical Computer Science 124, 93–125 (1994)
Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: POPL 1977. Proc. of the 4th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)
Lhoták, H., Hendren, L.: Scaling Java Points-to Analysis using Spark. In: Hedin, G. (ed.) CC 2003 and ETAPS 2003. LNCS, vol. 2622, pp. 153–169. Springer, Heidelberg (2003)
Lindholm, T., Yellin, F.: The Java\(^{\mathit{TM}}\) Virtual Machine Specification, 2nd edn. Addison-Wesley, Reading (1999)
Logozzo, F.: Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verfication of Java Classes. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, Springer, Heidelberg (2007)
Méndez, M., Navas, J., Hermenegildo, M.V.: An Efficient, Parametric Fixpoint Algorithm for Incremental Analysis of Java Bytecode. In: Proc. of the second workshop on Bytecode Semantics, Verification, Analysis and Transformation, Electronic Notes on Theoretical Computer Science. Braga, Portugal, March 2007 (to appear)
Pollet, I., Le Charlier, B., Cortesi, A.: Distinctness and Sharing Domains for Static Analysis of Java Programs. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 77–98. Springer, Heidelberg (2001)
Rossignoli, S., Spoto, F.: Detecting Non-Cyclicity by Abstract Compilation into Boolean Functions. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 95–110. Springer, Heidelberg (2005)
Sabelfeld, A., Myers, A.C.: Language-based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Secci, S., Spoto, F.: Pair-Sharing Analysis of Object-Oriented Programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 320–335. Springer, Heidelberg (2005)
Spoto, F.: The JULIA Static Analyser (2007), profs.sci.univr.it/~spoto/julia
Spoto, F., Hill, P.M., Payet, E.: Path-Length Analysis for Object-Oriented Programs. In: Proc. of Emerging Applications of Abstract Interpretation, Vienna, Austria (March 2006), profs.sci.univr.it/~spoto/papers.html
Spoto, F., Jensen, T.: Class Analyses as Abstract Interpretations of Trace Semantics. ACM Transactions on Programming Languages and Systems (TOPLAS) 25(5), 578–630 (2003)
Tarski, A.: A Lattice-theoretical Fixpoint Theorem and its Applications. Pacific J. Math. 5, 285–309 (1955)
Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Payet, É., Spoto, F. (2007). Magic-Sets Transformation for the Analysis of Java Bytecode. In: Nielson, H.R., Filé, G. (eds) Static Analysis. SAS 2007. Lecture Notes in Computer Science, vol 4634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74061-2_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-74061-2_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74060-5
Online ISBN: 978-3-540-74061-2
eBook Packages: Computer ScienceComputer Science (R0)