Polyvariant Flow Analysis with Constrained Types

  • Scott F. Smith
  • Tiejun Wang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)


The basic idea behind improving the quality of a monovariant control flow analysis such as 0CFAis the concept of polyvariant analyses such asAgesen’s Cartesian Product Algorithm (CPA) and Shivers’ nCFA. In this paper we develop a novel framework for polyvariant flow analysis based on Aiken-Wimmers constrained type theory. We develop instantiations of our framework to formalize various polyvariant algorithms, including nCFA and CPA. With our CPA formalization, we show the call-graph based termination condition for CPA will not always guarantee termination. We then develop a novel termination condition and prove it indeed leads to a terminating algorithm. Additionally, we show how data polymorphism can be modeled in the framework, by defining a simple extension to CPA that incorporates data polymorphism.


Type Variable Inference Rule Type Inference Data Polymorphism Call Site 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [1]
    Ole Agesen. The cartesian product algorithm. In Proceedings ECOOP’95, volume 952 of Lecture notes in Computer Science, 1995.Google Scholar
  2. [2]
    Ole Agesen. Concrete Type Inference: Delivering Object-Oriented Applications. PhD thesis, Stanford University, 1996. Available as Sun Labs Technical Report SMLI TR-96-52.Google Scholar
  3. [3]
    A. Aiken and E. L. Wimmers. Type inclusion constraints and type inference. In Proceedings of the International Conference on Functional Programming Languages and Computer Architecture, pages 31–41, 1993.Google Scholar
  4. [4]
    Anindya Bannerjee. A modular, polyvariant, and type-based closure analysis. In International Conference on Functional Programming, 1997.Google Scholar
  5. [5]
    Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. Making the future safe for the past: Adding genericity to the Java programming language. In Proceedings of the 13th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA-98), volume 33, 10 of ACM SIGPLAN Notices, pages 183–200, NewYork, October 18–22 1998. ACM Press.CrossRefGoogle Scholar
  6. [6]
    Jonathan Eifrig, Scott Smith, and Valery Trifonov. Sound polymorphic type inference for objects. In OOPSLA’ 95, pages 169–184, 1995.Google Scholar
  7. [7]
    Jonathan Eifrig, Scott Smith, and Valery Trifonov. Type inference for recursively constrained types and its application to OOP. In Proceedings of the 1995 Mathematical Foundations of Programming Semantics Conference, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995.
  8. [8]
    Cormac Flanagan and Matthias Felleisen. Componential set-based analysis. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI-97), volume 32, 5 of ACMSIGPLAN Notices, pages 235–248, NewYork, June 15–18 1997. ACM Press.CrossRefGoogle Scholar
  9. [9]
    Cormac Flanagan. Effective Static Debugging via Componential Set-Based Analysis. PhD thesis, Rice University, 1997.Google Scholar
  10. [10]
    David Grove, Greg DeFouw, Jerey Dean, and Craig Chambers. Call graph construction in object-oriented languages. In ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 1997.Google Scholar
  11. [11]
    Trevor Jim. What are principal typings and what are they good for? In Conference Record of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, 1996.Google Scholar
  12. [12]
    Suresh Jagannathan and Stephen Weeks. A unified treatment of flow analysis in higher-order languages. In Conference Record of the Twenty-Second Annual ACM Symposium on Principles of Programming Languages, pages 393–408, 1995.Google Scholar
  13. [13]
    Flemming Nielson and Hanne Riis Nielson. Infinitary control flow analysis: A collecting semantics for closure analysis. In Conference Record of the Twenty-Fourth Annual ACM Symposium on Principles of Programming Languages, pages 332–345, 1997.Google Scholar
  14. [14]
    John Plevyak and Andrew Chien. Precise concrete type inference for object-oriented languages. In Proceedings of the Ninth Annual ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, pages 324–340, 1994.Google Scholar
  15. [15]
    François Pottier. A framework for type inference with subtyping. In Proceedings of the ACMSIGPLAN International Conference on Functional Programming (ICFP’ 98), volume 34(1) of ACM SIGPLAN Notices, pages 228–238. ACM, June 1999.Google Scholar
  16. [16]
    Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. In Proceedings of 25th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’98), pages 197–208, 1998.Google Scholar
  17. [17]
    Olin Shivers. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie-Mellon University, 1991. Available as CMU Technical Report CMU-CS-91-145.Google Scholar
  18. [18]
    J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A typed intermediate language for flow-directed compilation. In Theory and Practice of Software Development (TAPSOFT), number 1214 in Lecture notes in Computer Science. Springer-Verlag, 1997.CrossRefGoogle Scholar
  19. [19]
    Andrew K. Wright and Suresh Jagannathan. Polymorphic splitting: an effective polyvariant flow analysis. ACM Transactions on Programming Languages and Systems, 20(1):166–207, January 1998.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Scott F. Smith
    • 1
  • Tiejun Wang
    • 1
  1. 1.Department of Computer ScienceThe Johns Hopkins UniversityBaltimoreUSA

Personalised recommendations