Abstract
This paper shows how logic programs can be used to implement the transition functions of denotational abstract interpretation. The logic variables express regularity in the abstract behaviour of commands. The technique is applied here to sign, class and escape analysis for object-oriented programs. We show that the time and space costs using logic programs are smaller than those of a ground relational representation. Moreover, we show that, in the case of sign analysis, our technique requires less memory and has an efficiency comparable to that of an implementation based on binary decision diagrams.
This work has been funded by the MURST grant “Abstract Interpretation, type systems and control-flow analysis” and the EPSRC grant GR/R53401.
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
D. F. Bacon and P. F. Sweeney. Fast Static Analysis of C++ Virtual Function Calls. In Proc. of OOPSLA’96, volume 31(10) of ACM SIGPLAN Notices, pages 324–341, New York, 1996. ACM Press.
B. Blanchet. Escape Analysis for Object Oriented Languages. Application to JavaTM. In OOPSLA’99, volume 34(10) of SIGPLAN Notices, pages 20–34, 1999.
R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 35(8):677–691, 1986.
M. Codish and B. Demoen. Deriving Polymorphic Type Dependencies for Logic Programs Using Multiple Incarnations of Prop. In B. Le Charlier, editor, Proc. SAS, volume 864 of LNCS, pages 281–296. Springer-Verlag, 1994.
P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. of POPL’77, pages 238–252, 1977.
A. Diwan, J. E. B. Moss, and K. S. McKinley. Simple and Effective Analysis of Statically Typed Object-Oriented Programs. In Proc. of OOPSLA’96, volume 31(10) of ACM SIGPLAN Notices, pages 292–305, New York, 1996. ACM Press.
J. Gallagher, D. Boulanger, and H. Saglam. Practical Model-Based Static Analysis for Definite Logic Programs. In J. W. Lloyd, editor, Proc. of the Int. Logic Programming Symp., ILPS’95, pages 351–365, Portland, Oregon, 1995. MIT Press.
N. Heintze and J. Jaffar. Set Constraints and Set-Based Analysis. In A. Borning, editor, Proc. of Principles and Practice of Constraint Programming, volume 874 of LNCS, pages 281–298. Springer-Verlag, 1994.
M. Hermenegildo, W. Warren, and S.K. Debray. Global Flow Analysis as a Practical Compilation Tool. Journal of Logic Programming, 13(2 & 3):349–366, 1992.
P. M. Hill and F. Spoto. A Foundation of Escape Analysis. In H. Kirchner and C. Ringeissen, editors, Proc. of AMAST’02, volume 2422 of LNCS, pages 380–395, St. Gilles les Bains, La Réunion island, France, September 2002. Springer-Verlag.
R. Hindley. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc., 146:29–60, 1969.
J. M. Howe and A. King. Implementing Groundness Analysis with Definite Boolean Functions. In G. Smolka, editor, ESOP 2000, volume 1782 of LNCS, pages 200–214, Berlin, Germany, 2000. Springer-Verlag.
T. Jensen and F. Spoto. Class Analysis of Object-Oriented Programs through Abstract Interpretation. In F. Honsell and M. Miculan, editors, Proceedings of FOSSACS 2001, volume 2030 of LNCS, pages 261–275. Springer-Verlag, 2001.
J. Köller and M. Mohnen. A New Class of Function for Abstract Interpretation. In A. Cortesi and G. Filé, editors, Proc. of the Static Analysis Symposium, SAS’99, volume 1694 of LNCS, pages 248–263, Venice, Italy, 1999. Springer-Verlag.
J. Lind-Nielsen. BuDDy-A Binary Decision Diagram Package. Available at http://www.itu.dk/research/buddy/.
R. Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and Systems Sciences, 17-3:348–375, 1978.
H. R. Nielson and F. Nielson. Bounded Fixed Point Iteration. In Proc. of POPL’92, pages 71–82. ACM Press, 1992.
J. Palsberg and M. I. Schwartzbach. Object-Oriented Type Inference. In Proc. OOPSLA’91, volume 26(11) of ACM SIGPLAN Notices, pages 146–161, 1991.
F. Spoto. The LOOP Analyser. http://www.sci.univr.it/∼spoto/loop/.
F. Spoto. Watchpoint Semantics: A Tool for Compositional and Focussed Static Analyses. In P. Cousot, editor, Proc. of SAS’01, LNCS. Springer-Verlag, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hill, P.M., Spoto, F. (2003). Logic Programs as Compact Denotations. In: Dahl, V., Wadler, P. (eds) Practical Aspects of Declarative Languages. PADL 2003. Lecture Notes in Computer Science, vol 2562. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36388-2_23
Download citation
DOI: https://doi.org/10.1007/3-540-36388-2_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00389-2
Online ISBN: 978-3-540-36388-0
eBook Packages: Springer Book Archive