Abstract
In the context of denotational style abstract interpretation it is crucial to have an efficient fixed point solver. In general, however, finding a fixed point requires exponential time. One approach to improving the efficiency is the use of special classes of functions. A well-known example for such a class are additive functions, which allow the reduction to quadratic runtime.
In this paper, we demonstrate that additive functions are not suited in a higher-order context. To overcome this defficiency, we introduce the class of component-wise additive functions, which are an extension of the class of additive functions.
Component-wise additive functions allow us to solve many higher-order equation systems in polynomial time. We stress the usefulness of our class by presenting a package for implementing abstract interpretations using our theoretical results. Furthermore, experimental results taken in a case study for escape analysis are presented to relate our approach to other approaches.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
K. Brace, R. Bryant, and L. Rudell. Efficient Implementation of a BDD Package. In 27th ACM/IEEE Design Automation Conference, June 1990.
G. L. Burn, C. Hankin, and S. Abramsky. Strictness Analysis for Higher-Order Functions. Science of Computer Programming, 7:249–278, 1986.
R. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35, August 1986.
T. Brus, M. van Eekelen, M. Van Leer, and M. Plasmeijer. Clean–A Language for Functional Graph Rewriting. In Kahn [Kah87], pages 364–384.
P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction of Approximation of Fixed Points. In Proceedings of the 4th Symposium on Principles of Programming Languages (POPL), pages 238–252. ACM, January 1977.
B. A. Davey and H. A. Priestly. Introduction to Lattices and Order. Cambridge Mathematical Textbooks. Cambridge University Press, 1990.
P. Hudak, S. L. Peyton Jones, and P. Wadler et. al. Report on the Programming Language Haskell — A Non-strict, Purely Functional Language. ACM SIGPLAN Notices, 27(4), 1992.
G. Kahn, editor. Proceedings of the 3rd Conference on Functional Programming Languages and Computer Architecture (FPCA), number 274 in Lecture Notes in Computer Science. Springer-Verlag, September 1987.
C. Martin and C. Hankin. Finding Fixed points in Finite Lattices. In Kahn [Kah87], pages 426–445.
M. Mohnen. Efficient Closure Utilisation by Higher-Order Inheritance Analysis. In A. Mycroft, editor, Proceedings of the 2nd International Symposium on Static Analysis (SAS), number 983 in Lecture Notes in Computer Science, pages 261–278. Springer-Verlag, 1995.
M. Mohnen. Efficient Compile-Time Garbage Collection for Arbitrary Data Structures. In M. Hermenegildo and S. Doaitse Swierstra, editors, Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs (PLILP), number 982 in Lecture Notes in Computer Science, pages 241–258. Springer-Verlag, 1995.
M. Mohnen. Optimising the Memory Management of Higher-Order Functional Programs. Technical Report AIB-97-13, RWTH Aachen, 1997. PhD Thesis.
H. R. Nielson and F. Nielson. Transformations on Higher-Order Functions. In Proceedings of the 4th Conference on Functional Programming Languages and Computer Architecture (FPCA), pages 129–143. ACM, September 1989.
H. R. Nielson and F. Nielson. Bounded Fixed Point Iteration. In Proceedings of the 19th Symposium on Principles of Programming Languages (POPL), pages 71–82. ACM, January 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Köller, J., Mohnen, M. (1999). A New Class of Functions for Abstract Interpretation. In: Cortesi, A., Filé, G. (eds) Static Analysis. SAS 1999. Lecture Notes in Computer Science, vol 1694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48294-6_16
Download citation
DOI: https://doi.org/10.1007/3-540-48294-6_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66459-8
Online ISBN: 978-3-540-48294-9
eBook Packages: Springer Book Archive