It is well known that a staged interpreter is a compiler: specializing the interpreter to a given program produces an equivalent program that runs faster, which is known as the first Futamura projection. It is even more widely known that an abstract interpreter is a program analyzer: tweaking the interpreter to run on a domain of abstract values produces a sound static analysis. What happens when we combine these two ideas, and apply staging to an abstract interpreter?
In this paper, we present a unifying framework that naturally extends the first Futamura projection of concrete interpreters to abstract interpreters. Our approach derives a sound staged abstract interpreter based on a semantic-agnostic interpreter with type-level binding-time abstraction and monadic abstraction. By using different instantiations of these abstractions, the generic interpreter can flexibly behave in four modes: unstaged concrete interpreter, staged concrete interpreter, unstaged abstract interpreter, or staged abstract interpreter.
As an example of abstraction without regret, we show that staging abstract interpreters is practical and useful to optimize static analysis while requiring least engineering efforts and not compromising any soundness. We conduct three case studies, including a comparison with Boucher and Feeley’s abstract compilation, the application on various control-flow analyses, and the use to modular analysis. We also empirically evaluate the performance improved by staging. The overhead of the abstraction layers is eliminated in the generated code, and the experiment shows an average speedup of 11x times with staging for control-flow analysis.