Deciding kCFA is complete for EXPTIME

ABSTRACT

We give an exact characterization of the computational complexity of the kCFA hierarchy. For any k > 0, we prove that the control flow decision problem is complete for deterministic exponential time. This theorem validates empirical observations that such control flow analysis is intractable. It also provides more general insight into the complexity of abstract interpretation.

REFERENCES

• 1: G. L. Burn , C. L. Hankin , S. Abramsky, The theory of strictness analysis for higher order functions, on Programs as data objects, p.42-62, April 1986, Copenhagen, Denmark
• 2: Haim Gaifman , Harry Mairson , Yehoshua Sagiv , Moshe Y. Vardi, Undecidable optimization problems for database logic programs, Journal of the ACM (JACM), v.40 n.3, p.683-713, July 1993 [doi>10.1145/174130.174142]
• 3: Fritz Henglein. Simple closure analysis. DIKU Semantics Report D-193, March 1992.
• 4: Gerd G. Hillebrand, Paris C. Kanellakis, Harry G. Mairson, and Moshe Y. Vardi. Undecidable boundedness problems for datalog programs. J. Logic Program., 25(2):163--190, 1995.
• 5: Suresh Jagannathan , Peter Thiemann , Stephen Weeks , Andrew Wright, Single and loving it: must-alias analysis for higher-order languages, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.329-341, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268973]
• 6: Neil D. Jones, Flow Analysis of Lambda Expressions (Preliminary Version), Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.114-128, July 13-17, 1981
• 7: Richard E. Ladner, The circuit value problem is log space complete for P, ACM SIGACT News, v.7 n.1, p.18-20, January 1975 [doi>10.1145/990518.990519]
• 8: Jean-Jacques Lévy. Réductions correctes et optimales dans le lambdacalcul. PhD thesis, Paris 7, January 1978. Thèse d'Etat.
• 9: Harry G. Mairson, Linear lambda calculus and PTIME-completeness, Journal of Functional Programming, v.14 n.6, p.623-633, November 2004 [doi>10.1017/S0956796804005131]
• 10: Harry G. Mairson, Deciding ML typability is complete for deterministic exponential time, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.382-401, December 1989, San Francisco, California, United States [doi>10.1145/96709.96748]
• 11: Jan Midtgaard. Control-flow analysis of functional programs. Technical Report BRICS RS-07-18, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 2007.
• 12: Matthew Might , Olin G. Shivers, Environment analysis of higher-order languages, Georgia Institute of Technology, Atlanta, GA, 2007
• 13: Matthew Might , Olin Shivers, Improving flow analyses via ΓCFA: abstract garbage collection and counting, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 14: Christian Mossin, Exact Flow Analysis, Proceedings of the 4th International Symposium on Static Analysis, p.250-264, September 08-10, 1997
• 15: Peter Møller Neergaard , Harry G. Mairson, Types, potency, and idempotency: why nonlinearity and amnesia make a type system work, Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, September 19-21, 2004, Snow Bird, UT, USA
• 16: 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]
• 17: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 18: Peter Sestoft. Replacing function parameters by global variables. Master's thesis, DIKU, University of Copenhagen, Denmark, October 1988. Master's thesis no. 254.
• 19: O. Shivers, Control flow analysis in scheme, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.164-174, June 20-24, 1988, Atlanta, Georgia, United States
• 20: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 1991
• 21: Olin Shivers, Higher-order control-flow analysis in retrospect: lessons learned, lessons abandoned, ACM SIGPLAN Notices, v.39 n.4, April 2004 [doi>10.1145/989393.989421]
• 22: David Van Horn , Harry G. Mairson, Relating complexity and precision in control flow analysis, Proceedings of the 12th ACM SIGPLAN international conference on Functional programming, October 01-03, 2007, Freiburg, Germany
• 23: David Horn , Harry G. Mairson, Flow Analysis, Linearity, and PTIME, Proceedings of the 15th international symposium on Static Analysis, July 16-18, 2008, Valencia, Spain [doi>10.1007/978-3-540-69166-2_17]
• 24: 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]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computability theory; Computational logic; Lambda calculus and related systems

General Terms:
Languages, Theory

Keywords:
complexity, flow analysis