Article

Relating complexity and precision in control flow analysis

Authors:

David Van Horn,

Harry G. MairsonAuthors Info & Claims

ICFP '07: Proceedings of the 12th ACM SIGPLAN international conference on Functional programming

Pages 85 - 96

https://doi.org/10.1145/1291151.1291166

Published: 01 October 2007 Publication History

Abstract

We analyze the computational complexity of kCFA, a hierarchy of control flow analyses that determine which functions may be applied at a given call-site. This hierarchy specifies related decision problems, quite apart from any algorithms that may implement their solutions. We identify a simple decision problem answered by this analysis and prove that in the 0CFA case, the problem is complete for polynomial time. The proof is based on a nonstandard, symmetric implementation of Boolean logic within multiplicative linear logic (MLL). We also identify a simpler version of 0CFA related to η-expansion, and prove that it is complete for logarithmic space, using arguments based on computing paths and permutations.

For any fixed k>0, it is known that kCFA (and the analogous decision problem) can be computed in time exponential in the program size. For k=1, we show that the decision problem is NP-hard, and sketch why this remains true for larger fixed values of k. The proof technique depends on using the approximation of CFA as an essentially nondeterministic computing mechanism, as distinct from the exactness of normalization. When k=n, so that the "depth" of the control flow analysis grows linearly in the program length, we show that the decision problem is complete for exponential time.

In addition, we sketch how the analysis presented here may be extended naturally to languages with control operators. All of the insights presented give clear examples of how straightforward observations about linearity, and linear logic, may in turn be used to give a greater understanding of functional programming and program analysis.

References

[1]

Andrea Asperti and Cosimo Laneve. Paths, computations and labels in the lambda-calculus. Theor. Comput. Sci., 142(2): 277--297, 1995.

Digital Library

[2]

Andrea Asperti and Harry G. Mairson. Parallel beta reduction is not elementary recursive. In POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 303--315. ACM Press, 1998.

Digital Library

[3]

Anindya Banerjee. A modular, polyvariant and type-based closure analysis. In ICFP '97: Proceedings of the second ACM SIGPLAN international conference on Functional programming, pages 1--10. ACM Press, 1997.

Digital Library

[4]

Anindya Banerjee and Thomas Jensen. Modular control-flow analysis with rank 2 intersection types. Mathematical Structures in Comp. Sci., 13(1): 87--124, 2003.

Digital Library

[5]

Olivier Danvy and Andrzej Filinski. Abstracting control. In LFP '90: Proceedings of the 1990 ACM conference on LISP and functional programming, pages 151-160. ACM Press, 1990.

Digital Library

[6]

Karl-Filip Faxén. Polyvariance, polymorphism and flow analysis. In Selected papers from the 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, pages 260--278. Springer-Verlag, 1997.

[7]

Karl-Filip Faxén. Optimizing lazy functional programs using flow inference. In SAS '95: Proceedings of the Second International Symposium on Static Analysis, pages 136--153. Springer-Verlag, 1995.

Digital Library

[8]

Andrzej Filinski. Declarative continuations: an investigation of duality in programming language semantics. In Category Theory and Computer Science, pages 224--249. Springer-Verlag, 1989.

[9]

Jean-Yves Girard. Geometry of interaction I: Interpretation of System F. In C. Bonotto, editor, Logic Colloquium '88, pages 221--260. North Holland, 1989.

[10]

Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types. Cambridge University Press, New York, NY, USA, 1989.

Digital Library

[11]

Timothy G. Griffin. A formulae-as-type notion of control. In POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 47--58. ACM Press, 1990.

Digital Library

[12]

Nevin Heintze. Set-based analysis of ML programs. In LFP '94: Proceedings of the 1994 ACM conference on LISP and functional programming, pages 306--317. ACM Press, 1994.

Digital Library

[13]

Nevin Heintze. Control-flow analysis and type systems. In SAS '95: Proceedings of the Second International Symposium on Static Analysis, pages 189--206. Springer-Verlag, 1995.

Digital Library

[14]

Nevin Heintze and David McAllester. On the cubic bottleneck in subtyping and flow analysis. In LICS '97: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, page 342. IEEE Computer Society, 1997.

Digital Library

[15]

Nevin Heintze and David McAllester. Linear-time subtransitive control flow analysis. In PLDI '97: Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, pages 261--272. ACM Press, 1997.

Digital Library

[16]

Fritz Henglein and Harry G. Mairson. The complexity of type inference for higher-order lambda calculi. In POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 119--130. ACM Press, 1991.

Digital Library

[17]

Neil D. Jones. Flow analysis of lambda expressions (preliminary version). In Proceedings of the 8th Colloquium on Automata, Languages and Programming, pages 114--128. Springer-Verlag, 1981.

Digital Library

[18]

Richard E. Ladner. The circuit value problem is log space complete for P. SIGACT News, 7(1): 18--20, 1975.

Digital Library

[19]

Yves Lafont. From proof-nets to interaction nets. In Proceedings of the workshop on Advances in linear logic, pages 225--247. Cambridge University Press, 1995.

Digital Library

[20]

Julia L. Lawall and Harry G. Mairson. Sharing continuations: Proofnets for languages with explicit control. In ESOP '00: Proceedings of the 9th European Symposium on Programming Languages and Systems, pages 245--259. Springer-Verlag, 2000.

Digital Library

[21]

Jean-Jacques Lévy. Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Paris 7, January 1978. thése d'Etat.

[22]

Harry G. Mairson. From Hilbert spaces to Dilbert spaces: Context semantics made simple. In FST TCS '02: Proceedings of the 22nd Conference Kanpur on Foundations of Software Technology and Theoretical Computer Science, pages 2--17. Springer-Verlag, 2002.

Digital Library

[23]

Harry G. Mairson. From Hilbert space to Dilbert space: context semantics as a language for games and flow analysis. In ICFP '03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, pages 125--125. ACM Press, 2003.

Digital Library

[24]

Harry G. Mairson. Linear lambda calculus and PTIME-completeness. Journal of Functional Programming, 14(6): 623--633, 2004.

Digital Library

[25]

Harry G. Mairson. Deciding ML typability is complete for deterministic exponential time. In POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 382--401. ACM Press, 1990.

Digital Library

[26]

Harry G. Mairson. Axiom-sensitive normalization bounds for multiplicative linear logic, 2006. Unpublished manuscript.

[27]

Harry G. Mairson. A simple proof of a theorem of Statman. Theoretical Computer Science, 103(2): 387--394, 1992.

Digital Library

[28]

Harry G. Mairson and Kazushige Terui. On the computational complexity of cut-elimination in linear logic. In Carlo Blundo and Cosimo Laneve, editors, ICTCS, volume 2841 of Lecture Notes in Computer Science, pages 23--36. Springer, 2003.

[29]

Christian Mossin. Flow Analysis of Typed Higher-Order Programs. PhD thesis, DIKU, University of Copenhagen, January (revised August) 1997.

[30]

Christian Mossin. Exact flow analysis. In SAS '97: Proceedings of the 4th International Symposium on Static Analysis, pages 250--264. Springer-Verlag, 1997.

Digital Library

[31]

Peter Møller Neergaard and Harry G. Mairson. Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, pages 138--149. ACM Press, 2004.

Digital Library

[32]

Flemming Nielson and Hanne Riis Nielson. Infinitary control flow analysis: a collecting semantics for closure analysis. In POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 332--345. ACM Press, 1997.

Digital Library

[33]

Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1999.

Digital Library

[34]

Jens Palsberg. Closure analysis in constraint form. ACM Trans. Program. Lang. Syst., 17(1): 47--62, 1995.

Digital Library

[35]

Jens Palsberg and Patrick O'Keefe. A type system equivalent to flow analysis. ACM Trans. Program. Lang. Syst., 17(4): 576--599, 1995.

Digital Library

[36]

Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. In POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 197--208. ACM Press, 1998.

Digital Library

[37]

Michel Parigot. Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, LPAR, volume 624 of Lecture Notes in Computer Science, pages 190--201. Springer, 1992.

Digital Library

[38]

Thomas Reps. Undecidability of context-sensitive data-independence analysis. ACM Trans. Program. Lang. Syst., 22(1): 162--186, 2000.

Digital Library

[39]

Peter Sestoft. Replacing function parameters by global variables. In FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture, pages 39--53. ACM Press, 1989.

Digital Library

[40]

Peter Sestoft. Replacing function parameters by global variables. Master's thesis, DIKU, University of Copenhagen, Denmark, Oct 1988. Master's thesis no. 254.

[41]

Olin Shivers. Control-flow analysis of higher-order languages of taming lambda. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 1991.

Digital Library

[42]

Olin Shivers. Higher-order control-flow analysis in retrospect: lessons learned, lessons abandoned. SIGPLAN Not., 39(4): 257--269, 2004.

Digital Library

[43]

Richard Statman. The typed λ-calculus is not elementary recursive. Theor. Comput. Sci., 9: 73--81, 1979.

[44]

Yan Mei Tang and Pierre Jouvelot. Separate abstract interpretation for control-flow analysis. In TACS '94: Proceedings of the International Conference on Theoretical Aspects of Computer Software, pages 224--243. Springer-Verlag, 1994.

Digital Library

[45]

Kazushige Terui. On the complexity of cut-elimination in linear logic, July 2002. Invited talk at LL2002 (LICS2002 affiliated workshop),. Copenhagen.

[46]

Andrew K. Wright and Suresh Jagannathan. Polymorphic splitting: an effective polyvariant flow analysis. ACM Trans. Program. Lang. Syst., 20(1): 166--207, 1998.

Digital Library

Cited By

Facchinetti LPalmer ZSmith S(2019)Higher-order Demand-driven Program AnalysisACM Transactions on Programming Languages and Systems10.1145/331034041:3(1-53)Online publication date: 2-Jul-2019
https://dl.acm.org/doi/10.1145/3310340
Park CLee HRyu S(2017)Static analysis of JavaScript libraries in a scalable and precise way using loop sensitivitySoftware: Practice and Experience10.1002/spe.255248:4(911-944)Online publication date: 23-Oct-2017
https://doi.org/10.1002/spe.2552
Matsuoka S(2016)Strong Typed Böhm Theorem and Functional Completeness on the Linear Lambda CalculusElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.207.1207(1-22)Online publication date: 1-Apr-2016
https://doi.org/10.4204/EPTCS.207.1
Show More Cited By

Recommendations

Relating complexity and precision in control flow analysis
Proceedings of the ICFP '07 conference

We analyze the computational complexity of kCFA, a hierarchy of control flow analyses that determine which functions may be applied at a given call-site. This hierarchy specifies related decision problems, quite apart from any algorithms that may ...
The Landscape of Communication Complexity Classes

We prove several results which, together with prior work, provide a nearly-complete picture of the relationships among classical communication complexity classes between $${\mathsf{P}}$$P and $${\mathsf{PSPACE}}$$PSPACE, short of proving lower bounds ...
Pushdown control-flow analysis for free
POPL '16

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '07: Proceedings of the 12th ACM SIGPLAN international conference on Functional programming

October 2007

346 pages

ISBN:9781595938152

DOI:10.1145/1291151

General Chair:
Ralf Hinze
Universität Bonn, Germany
,
Program Chair:
Norman Ramsey
Harvard University, USA

ACM SIGPLAN Notices Volume 42, Issue 9
Proceedings of the ICFP '07 conference
September 2007
331 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1291220
Issue’s Table of Contents

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICFP07

Sponsor:

ICFP07: ACM SIGPLAN International Conference on Functional Programming

October 1 - 3, 2007

Freiburg, Germany

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
301
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Facchinetti LPalmer ZSmith S(2019)Higher-order Demand-driven Program AnalysisACM Transactions on Programming Languages and Systems10.1145/331034041:3(1-53)Online publication date: 2-Jul-2019
https://dl.acm.org/doi/10.1145/3310340
Park CLee HRyu S(2017)Static analysis of JavaScript libraries in a scalable and precise way using loop sensitivitySoftware: Practice and Experience10.1002/spe.255248:4(911-944)Online publication date: 23-Oct-2017
https://doi.org/10.1002/spe.2552
Matsuoka S(2016)Strong Typed Böhm Theorem and Functional Completeness on the Linear Lambda CalculusElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.207.1207(1-22)Online publication date: 1-Apr-2016
https://doi.org/10.4204/EPTCS.207.1
Cortesi AFerrara PChaki N(2013)Static analysis techniques for robotics software verificationIEEE ISR 201310.1109/ISR.2013.6739742(1-6)Online publication date: Oct-2013
https://doi.org/10.1109/ISR.2013.6739742
Lyde SMight M(2013)Control-Flow Analysis with SAT SolversRevised Selected Papers of the 14th International Symposium on Trends in Functional Programming - Volume 832210.1007/978-3-642-45340-3_8(125-133)Online publication date: 14-May-2013
https://dl.acm.org/doi/10.1007/978-3-642-45340-3_8
Midtgaard J(2012)Control-flow analysis of functional programsACM Computing Surveys10.1145/2187671.218767244:3(1-33)Online publication date: 14-Jun-2012
https://dl.acm.org/doi/10.1145/2187671.2187672
Prabhu TRamalingam SMight MHall MBall TSagiv M(2011)EigenCFAProceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1926385.1926445(511-522)Online publication date: 26-Jan-2011
https://dl.acm.org/doi/10.1145/1926385.1926445
Prabhu TRamalingam SMight MHall M(2011)EigenCFAACM SIGPLAN Notices10.1145/1925844.192644546:1(511-522)Online publication date: 26-Jan-2011
https://dl.acm.org/doi/10.1145/1925844.1926445
Might MSmaragdakis YVan Horn D(2010)Resolving and exploiting the k-CFA paradoxACM SIGPLAN Notices10.1145/1809028.180663145:6(305-315)Online publication date: 5-Jun-2010
https://dl.acm.org/doi/10.1145/1809028.1806631
Might MSmaragdakis YVan Horn DZorn BAiken A(2010)Resolving and exploiting the k-CFA paradoxProceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1806596.1806631(305-315)Online publication date: 5-Jun-2010
https://dl.acm.org/doi/10.1145/1806596.1806631
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents