ESMeta is an ECMAScript Specification Metalanguage. This framework extracts a mechanized specification from a given version of ECMAScript/JavaScript specification (ECMA-262) and automatically generates language-based tools.

• Installation Guide
  • Download ESMeta
  • Environment Setting
  • Installation of ESMeta using sbt
• Basic Commands
  • Parsing and Executing ECMAScript files
  • Executing Test262 tests
• Supported Features
  • Interactive Execution with ECMAScript Double Debugger
  • Conformance Test Synthesizer from ECMA-262
  • Type Analysis on ECMA-262
  • Meta-Level Static Analyzer for ECMAScript (temporarily removed)
• Academic Achievement
  • Publications
  • PLDI 2022 Tutorial
  • Communications of the ACM (CACM)

We explain how to install ESMeta with the necessary environment settings from scratch. Our framework is developed in Scala, which works on JDK 17+. So before installation, please install JDK 17+ and sbt, an interactive build tool for Scala.

$ git clone https://github.com/es-meta/esmeta.git

Insert the following commands to ~/.bashrc (or ~/.zshrc):

# for ESMeta
export ESMETA_HOME="<path to ESMeta>" # IMPORTANT!!!
export PATH="$ESMETA_HOME/bin:$PATH" # for executables `esmeta` and etc.
source $ESMETA_HOME/.completion # for auto-completion

The <path to ESMeta> should be the absolute path of the ESMeta repository.

Please type the following command to 1) update the git submodules, 2) generate binary file bin/esmeta, and 3) apply the .completion for auto-completion.

$ cd esmeta && git submodule update --init && sbt assembly && source .completion

If you see the following message, ESMeta is successfully installed:

$ esmeta
# Welcome to ESMeta v0.5.1 - ECMAScript Specification Metalanguage.
# Please type `esmeta help` to see the help message.

You can run this framework with the following command:

$ esmeta <command> <option>* <filename>*

It supports the following commands:

• help shows help messages.
• extract extracts specification model from ECMA-262 (ecma262/spec.html).
• compile compiles a specification to an IR program.
• build-cfg builds a control-flow graph (CFG) from an IR program.
• tycheck performs a type analysis of ECMA-262.
• parse parses an ECMAScript file.
• eval evaluates an ECMAScript file.
• web starts a web server for an ECMAScript double debugger.
• test262-test tests Test262 tests with harness files (default: tests/test262).
• inject injects assertions to check final state of an ECMAScript file.
• mutate mutates an ECMAScript program.
• analyze analyzes an ECMAScript file using meta-level static analysis. (temporarily removed)

and global options:

• -silent does not show final results.
• -error shows error stack traces.
• -status exits with status.
• -time displays the duration time.
• -test262dir={string} sets the directory of Test262 (default: $ESMETA_HOME/tests/test262).

If you want to see the detailed help messages and command-specific options, please use the help command:

# show help messages for all commands
$ esmeta help

# show help messages for specific commands with more details
$ esmeta help <command>

Please use the build-cfg command to extract a mechanized specification as a control-flow graph from ECMA-262:

$ esmeta build-cfg
# ========================================
#  extract phase
# ----------------------------------------
# ========================================
#  compile phase
# ----------------------------------------
# ========================================
#  build-cfg phase
# ----------------------------------------
# 0: def <BUILTIN>:INTRINSICS.SyntaxError(...): Unknown {
#   ...
# }
# 1: def <INTERNAL>:BuiltinFunctionObject.Construct(...): Normal[Object] | Abrupt[throw] {
#   ...
# }
# ...

The build-cfg command consists of three phases:

1. The extract phase extracts specification model (esmeta.spec.Spec) from ECMA-262 (spec.html).
2. The compile phase compiles it into a program (esmeta.ir.Program) in IRES, an Intermediate Representations for ECMAScript Specification.
3. The build-cfg phase builds a control-flow graph (esmeta.cfg.CFG) for a given IRES program.

You can extract mechanized specifications from other versions of ECMA-262 with the -extract:target option. Please enter any git tag/branch names or commit hash as an input of the option:

# extract a mechanized specification from the origin/main branch version of ECMA-262
$ esmeta build-cfg -extract:target=origin/main

# extract a mechanized specification from the 2c78e6f commit version of ECMA-262
$ esmeta build-cfg -extract:target=2c78e6f

After extracting mechanized specifications from ECMA-262, you can parse or execute ECMAScript/JavaScript programs. For example, consider the following example JavaScript file:

// example.js
let x; x ??= class {}; function* f() {}

You can parse or execute it with parse and eval commands.

# parse example.js
$ esmeta parse example.js

# execute example.js
$ esmeta eval example.js

ESMeta supports the execution of Test262 tests to check the conformance between Test262 and ECMA-262.

# run all the applicable Test262 tests
$ esmeta test262-test
# ...
# ========================================
#  test262-test phase
# ----------------------------------------
# - harness                       :    96 tests are removed
# ...
# ----------------------------------------
# - total: 31,537 available tests
#   - normal: 31,537 tests
#   - error: 0 tests
# ----------------------------------------
# ...

If you want to execute specific Test262 files or directories, please list their paths as arguments:

# run Test262 tests in a given directory
$ esmeta test262-test tests/test262/test/language/expressions/addition

ESMeta supports other features utilizing mechanized specifications, including 1) interactive execution of ECMAScript/JavaScript file with a double debugger, 2) conformance test synthesizer, 3) type analysis of ECMA-262, and 4) meta-level static analysis for ECMAScript/JavaScript files. All of them utilize mechanized specifications from ECMA-262. Thus, ESMeta always extracts mechanized specifications as control-flow graphs before performing these features.

ECMAScript Double Debugger extends the ECMAScript/JavaScript interpreter in ESMeta to help you understand how a JavaScript Program runs according to ECMA-262. Currently, it is in an alpha stage and supports only basic features such as:

• Step-by-step execution of ECMA-262 algorithms
• Line-by-line execution of ECMAScript/JavaScript code
• Breakpoints by abstract algorithm names in ECMA-262
• Visualization of ECMA-262 internal states

You can start it with the following instructions:

# turn on server of the double debugger
$ esmeta web

# install and turn on the client-side application using NPM
$ cd client && npm install && npm start

A short introduction video is also available.

We will enhance it with the following features:

• Add more debugger features:
  • Show a JavaScript state by refining an ECMAScript state.
  • Record timestamps during execution for resume & suspend steps (especially for Generator).
  • ...
• Show relevant Test262 tests for each algorithm step in the specification viewer.
• Show the type of each variable using the type analysis result.
• Live-edit of ecma262/spec.html in the specification viewer.

ESMeta supports the synthesis of JavaScript files as conformance tests. We introduced the main concept of the test synthesis in the ICSE 2021 paper with a tool named JEST, a JavaScript Engines and Specification Tester. The test synthesis technique consists of two parts: 1) program synthesis of JavaScript programs using specification coverage and 2) assertion injection based on the mechanized specification extract from ECMA-262.

If you want to synthesize JavaScript programs, please use the fuzz command:

esmeta fuzz -fuzz:log

It basically uses the node/branch coverage in the mechanized specification to synthesize JavaScript programs. The -fuzz:log option dumps the synthesized JavaScript programs into the logs/fuzz/fuzz-<date> directory with the detailed information of the synthesis process:

• seed: seed of the random number generator
• node-coverage.json: node coverage information
• branch-coverage.json: branch coverage information
• constructor.json: constructor information
• mutation-stat.tsv: statistics of mutation methods
• selector-stat.tsv: statistics of selector methods
• summary.tsv: summary of the synthesis process for each logging interval
• target-conds.json: target conditions for the synthesis
• unreach-funcs: unreachable functions
• version: ESMeta version information

In addition, you can use feature-sensitive coverage, which is introduced in the PLDI 2023 paper, with the following options:

• -fuzz:k-fs=<int>: the depth of features for feature-sensitive coverage
• -fuzz:cp: use the call path for feature-sensitive coverage

For example, you can synthesize JavaScript programs with the 2-FCPS coverage (2-feature-sensitive coverage with call path) as follows:

esmeta fuzz -fuzz:log -fuzz:k-fs=2 -fuzz:cp

You can inject assertions into the synthesized JavaScript programs according to the mechanized specification. If you want to inject assertions, please use the inject command:

# inject assertions based on the semantics described in ECMA-262
$ esmeta inject example.js
# ...
# ========================================
#  inject phase
# ----------------------------------------
# // [EXIT] normal
# let x; x ??= class {}; function* f() {}
#
# $algo.set(f, "GeneratorDeclaration[0,0].InstantiateGeneratorFunctionObject")
# $assert.sameValue(Object.getPrototypeOf(f), GeneratorFunction.prototype);
# $assert.sameValue(Object.isExtensible(f), true);
# ...

It prints the assertion-injected JavaScript program without definitions of assertions. The comment // [EXIT] normal denotes that this program should normally terminate. From the fourth line, injected assertions represent the expected value stored in variables, objects, or even internal properties.

If you want to dump the assertion-injected code to a program, please use the -inject:out option. If you want to inject definitions of assertions as well, please use the -inject:defs option:

$ esmeta inject example.js -silent -inject:defs -inject:out=test.js
# - Dumped an assertion-injected ECMAScript program into test.js.

ESMeta provides a type analysis on ECMA-262 to infer unknown types in the specification. We introduced its main concept in the ASE 2021 paper with a tool names JSTAR, a JavaScript Specification Type Analyzer using Refinement. It analyzes types of mechanized specification by performing type analysis of IRES. We utilized condition-based type refinement to prune out infeasible types in each branch for enhanced analysis precision.

If you want to perform a type analysis of ES2022 (or ES13), the latest official version of ECMA-262, please type the following command:

$ esmeta tycheck
# ...
# ========================================
#  tycheck phase
# ----------------------------------------
# - 1806 functions are initial targets.
# - 2372 functions are analyzed in 32493 iterations.

You can perform type analysis on other versions of ECMA-262 with the -extract:target option. Please enter any git tag/branch names or commit hash as an input of the option:

# analyze types for origin/main branch version of ECMA-262
$ esmeta tycheck -extract:target=origin/main

# analyze types for 2c78e6f commit version of ECMA-262
$ esmeta tycheck -extract:target=2c78e6f

ESMeta also supports a meta-level static analyzer for ECMAScript/JavaScript programs based on mechanized specifications extracted from ECMA-262. A mechanized specification is an interpreter that can parse and execute JavaScript programs. We introduced a way to indirectly analyze an ECMAScript/JavaScript program by analyzing its interpreter with a restriction with the given program. We call it meta-level static analysis and presented this technique at ESEC/FSE 2022.

If you want to analyze JavaScript program using a meta-level static analysis, please use the analyze command:

$ esmeta analyze example.js
# ...
# ========================================
#  analyze phase
# ----------------------------------------
# - 108 functions are analyzed in 1688 iterations.

ESMeta supports an interactive Read–eval–print loop (REPL) for the analysis with the -analyze:repl option:

$ esmeta analyze example.js -analyze:repl
# ========================================
#  analyze phase
# ----------------------------------------
#
# command list:
# - help                     Show help message.
# ...
#
# [1] RunJobs[42]:Call[339] -> {
#   ...
# }

analyzer> continue
# - Static analysis finished. (# iter: 1688)

analyzer> print -expr @REALM.GlobalObject.SubMap.f.Value.SubMap.name.Value
# "f"

analyzer> exit

It showed that the property name of the global variable f points to a single string "f".

In the future version of ESMeta, we will add more kind documentation for this analyzer REPL.

• [PLDI 2023] Feature-Sensitive Coverage for Conformance Testing of Programming Language Implementations (old repo)
• [ESEC/FSE 2022] Automatically Deriving JavaScript Static Analyzers from Specifications using Meta-Level Static Analysis (old repo)
• [ASE 2021] JSTAR: JavaScript Specification Type Analyzer using Refinement (old repo)
• [ICSE 2021] JEST: N+1-version Differential Testing of Both JavaScript Engines (old repo)
• [ASE 2020] JISET: JavaScript IR-based Semantics Extraction Toolchain (old repo)

Title: Filling the gap between the JavaScript language specification and tools using the JISET family

• Presenters: Jihyeok Park, Seungmin An, and Sukyoung Ryu
• Session 1
• Session 2-1
• Session 2-2

• Title: JavaScript Language Design and Implementation in Tandem
  • DOI: 10.1145/3624723

See the following video for more details:

• link: https://youtu.be/JGxc-KIUnQY