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^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 continuation. Our technique imposes only a constant-factor overhead on the underlying analysis and, with monovariance, costs only O(n^3) 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.
Fri 22 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:10 | Track 1: Program Design and AnalysisResearch Papers at Grand Bay North Chair(s): Manu Sridharan Samsung Research America | ||
10:30 25mTalk | Newtonian Program Analysis via Tensor Product Research Papers Thomas Reps University of Wisconsin - Madison and Grammatech Inc., Emma Turetsky CS Dept., Univ. of Wisconsin-Madison, Prathmesh Prabhu Google Media Attached | ||
10:55 25mTalk | Casper: An Efficient Approach to Call Trace Collection Research Papers Rongxin Wu Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao Xiao The Hong Kong University of Science and Technology, Shing-Chi Cheung Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu Zhang Microsoft Research, Charles Zhang HKUST Media Attached | ||
11:20 25mTalk | Pushdown Control-flow Analysis for Free Research Papers Thomas Gilray University of Utah, Steven Lyde , Michael D. Adams University of Utah, Matthew Might University of Utah, USA, David Van Horn University of Maryland, College Park Pre-print Media Attached | ||
11:45 25mTalk | Binding as Sets of Scopes Research Papers Matthew Flatt University of Utah Pre-print Media Attached |