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 Jan Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change
|10:30 - 10:55|
|Newtonian Program Analysis via Tensor Product|
Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc., Emma TuretskyCS Dept., Univ. of Wisconsin-Madison, Prathmesh PrabhuGoogleMedia Attached
|10:55 - 11:20|
|Casper: An Efficient Approach to Call Trace Collection|
Rongxin WuDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao XiaoThe Hong Kong University of Science and Technology, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu ZhangMicrosoft Research, Charles ZhangHKUSTMedia Attached
|11:20 - 11:45|
|Pushdown Control-flow Analysis for Free|
Thomas GilrayUniversity of Utah, Steven Lyde, Michael D. AdamsUniversity of Utah, Matthew MightUniversity of Utah, USA, David Van HornUniversity of Maryland, College ParkPre-print Media Attached
|11:45 - 12:10|
|Binding as Sets of Scopes|
Matthew FlattUniversity of UtahPre-print Media Attached