Pushdown Control-Flow Analysis for Free

Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, and David Van Horn

Status: Accepted. To be published at POPL 2016

Links

• Author’s copy
• ArXive (slightly out of date, will be updated soon)
• Code

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ⁿ), PDCFA is in O(n⁶), and AAC is in O(n⁸).

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³) in the monovariant case. We present the intuitions behind this development, benchmarks demonstrating its efficacy, and a proof of the precision of this analysis.

Keywords

Keywords Static analysis; Control-flow analysis; Abstract interpretation; Pushdown analysis; Store-allocated continuations

Citation

BibTeX Entry

@inproceedings{gilray2016p4f,
  author = {Gilray, Thomas and Lyde, Steven and Adams, Michael D. and Might, Matthew and Van Horn, David},
  title = {Pushdown Control-Flow Analysis for Free},
  booktitle = {Proceedings of the 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = {2016},
  series = {POPL '16},
  address = {New York, NY, USA},
  month = jan,
  publisher = {ACM},
  doi = {10.1145/2837614.2837631},
}

Copyright Notice