Pushdown control-flow analysis for free

DOI10.1145/2837614.2837631MaRDI QIDQ2828314zbMATH OpenOpenAlexWikidataFDO

Authors Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David van Horn

Publication date 24 October 2016

Published in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1507.03137

zbMATH Keywords

abstract interpretationcontrol-flow analysispushdown analysisstatic analysisstore-allocated continuations

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: Traditional control-flow analysis (CFA) for higher-order languages, whether implemented by constraint-solving or abstract interpretation, introduces spurious connections between callers and callees. Two distinct invocations of a function will necessarily pollute one another's return-flow. Recently, three distinct approaches have been published which provide perfect call-stack precision in a computable manner: CFA2, PDCFA, and AAC. Unfortunately, CFA2 and PDCFA are difficult to implement and require 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^{9}logn)$. 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 continuation. Our technique imposes only a constant-factor overhead on the underlying analysis and, with monovariance, costs only O(n3) in the worst case. This paper presents the intuitions behind this development, a proof of the precision of this analysis, and benchmarks demonstrating its efficacy.

Recommendations

• CFA2: A Context-Free Approach to Control-Flow Analysis
• CFA2: a context-free approach to control-flow analysis
• Pushdown flow analysis of first-class control
• Pushdown flow analysis with abstract garbage collection
• A posteriori environment analysis with Pushdown Delta CFA

Cited in

(12)

• Relatively complete pushdown analysis of escape continuations
• Pushdown flow analysis with abstract garbage collection
• CFA2: a context-free approach to control-flow analysis
• Higher-order model checking in direct style
• Abstract allocation as a unified approach to polyvariance in control-flow analyses
• Liberate abstract garbage collection from the stack by decomposing the heap
• Introspective pushdown analysis of higher-order programs
• Pushdown flow analysis of first-class control
• A posteriori environment analysis with Pushdown Delta CFA
• EigenCFA, accelerating flow analysis with GPUs
• Control-flow analysis of function calls and returns by abstract interpretation
• Pushdown normal-form bisimulation: a nominal context-free approach to program equivalence

This page was built for publication: Pushdown control-flow analysis for free

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2828314)