Abstracting Abstract Control (Extended)
J. Ian Johnson, David Van Horn

TL;DR
This paper extends the abstracting abstract machines (AAM) approach to incorporate pushdown systems for more accurate static analysis of dynamic language features like control stack inspection and first-class continuations.
Contribution
It revises the AAM technique to target pushdown systems, enabling more precise analysis of dynamic language features using only abstract machines and memoization.
Findings
The approach applies to languages with closures and continuations.
It handles features like garbage collection and stack inspection.
Provides more accurate static analysis for dynamic languages.
Abstract
The strength of a dynamic language is also its weakness: run-time flexibility comes at the cost of compile-time predictability. Many of the hallmarks of dynamic languages such as closures, continuations, various forms of reflection, and a lack of static types make many programmers rejoice, while compiler writers, tool developers, and verification engineers lament. The dynamism of these features simply confounds statically reasoning about programs that use them. Consequently, static analyses for dynamic languages are few, far between, and seldom sound. The "abstracting abstract machines" (AAM) approach to constructing static analyses has recently been proposed as a method to ameliorate the difficulty of designing analyses for such language features. The approach, so called because it derives a function for the sound and computable approximation of program behavior starting from the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
