一句话：首个对 ECMAScript 规范做类型分析并检测规范缺陷的工具，借助基于条件的精化提升分析精度。
ECMAScript 规范频繁更新，其类型相关的错误只能由 TC39 人工评审，缺乏自动化检查手段。本文提出 JSTAR：它把规范中以结构化自然语言描述的抽象算法编译为无类型中间表示 IRES 中的函数，再结合 ECMAScript 规范类型对函数做类型分析；为提升精度，作者提出基于条件的精化，利用断言与分支条件剪除不可行的抽象状态。分析结果输入由四个检查器组成的缺陷检测器以发现规范缺陷。作者在 2018–2021 年官方仓库全部 864 个版本上评估，每版平均耗时 137.3 秒，检出 157 个类型相关规范缺陷，精度 59.2%（93 个为真实缺陷），其中 14 个为新发现且均获 TC39 确认。
JavaScript is one of the mainstream programming languages for client-side programming, server-side programming, and even embedded systems. Various JavaScript engines developed and maintained in diverse fields must conform to the syntax and semantics described in ECMAScript, the standard specification of JavaScript. Since an incorrect description in ECMAScript can lead to wrong JavaScript engine implementations, checking the correctness of ECMAScript is critical and essential. However, all the specification updates are currently manually reviewed by the Ecma Technical Committee 39 (TC39) without any automated tools. Moreover, in late 2014, the committee announced the yearly release cadence and open development process of ECMAScript to quickly adapt to evolving development environments. Because of such frequent updates, checking the correctness of ECMAScript becomes more labor-intensive and error-prone.To alleviate the problem, we propose JSTAR, a JavaScript Specification Type Analyzer using Refinement. It is the first tool that performs type analysis on JavaScript specifications and detects specification bugs using a bug detector. For a given specification, JSTAR first compiles each abstract algorithm written in a structured natural language to a corresponding function in IRES, an untyped intermediate representation for ECMAScript. Then, it performs type analysis for compiled functions with specification types defined in ECMAScript. Based on the result of type analysis, JSTAR detects specification bugs using a bug detector consisting of four checkers. To increase the precision of the type analysis, we present condition-based refinement for type analysis, which prunes out infeasible abstract states using conditions of assertions and branches. We evaluated JSTAR with all 864 versions in the official ECMAScript repository for the recent three years from 2018 to 2021. JSTAR took 137.3 seconds on average to perform type analysis for each version, and detected 157 type-related specification bugs with 59.2% precision; 93 out of 157 bugs are true bugs. Among them, 14 bugs are newly detected by JSTAR, and the committee confirmed them all.
DOI 原文 ·
@inproceedings{paperbot6539,
title = {JSTAR: JavaScript Specification Type Analyzer using Refinement},
author = {Jihyeok Park and Seungmin An and Wonho Shin and Yusung Sim and Sukyoung Ryu},
booktitle = {ASE},
year = {2021},
doi = {10.1109/ase51524.2021.9678781}
}