JavaScript is one of the most dominant programming languages. However, despite its popularity, it is a challenging task to correctly understand the behaviors of JavaScript programs because of their highly dynamic nature. Researchers have developed various static analyzers that strive to conform to ECMA-262, the standard specification of JavaScript. Unfortunately, all the existing JavaScript static analyzers require manual updates for new language features. This problem has become more critical since 2015 because the JavaScript language itself rapidly evolves with a yearly release cadence and open development process.

Modern programming follows the continuous integration (CI) and continuous deployment (CD) approach rather than the traditional waterfall model. Even the development of modern programming languages uses the CI/CD approach to swiftly provide new language features and to adapt to new development environments. Unlike in the conventional approach, in the modern CI/CD approach, a language specification is no more the oracle of the language semantics because both the specification and its implementations (interpreters or compilers) can co-evolve. In this setting, both the specification and implementations may have bugs, and guaranteeing their correctness is non-trivial. In this paper, we propose a novelN+1-versiondifferentialtestingto resolve the problem. Unlike the traditional differential testing, our approach consists of three steps: (1) to automatically synthesize programs guided by the syntax and semantics from a given language specification, (2) to generate conformance tests by injecting assertions to the synthesized programs to check their final program states, (3) to detect bugs in the specification and implementations via executing the conformance tests on multiple implementations and (4) to localize bugs on the specification using statistical information. We actualize our approach for the JavaScript programming language via JEST, which performsN+1-version differential testing for modern JavaScript engines and ECMAScript, the language specification describing the syntax and semantics of JavaScript in a natural language. We evaluated JEST with four JavaScript engines that support all modern JavaScript language features and the latest version of ECMAScript (ES11, 2020). JEST automatically synthesized 1,700 programs that covered 97.78% of syntax and 87.70% of semantics from ES11. Using the assertion-injected JavaScript programs, it detected 44 engine bugs in four different engines and 27 specification bugs in ES11.

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.

JavaScript was initially designed for client-side programming in web browsers, but its engine is now embedded in various kinds of host software. Despite the popularity, since the JavaScript semantics is complex especially due to its dynamic nature, understanding and reasoning about JavaScript programs are challenging tasks. Thus, researchers have proposed several attempts to define the formal semantics of JavaScript based on ECMAScript, the official JavaScript specification. However, the existing approaches are manual, labor-intensive, and error-prone and all of their formal semantics target ECMAScript 5.1 (ES5.1, 2011) or its former versions. Therefore, they are not suitable for understanding modern JavaScript language features introduced since ECMAScript 6 (ES6, 2015). Moreover, ECMAScript has been annually updated since ES6, which already made five releases after ES5.1.