Type-base flow analysis: from polymorphic subtyping to CFL-reachability

ABSTRACT

We present a novel approach to scalable implementation of type-based flow analysis with polymorphic subtyping. Using a new presentation of polymorphic subytping with instantiation constraints, we are able to apply context-free language (CFL) reachability techniques to type-based flow analysis. We develop a CFL-based algorithm for computing flow-information in time O(n³), where n is the size of the typed program. The algorithm substantially improves upon the best previously known algorithm for flow analysis based on polymorphic subtyping with complexity O(n⁸). Our technique also yields the first demand-driven algorithm for polymorphic subtype-based flow-computation. It works directly on higher-order programs with structured data of finite type (unbounded data structures are incorporated via finite approximations), supports context-sensitive, global flow summariztion and includes polymorphic recursion.

REFERENCES

• 1: Alexander Aiken , Edward L. Wimmers , Jens Palsberg, Optimal Representations of Polymorphic Types with Subtyping (Extended Abstract), Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, p.47-76, September 23-26, 1997
• 2: [Cur90] P. Curtis. Constrained quantification in polymorphic type analysis. Technical Report CSL- 90-1, Xerox Parc, 1990.
• 3: Dirk Dussart , Fritz Henglein , Christian Mossin, Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time, Proceedings of the Second International Symposium on Static Analysis, p.118-135, September 25-27, 1995
• 4: [DHM95b] Dirk Dussart, Fritz Henglein, and Christian Mossin. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. Unpublished draft, May 1995.
• 5: 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
• 6: [FA96] M. Fähndrich and A. Aiken. Making set-constraint program analyses scale. In Workshop on Set Constraints, Cambridge MA, 1996.
• 7: 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
• 8: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, Polymorphic versus Monomorphic Flow-Insensitive Points-to Analysis for C, Proceedings of the 7th International Symposium on Static Analysis, p.175-198, June 29-July 01, 2000
• 9: You-Chin Fuh , Prateek Mishra, Polymorphic Subtype Inference: Closing the Theory-Practice Gap, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.167-183, March 13-17, 1989
• 10: [FRD00a] M. Fähndrich, J. Rehof, and M. Das. From polymorphic subtyping to CFL reachability: Context-sensitive flow analysis using instantiation constraints. Technical Report MSRTR-99-84, Microsoft Research, 2000. Available at http://research.microsoft.com/~rehof/publications.html.
• 11: Manuel Fähndrich , Jakob Rehof , Manuvir Das, Scalable context-sensitive flow analysis using instantiation constraints, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.253-263, June 18-21, 2000, Vancouver, British Columbia, Canada
• 12: Jörgen Gustavsson , Josef Svenningsson, A Usage Analysis with Bounded Usage Polymorphism and Subtyping, Selected Papers from the 12th International Workshop on Implementation of Functional Languages, p.140-157, September 04-07, 2000
• 13: Nevin Heintze, Control-Flow Analysis and Type Systems, Proceedings of the Second International Symposium on Static Analysis, p.189-206, September 25-27, 1995
• 14: 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]
• 15: Nevin Heintze , David McAllester, Linear-time subtransitive control flow analysis, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.261-272, June 16-18, 1997, Las Vegas, Nevada, United States
• 16: Susan Horwitz , Thomas Reps , Mooly Sagiv, Demand interprocedural dataflow analysis, Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, p.104-115, October 12-15, 1995, Washington, D.C., United States
• 17: Stefan Kaes, Type inference in the presence of overloading, subtyping and recursive types, Proceedings of the 1992 ACM conference on LISP and functional programming, p.193-204, June 22-24, 1992, San Francisco, California, United States
• 18: John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
• 19: [Mose96] Christian Mossin. Flow Analysis of Typed Higher-Order Programs. PhD thesis, DIKU, Department of Computer Science, University of Copenhagen, 1996.
• 20: Christian Mossin, Higher-order value flow graphs, Nordic Journal of Computing, v.5 n.3, p.214-234, Fall 1998
• 21: David Melski , Thomas Reps, Interconvertbility of set constraints and context-free language reachability, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.74-89, June 12-13, 1997, Amsterdam, The Netherlands
• 22: David Melski , Thomas Reps, Interconvertibility of a class of set constraints and context-free-language reachability, Theoretical Computer Science, v.248 n.1-2, p.29-98, October 2000 [doi>10.1016/S0304-3975(00)00049-9]
• 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: Robert O'Callahan , Daniel Jackson, Lackwit: a program understanding tool based on type inference, Proceedings of the 19th international conference on Software engineering, p.338-348, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253351]
• 26: Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.4, p.576-599, July 1995 [doi>10.1145/210184.210187]
• 27: 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
• 28: Jakob Rehof, Minimal typings in atomic subtyping, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.278-291, January 15-17, 1997, Paris, France [doi>10.1145/263699.263738]
• 29: [Reh98] J. Rehof. The Complexity of Simple Subtyping Systems. PhD thesis, Dept. of Computer Science, University of Copenhagen, Denmark, April 1998.
• 30: [Rep98] Thomas Reps. Program analysis via graph reachability. Information and Software Technology , 40 (11-12):701-726, 1998.
• 31: Thomas Reps, Undecidability of context-sensitive data-independence analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.162-186, Jan. 2000 [doi>10.1145/345099.345137]
• 32: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 33: Geoffrey S. Smith, Principal type schemes for functional programs with overloading and subtyping, Science of Computer Programming, v.23 n.2-3, p.197-226, Dec. 1994
• 34: Valery Trifonov , Scott F. Smith, Subtyping Constrained Types, Proceedings of the Third International Symposium on Static Analysis, p.349-365, September 24-26, 1996
• 35: Mihalis Yannakakis, Graph-theoretic methods in database theory, Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.230-242, April 02-04, 1990, Nashville, Tennessee, United States [doi>10.1145/298514.298576]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Classes defined by grammars or automata (e.g., context-free languages, regular sets, recursive sets)

General Terms:
Algorithms, Design, Languages, Performance, Theory, Verification