Pushdown Abstractions of JavaScript

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 computable.