Designing Precise Higher-Order Pushdown Flow Analyses

J. Ian Johnson and David Van Horn
Preprint, 2012

Formalisms for context-free approaches to higher-order control-flow analysis are complex and require significant effort to prove correct. However, these approaches are enticing because they provide improved precision over finite state approaches. We present a new method for deriving context-free analyses that results in “obviously correct” formalisms that consists of making small changes to the original concrete semantics. We validate this method by using it to derive existing context-free analyses from abstract machines. We further exercise the technique by applying it to abstract machines that more closely represent real language implementations and consequently derive analyses more precise than existing ones. Specifically, we use an escape analysis to derive better stack allocation, and use garbage collection to derive better heap allocation. We also present a novel semantics for call/cc that, when turned into an analysis, handles non-escaping continuations more precisely than prior treatments of first-class control.