Pushdown Abstractions of JavaScript
David Van Horn, Matthew Might

TL;DR
This paper introduces a pushdown analysis framework for JavaScript that precisely models control flow, including exceptions and labels, by transforming semantics into an abstract machine and deriving a decidable pushdown model.
Contribution
It systematically derives a pushdown control-flow analysis for JavaScript from its semantics, enabling precise matching of calls, returns, and control effects.
Findings
Provides a sound and computable pushdown analysis framework.
Achieves precise control-flow analysis even with exceptions.
Extends traditional analysis methods like k-CFA to pushdown models.
Abstract
We design a family of program analyses for JavaScript that make no approximation in matching calls with returns, exceptions with handlers, and breaks with labels. We do so by starting from an established reduction semantics for JavaScript and systematically deriving its intensional abstract interpretation. Our first step is to transform the semantics into an equivalent low-level abstract machine: the JavaScript Abstract Machine (JAM). We then give an infinite-state yet decidable pushdown machine whose stack precisely models the structure of the concrete program stack. The precise model of stack structure in turn confers precise control-flow analysis even in the presence of control effects, such as exceptions and finally blocks. We give pushdown generalizations of traditional forms of analysis such as k-CFA, and prove the pushdown framework for abstract interpretation is sound and…
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.
Taxonomy
TopicsLogic, programming, and type systems · Security and Verification in Computing · Parallel Computing and Optimization Techniques
