Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
CFA2: Pushdown Flow Analysis for Higher-Order Languages

Speaker  Dimitris Vardoulakis

Affiliation  Northeastern University

Host  Ben Livshits, RiSE

Duration  00:46:48

Date recorded  20 June 2011

Flow analysis is a valuable tool for creating better programming languages; its applications span optimization, debugging, verification and program understanding. Despite its apparent usefulness, flow analysis of higher-order programs has not been made practical. The reason is that existing analyses do not model function call and return well: they remember only a bounded number of pending calls because they approximate programs with control-flow graphs. Call/return mismatch results in imprecision and increases the analysis time.

We describe CFA2, a flow analysis that provides unbounded call/return matching in the presence of hard-to-analyze language features, such as first-class functions, tail recursion and first-class control. The key insight is that we can model a higher-order program as a pushdown automaton. By pushing return points on the stack, we eliminate call/return mismatch. We have implemented CFA2 for JavaScript and used it for type inference. Our experimental results show that the analysis is precise and scalable.

©2011 Microsoft Corporation. All rights reserved.
> CFA2: Pushdown Flow Analysis for Higher-Order Languages