CFA2: Pushdown Flow Analysis for Higher-Order Languages

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.