research-article

Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis

Authors:

Yannis Smaragdakis,

David Van HornAuthors Info & Claims

ACM SIGPLAN Notices, Volume 45, Issue 6

Pages 305 - 315

https://doi.org/10.1145/1809028.1806631

Published: 05 June 2010 Publication History

Abstract

Low-level program analysis is a fundamental problem, taking the shape of "flow analysis" in functional languages and "points-to" analysis in imperative and object-oriented languages. Despite the similarities, the vocabulary and results in the two communities remain largely distinct, with limited cross-understanding. One of the few links is Shivers's k-CFA work, which has advanced the concept of "context-sensitive analysis" and is widely known in both communities.

Recent results indicate that the relationship between the functional and object-oriented incarnations of k-CFA is not as well understood as thought. Van Horn and Mairson proved k-CFA for k ≥ 1 to be EXPTIME-complete; hence, no polynomial-time algorithm can exist. Yet, there are several polynomial-time formulations of context-sensitive points-to analyses in object-oriented languages. Thus, it seems that functional k-CFA may actually be a profoundly different analysis from object-oriented k-CFA. We resolve this paradox by showing that the exact same specification of k-CFA is polynomial-time for object-oriented languages yet exponential-time for functional ones: objects and closures are subtly different, in a way that interacts crucially with context-sensitivity and complexity. This illumination leads to an immediate payoff: by projecting the object-oriented treatment of objects onto closures, we derive a polynomial-time hierarchy of context-sensitive CFAs for functional programs.

References

[1]

Andrew W. Appel. Compiling with Continuations. Cambridge University Press, November 1991. ISBN 0-521-41695-7.

Digital Library

[2]

Martin Bravenboer and Yannis Smaragdakis. Strictly declarative specification of sophisticated points-to analyses. In OOPSLA'09: 24th annual ACM SIGPLAN conference on Object Oriented Programming, Systems, Languages, and Applications, 2009.

Digital Library

[3]

Luca Cardelli. Compiling a functional language. In LISP and Functional Programming, pages 208--217, 1984.

Digital Library

[4]

Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 238--252. ACM Press, 1977.

Digital Library

[5]

Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In POPL'79: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 269--282. ACM Press, 1979.

Digital Library

[6]

Jörgen Gustavsson and Josef Svenningsson. Constraint abstractions. In PADO'01: Proceedings of the Second Symposium on Programs as Data Objects, pages 63--83. Springer-Verlag, 2001. ISBN 3-540-42068-1.

Digital Library

[7]

Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst., 23 (3): 396--450, 2001. ISSN 0164-0925.

Digital Library

[8]

Suresh Jagannathan and Stephen Weeks. A unified treatment of flow analysis in higher-order languages. In POPL'95: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 393--407. ACM, 1995. ISBN 0-89791-692-1.

Digital Library

[9]

Ondřej Lhoták. Program Analysis using Binary Decision Diagrams. PhD thesis, McGill University, January 2006.

[10]

Ondřej Lhoták and Laurie Hendren. Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation. ACM Trans. Softw. Eng. Methodol., 18 (1): 1--53, 2008. ISSN 1049-331X.

Digital Library

[11]

Jan Midtgaard. Control-flow analysis of functional programs. Technical Report BRICS RS-07-18, DAIMI, Department of Computer Science, University of Aarhus, December 2007. To appear in revised form in ACM Computing Surveys.

[12]

Matthew Might and Olin Shivers. Environment analysis via Δ-CFA. In POPL'06: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 127--140. ACM, 2006\natexlaba. ISBN 1-59593-027-2.

Digital Library

[13]

Matthew Might and Olin Shivers. Improving flow analyses via Γ-CFA: Abstract garbage collection and counting. In ICFP'06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, pages 13--25. ACM, 2006. ISBN 1-59593-309-3.

Digital Library

[14]

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

[15]

Jakob Rehof and Manuel Fähndrich. Type-base flow analysis: from polymorphic subtyping to CFL-reachability. In POPL'01: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 54--66. ACM, 2001. ISBN 1-58113-336-7.

Digital Library

[16]

Olin Shivers. Higher-order control-flow analysis in retrospect: lessons learned, lessons abandoned. In Kathryn S. McKinley, editor, Best of PLDI 1988, volume 39, pages 257--269. ACM, 2004.

[17]

Olin G. Shivers. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University, 1991.

Digital Library

[18]

David Van Horn and Harry G. Mairson. Relating complexity and precision in control flow analysis. In ICFP'07: Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, pages 85--96. ACM, 2007. ISBN 9781-59593-815-2.

Digital Library

[19]

David Van Horn and Harry G. Mairson. Deciding k-CFA is complete for EXPTIME. In ICFP'08: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, pages 275--282. ACM, 2008. ISBN 9781-595-9391-9-7.

Digital Library

Cited By

Bračevac OWei GJia SAbeysinghe SJiang YBao YRompf T(2023)Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect DependenciesProceedings of the ACM on Programming Languages10.1145/36228137:OOPSLA2(400-430)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622813
Germane K(2023)m-CFA Exhibits Perfect Stack PrecisionProgramming Languages and Systems10.1007/978-981-99-8311-7_14(290-309)Online publication date: 21-Nov-2023
https://doi.org/10.1007/978-981-99-8311-7_14
Zhang QSu Z(2017)Context-sensitive data-dependence analysis via linear conjunctive language reachabilityACM SIGPLAN Notices10.1145/3093333.300984852:1(344-358)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009848
Show More Cited By

Index Terms

Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

Recommendations

Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis
PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation

Low-level program analysis is a fundamental problem, taking the shape of "flow analysis" in functional languages and "points-to" analysis in imperative and object-oriented languages. Despite the similarities, the vocabulary and results in the two ...
Precise flow-insensitive may-alias analysis is NP-hard

Determining aliases is one of the foundamental static analysis problems, in part because the precision with which this problem is solved can affect the precision of other analyses such as live variables, available expressions, and constant propagation. ...
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 SIGPLAN Notices

ACM SIGPLAN Notices Volume 45, Issue 6

PLDI '10

June 2010

496 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1809028

Issue’s Table of Contents

PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2010
514 pages
ISBN:9781450300193
DOI:10.1145/1806596
General Chair:
Ben Zorn
Microsoft Research
,
Program Chair:
Alex Aiken
Stanford University

Copyright © 2010 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 June 2010

Published in SIGPLAN Volume 45, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

63
Total Citations
View Citations
782
Total Downloads

Downloads (Last 12 months)44
Downloads (Last 6 weeks)5

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bračevac OWei GJia SAbeysinghe SJiang YBao YRompf T(2023)Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect DependenciesProceedings of the ACM on Programming Languages10.1145/36228137:OOPSLA2(400-430)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622813
Germane K(2023)m-CFA Exhibits Perfect Stack PrecisionProgramming Languages and Systems10.1007/978-981-99-8311-7_14(290-309)Online publication date: 21-Nov-2023
https://doi.org/10.1007/978-981-99-8311-7_14
Zhang QSu Z(2017)Context-sensitive data-dependence analysis via linear conjunctive language reachabilityACM SIGPLAN Notices10.1145/3093333.300984852:1(344-358)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009848
Zhang QSu ZCastagna GGordon A(2017)Context-sensitive data-dependence analysis via linear conjunctive language reachabilityProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009848(344-358)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009848
Feng YAnand SDillig IAiken ACheung SOrso AStorey M(2014)Apposcopy: semantics-based detection of Android malware through static analysisProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2635868.2635869(576-587)Online publication date: 11-Nov-2014
https://dl.acm.org/doi/10.1145/2635868.2635869
Grech NRathke JFischer B(2013)Preemptive Type Checking in Dynamically Typed LanguagesTheoretical Aspects of Computing – ICTAC 201310.1007/978-3-642-39718-9_12(195-212)Online publication date: 2013
https://doi.org/10.1007/978-3-642-39718-9_12
Kastrinis GSmaragdakis Y(2013)Efficient and effective handling of exceptions in java points-to analysisProceedings of the 22nd international conference on Compiler Construction10.1007/978-3-642-37051-9_3(41-60)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-37051-9_3
Madhavan RRamalingam GVaswani K(2012)Modular heap analysis for higher-order programsProceedings of the 19th international conference on Static Analysis10.1007/978-3-642-33125-1_25(370-387)Online publication date: 11-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-33125-1_25
Ryder BWiedermann B(2012)Language design and analyzabilitySoftware—Practice & Experience10.1002/spe.113342:1(3-18)Online publication date: 1-Jan-2012
https://dl.acm.org/doi/10.1002/spe.1133
Hong JRyu S(2024)Don’t Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust TranslationProceedings of the ACM on Programming Languages10.1145/36564068:PLDI(716-740)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656406
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 Issue’s Table of Contents