article

Public Access

Pushdown control-flow analysis for free

Authors:

Michael D. Adams,

David Van HornAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 1

Pages 691 - 704

https://doi.org/10.1145/2914770.2837631

Published: 11 January 2016 Publication History

Abstract

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 published that provide perfect call-stack precision in a computable manner: CFA2, PDCFA, and AAC. Unfortunately, implementing CFA2 and PDCFA requires significant engineering effort. Furthermore, all three are computationally expensive. For a monovariant analysis, CFA2 is in O(2^n), PDCFA is in O(n^6), and AAC is in O(n^8). In this paper, we describe a new technique that builds on these but is both straightforward to implement and computationally inexpensive. The crucial insight is an unusual state-dependent allocation strategy for the addresses of continuations. Our technique imposes only a constant-factor overhead on the underlying analysis and costs only O(n^3) in the monovariant case. We present the intuitions behind this development, benchmarks demonstrating its efficacy, and a proof of the precision of this analysis.

References

[1]

P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming, pages 106–130. Paris, France, 1976.

[2]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages, POPL ’77, pages 238–252, New York, NY, USA, Jan. 1977. ACM.

Digital Library

[3]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’79, pages 269–282, New York, NY, USA, Jan. 1979. ACM.

Digital Library

[4]

C. Earl, M. Might, and D. Van Horn. Pushdown control-flow analysis of higher-order programs: Precise, polyvariant and polynomial-time. In Scheme Workshop, August 2010.

[5]

C. Earl, I. Sergey, M. Might, and D. Van Horn. Introspective pushdown analysis of higher-order programs. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP ’12, pages 177–188, New York, NY, USA, Sept. 2012.

Digital Library

[6]

ACM. ISBN 978-1-4503-1054-3.

[7]

C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, PLDI ’93, pages 237–247, New York, NY, USA, Aug. 1993.

Digital Library

[8]

ACM. ISBN 0-89791-598-4.

[9]

J. I. Johnson. AAC complexity analysis discussion. Unpublished correspondence, June 2015.

[10]

J. I. Johnson and D. Van Horn. Abstracting abstract control. In Proceedings of the 10th ACM Symposium on Dynamic Languages, DLS ’14, pages 11–22, New York, NY, USA, Oct. 2014. ACM. ISBN 978-1-4503-3211-8.

Digital Library

[11]

J. I. Johnson, N. Labich, M. Might, and D. Van Horn. Optimizing abstract abstract machines. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP ’13, pages 443–454, New York, NY, USA, Sept. 2013. ACM. ISBN 978- 1-4503-2326-0.

Digital Library

[12]

J. Midtgaard. Control-flow analysis of functional programs. ACM Computing Surveys (CSUR), 44(3):10:1–10:33, June 2012.

Digital Library

[13]

ISSN 0360-0300.

[14]

M. Might. Environment Analysis of Higher-Order Languages. PhD thesis, Georgia Institute of Technology, Atlanta, GA, 2007.

Digital Library

[15]

M. Might. Abstract interpreters for free. In R. Cousot and M. Martel, editors, Proceedings of the Static Analysis Symposium, volume 6337 of Lecture Notes in Computer Science, pages 407–421. Springer Berlin Heidelberg, 2010. ISBN 978-3-642-15768-4. 642-15769-1_25.

Digital Library

[16]

M. Might, Y. Smaragdakis, and D. Van Horn. Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’10, pages 305–315, New York, NY, USA, June 2010. ACM. ISBN 978-1- 4503-0019-3.

Digital Library

[17]

A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285–309, 1955.

[18]

D. Van Horn and M. Might. Abstracting abstract machines. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP ’10, pages 51–62, New York, NY, USA, Sept. 2010. ACM. ISBN 978-1-60558-794-3.

Digital Library

[19]

D. Vardoulakis and O. Shivers. CFA2: A context-free approach to control-flow analysis. In A. D. Gordon, editor, Proceedings of the European Symposium on Programming, volume 6012 of Lecture Notes in Computer Science, pages 570–589. Springer Berlin Heidelberg, 2010. ISBN 978-3-642-11956-9. 6_30.

Digital Library

Cited By

GILRAY TADAMS MMIGHT M(2018)Abstract allocation as a unified approach to polyvariance in control-flow analysesJournal of Functional Programming10.1017/S095679681800013828Online publication date: 1-Aug-2018
https://doi.org/10.1017/S0956796818000138
Nicolay JStiévenart QDe Meuter WDe Roover C(2017)Purity analysis for JavaScript through abstract interpretationJournal of Software: Evolution and Process10.1002/smr.188929:12(e1889)Online publication date: 25-Aug-2017
https://doi.org/10.1002/smr.1889
Stiévenart QNicolay JDe Meuter WDe Roover CBiboudis AJonnalagedda MStucki SUreche V(2016)Building a modular static analysis framework in Scala (tool paper)Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala10.1145/2998392.3001579(105-109)Online publication date: 30-Oct-2016
https://dl.acm.org/doi/10.1145/2998392.3001579
Show More Cited By

Index Terms

Pushdown control-flow analysis for free
1. Software and its engineering
  1. Software notations and tools
    1. Compilers

Recommendations

Pushdown control-flow analysis for free
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

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 ...
Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis
ICFP '16

The polyvariance of a static analysis is the degree to which it structurally differentiates approximations of program values. Polyvariant techniques come in a number of different flavors that represent alternative heuristics for managing the trade-off ...
Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

The polyvariance of a static analysis is the degree to which it structurally differentiates approximations of program values. Polyvariant techniques come in a number of different flavors that represent alternative heuristics for managing the trade-off ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 1

POPL '16

January 2016

815 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2914770

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2016
815 pages
ISBN:9781450335492
DOI:10.1145/2837614
General Chair:
Rastislav Bodik
UC Berkeley, USA
,
Program Chair:
Rupak Majumdar
MPI-SWS, Germany

Copyright © 2016 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 the author(s) 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: 11 January 2016

Published in SIGPLAN Volume 51, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

34
Total Citations
View Citations
820
Total Downloads

Downloads (Last 12 months)181
Downloads (Last 6 weeks)50

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

GILRAY TADAMS MMIGHT M(2018)Abstract allocation as a unified approach to polyvariance in control-flow analysesJournal of Functional Programming10.1017/S095679681800013828Online publication date: 1-Aug-2018
https://doi.org/10.1017/S0956796818000138
Nicolay JStiévenart QDe Meuter WDe Roover C(2017)Purity analysis for JavaScript through abstract interpretationJournal of Software: Evolution and Process10.1002/smr.188929:12(e1889)Online publication date: 25-Aug-2017
https://doi.org/10.1002/smr.1889
Stiévenart QNicolay JDe Meuter WDe Roover CBiboudis AJonnalagedda MStucki SUreche V(2016)Building a modular static analysis framework in Scala (tool paper)Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala10.1145/2998392.3001579(105-109)Online publication date: 30-Oct-2016
https://dl.acm.org/doi/10.1145/2998392.3001579
Stievenart QVandercammen MMeuter WRoover C(2016)Scala-AM: A Modular Static Analysis Framework2016 IEEE 16th International Working Conference on Source Code Analysis and Manipulation (SCAM)10.1109/SCAM.2016.14(85-90)Online publication date: Oct-2016
https://doi.org/10.1109/SCAM.2016.14
Quiring BVan Horn D(2024)Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow AnalysisProceedings of the ACM on Programming Languages10.1145/36746508:ICFP(728-755)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674650
Koutavas VLin YTzevelekos NSobocinski PLago UEsparza J(2024)Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program EquivalenceProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662103(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662103
Smith SZhang R(2024)A Pure Demand Operational Semantics with Applications to Program AnalysisProceedings of the ACM on Programming Languages10.1145/36498528:OOPSLA1(1154-1180)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649852
Lermusiaux PMontagu B(2024)Detection of Uncaught Exceptions in Functional Programs by Abstract InterpretationProgramming Languages and Systems10.1007/978-3-031-57267-8_15(391-420)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_15
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
Quiring BReppy JShivers O(2022)Analyzing binding extent in 3CPSProceedings of the ACM on Programming Languages10.1145/35476456:ICFP(650-678)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547645
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Issue’s Table of Contents