Advertisement

Constraint Abstractions

  • Jörgen Gustavsson
  • Josef Svenningsson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2053)

Abstract

Many type based program analyses with subtyping, such as flow analysis, are based on inequality constraints over a lattice. When inequality constraints are combined with polymorphism it is often hard to scale the analysis up to large programs. A major source of inefficiency in conventional implementations stems from computing substitution instances of constraints. In this paper we extend the constraint language with constraint abstractions so that instantiation can be expressed directly in the constraint language and we give a cubic-time algorithm for constraint solving. As an application, we illustrate how a flow analysis with flow subtyping, flow polymorphism and flow-polymorphic recursion can be implemented in O(n 3) time where n is the size of the explicitly typed program.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [AWP97]
    A. Aiken, E. Wimmers, and J. Palsberg. Optimal representation of polymorphic types with subtyping. In Proceedings TACS’97 Theoretical Aspects of Computer Software, pages 47–77. Springer Lecture Notes in Computer Science, vol. 1281, September 1997.CrossRefGoogle Scholar
  2. [BS96]
    E. Barendsen and S. Smetsers. Uniqueness Typing for Functional Languages with Graph Rewriting Semantics. Mathematical Structures in Computer Science, 6:579–612, 1996.zbMATHMathSciNetGoogle Scholar
  3. [CC92]
    P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the Ninthteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 83–94, Albuquerque, New Mexico, January 1992. ACM Press, New York, NY.Google Scholar
  4. [Cur90]
    P. Curtis. Constrained qualification in polymorphic type analysis. Technical Report CSL-09-1, Xerox Parc, February 1990.Google Scholar
  5. [DHM95]
    D. Dussart, F. Henglein, and C. Mossin. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In proceedings of 2nd Static Analysis Symposium, September 1995.Google Scholar
  6. [EST95]
    J. Eifrig, S. Smith, and V. Trifonov. Sound polymorphic type inference for objects. In Proceedings OOPSLA’95, 1995.Google Scholar
  7. [FA96]
    M. Fändrich and A. Aiken. Making set-constraint program analyses scale. In Workshop on Set Constraints, 1996.Google Scholar
  8. [Fax95]
    Karl-Filip Faxén. Optimizing lazy functional programs using flow inference. In Proc. of SAS’95, pages 136–153. Springer-Verlag, LNCS 983, September 1995.Google Scholar
  9. [FF97]
    C. Flanagan and M. Felleisen. Componential set-based analysis. In Proceedings of the ACM SIGPLAN’97 Conference on Programming Language Design and Implementation. ACM, June 1997.Google Scholar
  10. [FFA00]
    J. Foster, M. Fändrich, and A. Aiken. Polymorphic versus Monomorphic Flow-insensitive Points-to Analysis for C. In Proceedings of 2000 Static Analysis Symposium, June 2000.Google Scholar
  11. [FM89]
    Y. Fuh and P. Mishra. Polymorphic subtype inference: Closing the theorypractice gap. In Proceedings of Int’l J’t Conf. on Theory and Practice of Software Development, pages 167–183. Springer-Verlag, March 1989.Google Scholar
  12. [GS00]
    J. Gustavsson and J. Svenningsson. A usage analysis with bounded usage polymorphism and subtyping. In Proceedings of the 12th International Workshop on Implementation of Functional Languages. Springer-Verlag, LNCS, September 2000. To appear.Google Scholar
  13. [Hen93]
    Fritz Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253–289, April 1993.CrossRefGoogle Scholar
  14. [Kae92]
    Stefan Kaes. Type inference in the presence of overloading, subtyping and recursive types. In 1992 ACM conference on LISP and Functional Programming, pages 193–204, San Francisco, CA, 1992. ACM Press.CrossRefGoogle Scholar
  15. [Mos97]
    C. Mossin. Flow Analysis of Typed Higher-Order Programs (Revised Version). PhD thesis, University of Copenhagen, Denmark, August 1997.Google Scholar
  16. [MR00]
    David Melski and Thomas Reps. Interconvertibility of a class of set constraints and context-free language reachability. Theoretical Computer Science, 248, November 2000.Google Scholar
  17. [Pot96]
    F. Pottier. Simplifying subtyping constraints. In Proceedings ICFP’97, International Conference on Functional Programming, pages 122–133. ACM Press, May 1996.Google Scholar
  18. [Reh97]
    J. Rehof. Minimal typings in atomic subtyping. In Proceedings POPL’97, 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 278–291, Paris, France, January 1997. ACM.CrossRefGoogle Scholar
  19. [Rep97]
    T. Reps. Program analysis via graph reachability. In Proc. of ILPS’ 97, pages 5–19. Springer-Verlag, October 1997.Google Scholar
  20. [RF01]
    Jakob Rehof and Manuel Fändrich. Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability. In Proceedings of 2001 Symposium on Principles of Programming Languages, 2001.Google Scholar
  21. [Smi94]
    G. S. Smith. Principal type schemes for functional programs with overloading and subtyping. Science of Computer Programming, 23:197–226, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  22. [Sve00]
    Josef Svenningsson. An efficient algorithm for a sharing analysis with polymorphism and subtyping. Masters thesis, June 2000.Google Scholar
  23. [TS96]
    V. Trifonov and S. Smith. Subtyping constrained types. In Proceedings SAS’96, Static Analysis Symposium, pages 349–365, Aachen, Germany, 1996. Springer Verlag.Google Scholar
  24. [TWM95]
    D. N. Turner, P. Wadler, and C. Mossin. Once upon a type. In Proc. of FPCA, La Jolla, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Jörgen Gustavsson
    • 1
  • Josef Svenningsson
    • 1
  1. 1.Chalmers University of Technology and Göteborg UniversityGermany

Personalised recommendations