Componential set-based analysis

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Componential set-based analysis

Full text

Pdf (497 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 21 , Issue 2 (March 1999) table of contents

Pages: 370 - 416

Year of Publication: 1999

ISSN:0164-0925

Authors

Cormac Flanagan	Compaq Systems Research Center, Palo Alto, CA
Matthias Felleisen	Rice Univ., Houston, TX

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 24, Citation Count: 11

Additional Information:

abstract references cited by index terms collaborative colleagues peer to peer

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTex EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/316686.316703 What is a DOI?

ABSTRACT

Set-based analysis (SBA) produces good predictions about the behavior of functional and object-oriented programs. The analysis proceeds by inferring constraints that characterize the data flow relationships of the analyzed program. Experiences with MrSpidey, a static debugger based on SBA, indicate that SBA can adequately deal with programs of up to a couple of thousand lines of code. SBA fails, however, to cope with larger programs because it generates systems of constraints that are at least linear, and possibility quadratic, in the size of the analyzed program. This article presents theoretical and practical results concerning methods for reducing the size of constraint systems. The theoretical results include of proof-theoretic characterization of the observable behavior of constraint systems for program components, and a complete algorithm for deciding the observable equivalence of constraint systems. In the course of this development we establish a close connection between the observable equivalence of constraint systems and the equivalence of regular-tree grammars. We then exploit this connection to adapt a variety of algoirthms for simplifying grammars to the problem of simplifying constraint systems. Based on the resulting algorithms, we have developed componential set-based analysis, a modular and polymorphic variant of SBA. Experimental results verify the effectiveness of the simplification algorithms and the componential analysis. The simplified constraint systems are typically an order of magnitude smaller than the original systems. These reductions in size produce significant gains in the speed of the analysis.

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	Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
	2	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]
	3	BARENDREGT, H.P. 1984. The Lambda Calculus: Its Syntax and Semantics, Revised ed. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam.
	4	Patrick Cousot , Radhia Cousot, Formal language, grammar and set-constraint-based program analysis by abstract interpretation, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.170-181, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224199]
	5	DEUTSCH, A. AND HEINTZE, N. 1996. Partial solving of set constraints. Unpublished manuscript.
	6	Evelyn Duesterwald , Rajiv Gupta , Mary Lou Soffa, Reducing the Cost of Data Flow Analysis By Congruence Partitioning, Proceedings of the 5th International Conference on Compiler Construction, p.357-373, April 07-09, 1994
	7	Jonathan Eifrig , Scott Smith , Valery Trifonov, Sound polymorphic type inference for objects, Proceedings of the tenth annual conference on Object-oriented programming systems, languages, and applications, p.169-184, October 15-19, 1995, Austin, Texas, United States
	8	Manuel Fahndrich , Alex Aiken, Making Set-Constraint Program Analyses Scale, University of California at Berkeley, Berkeley, CA, 1996
	9	FLANAGAN, C. 1997. Effective static debugging via componential set-based analysis. Ph.D. thesis, Rice University, Houston, Texas.
	10	Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Stephanie Weirich , Matthias Felleisen, Catching bugs in the web of program invariants, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.23-32, May 21-24, 1996, Philadelphia, Pennsylvania, United States
	11	FLATT, M. 1997. MzScheme reference manual. Technical Report TR97-280, Rice University.
	12	Matthew Flatt , Matthias Felleisen, Units: cool modules for HOT languages, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.236-248, June 17-19, 1998, Montreal, Quebec, Canada
	13	GECSEG, F. AND STEINBY, M. 1984. Tree Automata. Akad6miai Kiadd, Budapest.
	14	Nevin Heintze, Set-based analysis of ML programs, Proceedings of the 1994 ACM conference on LISP and functional programming, p.306-317, June 27-29, 1994, Orlando, Florida, United States
	15	HOPCROFT, J. E. 1971. An n log n algorithm for minimizing the states of a finite automaton. The Theory of Machines and Computations, 189-196.
	16	Suresh Jagannathan , Andrew K. Wright, Effective Flow Analysis for Avoiding Run-Time Checks, Proceedings of the Second International Symposium on Static Analysis, p.207-224, September 25-27, 1995
	17	Neil D. Jones , Steven S. Muchnick, A flexible approach to interprocedural data flow analysis and programs with recursive data structures, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.66-74, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582161]
	18	Jens Palsberg, Closure analysis in constraint form, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.1, p.47-62, Jan. 1995 [doi>10.1145/200994.201001]
	19	Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.367-378, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199533]
	20	PLOTKIN, G. D. 1975. CMl-by-name, cMl-by-vMue, and the N-cMculus. Theor. Comput. Sci. 1, 125-159.
	21	François Pottier, Simplifying subtyping constraints, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.122-133, May 24-26, 1996, Philadelphia, Pennsylvania, United States
	22	REYNOLDS, J. 1969. Automatic computation of data set defintions. Information Processing'68, 456-461.
	23	Mads Tofte, Type inference for polymorphic references, Information and Computation, v.89 n.1, p.1-34, Nov. 1990 [doi>10.1016/0890-5401(90)90018-D]
	24	Valery Trifonov , Scott F. Smith, Subtyping Constrained Types, Proceedings of the Third International Symposium on Static Analysis, p.349-365, September 24-26, 1996
	25	Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093 ]
	26	Andrew K. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, v.8 n.4, p.343-355, Dec. 1995 [doi>10.1007/BF01018828]

CITED BY 11

	Soham Sundar Chakraborty , Rajeev Kumar, Precise static type analysis in component based programming environment, Proceedings of the 1st conference on India software engineering conference, February 19-22, 2008, Hyderabad, India
	Matthias Neubauer , Michael Sperber, Down with Emacs Lisp: dynamic scope analysis, ACM SIGPLAN Notices, v.36 n.10, October 2001
	Oukseh Lee , Kwangkeun Yi , Yunheung Paek, A proof method for the corectness of modularized OCFA, Information Processing Letters, v.81 n.4, p.179-185, 28 February 2002
	Francesco Logozzo, Approximating module semantics with constraints, Proceedings of the 2004 ACM symposium on Applied computing, March 14-17, 2004, Nicosia, Cyprus
	Philippe Meunier , Robert Bruce Findler , Matthias Felleisen, Modular set-based analysis from contracts, ACM SIGPLAN Notices, v.41 n.1, p.218-231, January 2006
	David Herman , Philippe Meunier, Improving the static analysis of embedded languages via partial evaluation, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Philippe Meunier , Robert Bruce Findler , Paul Steckler , Mitchell Wand, Selectors Make Set-Based Analysis Too Hard, Higher-Order and Symbolic Computation, v.18 n.3-4, p.245-269, December 2005
	Sam Tobin-Hochstadt , Matthias Felleisen, Interlanguage migration: from scripts to programs, Companion to the 21st ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
	Matthias Neubauer , Peter Thiemann, Discriminative sum types locate the source of type errors, ACM SIGPLAN Notices, v.38 n.9, p.15-26, September 2003
	Sam Tobin-Hochstadt , Matthias Felleisen, The design and implementation of typed scheme, ACM SIGPLAN Notices, v.43 n.1, January 2008
	Yanhong A. Liu , Scott D. Stoller, Eliminating dead code on recursive data, Science of Computer Programming, v.47 n.2-3, p.221-242, May 2003