Introspective Pushdown Analysis of Higher-Order Programs

TL;DR

This paper introduces introspective pushdown systems that combine pushdown flow analysis with abstract garbage collection, enabling more precise and efficient static analysis of higher-order functional programs.

Contribution

It presents a novel class of pushdown systems that allow the integration of abstract garbage collection without losing decidability or soundness.

Findings

Synergistic improvement in analysis precision

Enhanced analysis efficiency

Demonstrated better-than-both-worlds results

Abstract

In the static analysis of functional programs, pushdown flow analysis and abstract garbage collection skirt just inside the boundaries of soundness and decidability. Alone, each method reduces analysis times and boosts precision by orders of magnitude. This work illuminates and conquers the theoretical challenges that stand in the way of combining the power of these techniques. The challenge in marrying these techniques is not subtle: computing the reachable control states of a pushdown system relies on limiting access during transition to the top of the stack; abstract garbage collection, on the other hand, needs full access to the entire stack to compute a root set, just as concrete collection does. \emph{Introspective} pushdown systems resolve this conflict. Introspective pushdown systems provide enough access to the stack to allow abstract garbage collection, but they remain restricted enough to compute control-state reachability, thereby enabling the sound and precise product of pushdown analysis and abstract garbage collection. Experiments reveal synergistic interplay between the techniques, and the fusion demonstrates "better-than-both-worlds" precision.