Set-based analysis of ML programs

ABSTRACT

Reasoning about program variables as sets of “values” leads to a simple, accurate and intuitively appealing notion of program approximation. This paper presents approach for the compile-time analysis of ML programs. To develop the core ideas of the analysis, we consider a simple untyped call-by-value functional language. Starting with an operational semantics for the language, we develop an approximate “set-based” operational semantics, which formalizes the intuition of treating program variables as sets. The key result of the paper is an O(n3) algorithm for computing the set based approximation of a program. We then extend this analysis in a natural way to deal with arrays, arithmetic, exceptions and continuations. We briefly describe our experience with an implementation of this analysis for ML programs.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	A. Aiken and E. Wimmers, "Solving Systems of Set Constraints", Proc. 7tn IEEE Syrup. on Logic in Com. purer Science, Santa Cruz, pp. 329-340, June 1992.
	2	Alexander Aiken , Edward L. Wimmers, Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture, p.31-41, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165188]
	3	Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177847]
	4	Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
	5	L. Bachmair, H. Ganzinger and U. Waldmann, "Set Constraints are the Monadic Class", Technical Report MPI-I-92-240, Max-Planck-institute for Computer Science, December 1992.
	6	Edoardo Biagioni , Robert Harper , Peter Lee , Brian G. Milnes, Signatures for a network protocol stack: a systems application of Standard ML, Proceedings of the 1994 ACM conference on LISP and functional programming, p.55-64, June 27-29, 1994, Orlando, Florida, United States
	7	Robert Cartwright , Mike Fagan, Soft typing, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.278-292, June 24-28, 1991, Toronto, Ontario, Canada
	8	Charles Consel , Olivier Danvy, Tutorial notes on partial evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.493-501, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158707]
	9	Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
	10	Nevin Charles Heintze, Set based program analysis, Carnegie Mellon University, Pittsburgh, PA, 1992
	11	Nevin Heintze, Set Based Analysis of Arithmetic, Carnegie Mellon University, Pittsburgh, PA, 1993
	12	Nevin Heintze , Joxan Jaffar, A finite presentation theorem for approximating logic programs, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.197-209, December 1989, San Francisco, California, United States [doi>10.1145/96709.96729]
	13	N. Heintze and J. Jaffar, "A Decision Procedure for a Class of Herbrand Set Constraints", Proc. 5th IEEE Syrup. on Logsc ,n Computer Science, Philadelphia, pp. 42-51, June 1990. (A full version of this paper appears as Carnegie Mellon University Technical Report CMU-CS-91-110, 42 pp., February 1991.)
	14	N. Heintze and J. Jaffar, "An Engine for Logic Program Analysis", Proc. 7th IEEE Syrup. on Logic in Computer Science, Santa Cruz, pp. 318-328, June 1992.
	15	Fritz Henglein, Efficient type inference for higher-order binding-time analysis, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.448-472, June 1991, Cambridge, Massachusetts, United States
	16	T. P. Jensen , T. Æ Mogensen, A backwards analysis for compile-time garbage collection, Proceedings of the third European symposium on programming on ESOP '90, p.227-239, May 1990, Copenhagen, Denmark
	17	N. Jones, "Flow Analysis of Lazy Higher-Order Functional Programs", in Abstract Interpretation of Declarative Languages, S. Abramsky and C. Hankln (Eds.), Ellis Horwood, 1987.
	18	Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
	19	Neil D. Jones , Steven S. Muchnick, Flow analysis and optimization of LISP-like structures, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.244-256, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567776]
	20	Steven S. Muchnick , Neil D. Jones, Program Flow Analysis: Theory and Application, Prentice Hall Professional Technical Reference, 1981
	21	K. Malmkjeer, N. Heintze and O. Danvy, "ML Partial Evaluation using Set-Based Analysis", submitted for publication.
	22	Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
	23	Torben Æ Mogensen, Separating binding times in language specifications, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.12-25, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99372]
	24	Flemming Nielson , Hanne Riis Nielson, Two-level functional languages, Cambridge University Press, New York, NY, 1992
	25	O. Shivers, Control flow analysis in scheme, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.164-174, June 20-24, 1988, Atlanta, Georgia, United States
	26	J. Palsberg, Private Communication, November 1993.
	27	Jens Palsberg , Michael I. Schwartzbach, Safety analysis versus type inference for partial types, Information Processing Letters, v.43 n.4, p.175-180, Sept. 28, 1992 [doi>10.1016/0020-0190(92)90196-3]
	28	Jens Palsberg , Michael I. Schwartzbach, Object-oriented type systems, John Wiley and Sons Ltd., Chichester, UK, 1994
	29	J. Reynolds, "Automatic Computation of Data Set Definitions", In/ormation Processing 68, pp. 456-461, North-Holland, 1969.
	30	Andrew K. Wright , Robert Cartwright, A practical soft type system for Scheme, Proceedings of the 1994 ACM conference on LISP and functional programming, p.250-262, June 27-29, 1994, Orlando, Florida, United States