Staged Abstract Interpreters: Fast and Modular Whole-Program Analysis via Meta-programming
It is well known that a staged interpreter is a compiler: specializing an interpreter to a given program produces an equivalent executable that runs faster. This connection is known as the first Futamura projection. It is even more widely known that an abstract interpreter is a program analyzer: tweaking an interpreter to run on abstract domains produces a sound static analysis. What happens when we combine these two ideas, and apply specialization to an abstract interpreter?
In this paper, we present a unifying framework that naturally extends the first Futamura projection from concrete interpreters to abstract interpreters. Our approach derives a sound staged abstract interpreter based on a generic interpreter with type-level binding-time abstractions and monadic abstractions. By using different instantiations of these abstractions, the generic interpreter can flexibly behave in one of four modes: as an unstaged concrete interpreter, a staged concrete interpreter, an unstaged abstract interpreter, or a staged abstract interpreter. As an example of abstraction without regret, the overhead of these abstraction layers is eliminated in the generated code after staging. We show that staging abstract interpreters is practical and useful to optimize static analysis, all while requiring less engineering effort and without compromising soundness. We conduct three case studies, including a comparison with Boucher and Feeley’s abstract compilation, applications to various control-flow analyses, and a demonstration for modular analysis. We also empirically evaluate the effect of staging on the execution time. The experiment shows an order of magnitude speedup with staging for control-flow analyses.
Wed 23 OctDisplayed time zone: Beirut change
11:00 - 12:30
|BDA: Practical Dependence Analysis for Binary Executables by Unbiased Whole-Program Path Sampling and Per-Path Abstract Interpretation|
Zhuo Zhang Purdue University, Wei You Purdue University, Guanhong Tao Purdue University, Guannan Wei Purdue University, Yonghwi Kwon University of Virginia, Xiangyu Zhang Purdue UniversityDOI Pre-print
|Staged Abstract Interpreters: Fast and Modular Whole-Program Analysis via Meta-programming|
|Static Analysis with Demand-Driven Value Refinement|
Benno Stein University of Colorado Boulder, Benjamin Barslev Nielsen Aarhus University, Bor-Yuh Evan Chang University of Colorado Boulder | Amazon, Anders Møller Aarhus UniversityDOI Pre-print
|Sound and Reusable Components for Abstract Interpretation|