Type-based analysis of uncaught exceptions

ABSTRACT

This article presents a program analysis to estimate uncaught exceptions in ML programs. This analysis relies on unification-based type inference in a nonstandard type system, using rows to approximate both the flow of escaping exceptions (a la effect systems) and the flow of result values (a la control-flow analyses). The resulting analysis is efficient and precise; in particular, arguments carried by exceptions are accurately handled.

REFERENCES

• 1: Henry G. Baker, Unify and conquer, Proceedings of the 1990 ACM conference on LISP and functional programming, p.218-226, June 27-29, 1990, Nice, France [doi>10.1145/91556.91652]
• 2: Robert Cartwright , Matthias Felleisen, Program verification through soft typing, ACM Computing Surveys (CSUR), v.28 n.2, p.349-351, June 1996 [doi>10.1145/234528.234747]
• 3: Allyn Dimock , Robert Muller , Franklyn Turbak , J. B. Wells, Strongly typed flow-directed representation transformations (extended abstract), Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.11-24, June 09-11, 1997, Amsterdam, The Netherlands
• 4: Peter Harry Eidorff , Fritz Henglein , Christian Mossin , Henning Niss , Morten Heine Sørensen , Mads Tofte, AnnoDomini: from type theory to Year 2000 conversion tool, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292543]
• 5: Manuel Fahndrich , Alex Aiken, Making Set-Constraint Program Analyses Scale, University of California at Berkeley, Berkeley, CA, 1996
• 6: Manuel Fähndrich , Alexander Aiken, Program Analysis Using Mixed Term and Set Constraints, Proceedings of the 4th International Symposium on Static Analysis, p.114-126, September 08-10, 1997
• 7: Manuel Fahndrich , Jeffrey Foster , Jason Cu , Alexander Aiken, Tracking down Exceptions in Standard ML Programs, University of California at Berkeley, Berkeley, CA, 1998
• 8: Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su , Alexander Aiken, Partial online cycle elimination in inclusion constraint graphs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.85-96, June 17-19, 1998, Montreal, Quebec, Canada
• 9: Cormac Flanagan , Matthias Felleisen, Componential set-based analysis, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.235-248, June 16-18, 1997, Las Vegas, Nevada, United States
• 10: Tim Freeman , Frank Pfenning, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.268-277, June 24-28, 1991, Toronto, Ontario, Canada
• 11: Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
• 12: GUZMJ~N, J. C. AND SUJ~REZ, A. 1994. A type system for exceptions. In Proc. 199g workshop on ML and its applications. Research report 2265, INRIA, 127-135.
• 13: 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
• 14: Fritz Henglein, Global tagging optimization by type inference, Proceedings of the 1992 ACM conference on LISP and functional programming, p.205-215, June 22-24, 1992, San Francisco, California, United States
• 15: Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
• 16: Andrew K. Wright , Suresh Jagannathan, Polymorphic splitting: an effective polyvariant flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.166-207, Jan. 1998 [doi>10.1145/271510.271523]
• 17: A. J. Kfoury , J. Tiuryn , P. Urzyczyn, Type reconstruction in the presence of polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.290-311, April 1993 [doi>10.1145/169701.169687]
• 18: A. J. Kfoury , J. B. Wells, Principality and decidable type inference for finite-rank intersection types, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-174, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292556]
• 19: K. Rustan M. Leino , Greg Nelson, An Extended Static Checker for Modular-3, Proceedings of the 7th International Conference on Compiler Construction, p.302-305, March 28-April 04, 1998
• 20: LEROY, X., VOUILLON, J., AND DOLIGEZ, D. 1996. The Objective Caml system. Software and documentation available on the Web, http ://cam1. inria, fr/ocaml/.
• 21: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 22: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
• 23: Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
• 24: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 25: Atsushi Ohori, A polymorphic record calculus and its compilation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.6, p.844-895, Nov. 1995 [doi>10.1145/218570.218572]
• 26: PESSAUX, F. 1999. D6tection statique d'exceptions non rattrap6es en Objective Caml. Ph.D. thesis, Universit6 Paris 6.
• 27: François Pottier, A framework for type inference with subtyping, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.228-238, September 26-29, 1998, Baltimore, Maryland, United States
• 28: POTTIER, F. 1998. Type inference in the presence of subtyping: from theory to practice. Research report 3483, INRIA. Sept.
• 29: G. Ramalingam , John Field , Frank Tip, Aggregate structure identification and its application to program analysis, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-132, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292553]
• 30: D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.77-88, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75284]
• 31: REMY, D. 1993a. Syntactic theories and the algebra of record terms. Research report 1869, INRIA.
• 32: Didier Rémy, Type inference for records in natural extension of ML, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• 33: Didier Rémy , Jérôme Vouillon, Objective ML: an effective object-oriented extension to ML, Theory and Practice of Object Systems, v.4 n.1, p.27-50, 1998 [doi>10.1002/(SICI)1096-9942(1998)4:1<27::AID-TAPO3>3.0.CO;2-4]
• 34: Zhong Shao , Andrew W. Appel, Smartest recompilation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.439-450, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158702]
• 35: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 1991
• 36: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 37: Jean-Pierre Talpin , Pierre Jouvelot, The type and effect discipline, Information and Computation, v.111 n.2, p.245-296, June 1994 [doi>10.1006/inco.1994.1046]
• 38: Mads Tofte , Lars Birkedal, A region inference algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.4, p.724-767, July 1998 [doi>10.1145/291891.291894]
• 39: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• 40: WAND, M. 1987. Complete type inference for simple objects. In Logic in Computer Science 1987. IEEE Computer Society Press, 37-44.
• 41: Andrew K. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, v.8 n.4, p.343-355, Dec. 1995 [doi>10.1007/BF01018828]
• 42: Andrew K. Wright , Robert Cartwright, A practical soft type system for scheme, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.1, p.87-152, Jan. 1997 [doi>10.1145/239912.239917]
• 43: 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]
• 44: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]
• 45: Kwangkeun Yi, An abstract interpretation for estimating uncaught exceptions in standard ML programs, Science of Computer Programming, v.31 n.1, p.147-173, May 1998 [doi>10.1016/S0167-6423(96)00044-5]
• 46: Kwangkeun Yi , Sukyoung Ryu, Towards a Cost-Effective Estimation of Uncaught Exceptions in SML Programs, Proceedings of the 4th International Symposium on Static Analysis, p.98-113, September 08-10, 1997

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Error handling and recovery; Symbolic execution
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages
          Nouns: ML

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis; Operational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Control primitives

General Terms:
Languages, Reliability, Theory

Keywords:
SML, caml, exceptions, polymorphism, rows, static debugging, type and effect systems, type inference