Scalable context-sensitive flow analysis using instantiation constraints

ABSTRACT

This paper shows that a type graph (obtained via polymorphic type inference) harbors explicit directional flow paths between functions. These flow paths arise from the instantiations of polymorphic types and correspond to call-return sequences in first-order programs. We show that flow information can be computed efficiently while considering only paths with well matched call-return sequences, even in the higher-order case. Furthermore, we present a practical algorithm for inferring type instantiation graphs and provide empirical evidence to the scalability of the presented techniques by applying them in the context of points-to analysis for C programs.

REFERENCES

• ASU88: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• CGS+99: Jong-Deok Choi , Manish Gupta , Mauricio Serrano , Vugranam C. Sreedhar , Sam Midkiff, Escape analysis for Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-19, November 01-05, 1999, Denver, Colorado, United States
• CRL99: Ramkrishna Chatterjee , Barbara G. Ryder , William A. Landi, Relevant context inference, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.133-146, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292554]
• DM82: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• FFA00: 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
• FRD00: Manuel Fahndrich, Jakob Rehof, and Manuvir Das. From polymorphic subtyping to CFL reachability: Context-sensitive flow analysis using instantiation constraints. Technical Report MSR- TR-99-84, Microsoft Research, March 2000.
• Hen93: 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]
• HM97: Nevin Heintze , David McAllester, Linear-time subtransitive control flow analysis, ACM SIGPLAN Notices, v.32 n.5, p.261-272, May 1997
• JW95: 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
• KTU93: A. J. Kfoury , J. Tiuryn , P. Urzyczyn, The undecidability of the semi-unification problem, Information and Computation, v.102 n.1, p.83-101, Jan. 1993 [doi>10.1006/inco.1993.1003]
• KTU94: A. J. Kfoury , J. Tiuryn , P. Urzyczyn, An analysis of ML typability, Journal of the ACM (JACM), v.41 n.2, p.368-398, March 1994 [doi>10.1145/174652.174659]
• LH99: Donglin Liang , Mary Jean Harrold, Efficient points-to analysis for whole-program analysis, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.199-215, September 06-10, 1999, Toulouse, France
• Mil78: R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, 1978.
• MR97: David Melski , Thomas Reps, Interconvertbility of set constraints and context-free language reachability, ACM SIGPLAN Notices, v.32 n.12, p.74-89, Dec. 1997
• Myc84: 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
• NN97: Flemming Nielson , Hanne Riis Nielson, Infinitary control flow analysis: a collecting semantics for closure analysis, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.332-345, January 15-17, 1997, Paris, France [doi>10.1145/263699.263745]
• OJ97: 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]
• OOP99: Proceedings of 14th Annual Conference on Object-Oriented Programming, Systems, Languages, and Applications, volume 34, 10 of A CM SIGPLAN Notices. ACM Press, November 1999.
• RHS95: 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]
• Ste96: 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]
• WL95: Robert P. Wilson , Monica S. Lam, Efficient context-sensitive pointer analysis for C programs, ACM SIGPLAN Notices, v.30 n.6, p.1-12, June 1995
• WR99: John Whaley , Martin Rinard, Compositional pointer and escape analysis for Java programs, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.187-206, November 01-05, 1999, Denver, Colorado, United States

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Design