JavaScript的下推抽象
Pushdown Abstractions of JavaScript
摘要：
我们为JavaScript设计了一系列程序分析，这些程序分析在将调用与返回、异常与处理程序以及中断与标签相匹配方面没有近似。我们这样做，从一个既定的还原语义JavaScript和系统地推导其内涵的抽象解释。我们的第一步是将语义转换为一个等价的低级抽象机：JavaScript抽象机（JAM）。然后，我们给出了一个无限状态但可判定的下推机，其堆栈精确地模拟了具体程序堆栈的结构。堆栈结构的精确模型反过来又赋予精确的控制流分析，即使在存在控制效果的情况下，如异常和finally块。我们给出了传统分析形式（如k-CFA）的下推推广，并证明了抽象解释的下推框架是合理的和可计算的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
