Authors Alan Schmitt Arthur Charguéraud Thomas Wood
License CC-BY-4.0
JSExplain: a Double Debugger for JavaScript
Arthur Charguéraud Alan Schmitt Thomas Wood
Inria & Université de Strasbourg, Inria & Univ Rennes, CNRS, IRISA Imperial College London
CNRS, ICube UMR 7357 alan.schmitt@inria.fr thomas.wood09@imperial.ac.uk
arthur.chargueraud@inria.fr
ABSTRACT Indeed, in JS, the evaluation of any sub-expression, of any type
We present JSExplain, a reference interpreter for JavaScript that conversion, and of most internal operations from the specification
closely follows the specification and that produces execution traces. may result in the execution of user code, hence the raising of an
These traces may be interactively investigated in a browser, with exception, interrupting the normal control flow. Throught its suc-
an interface that displays not only the code and the state of the in- cessive editions, the ECMA standard progressively introduced a
terpreter, but also the code and the state of the interpreted program. notation akin to an exception monad (§1.2). This notation is natu-
Conditional breakpoints may be expressed with respect to both the rally translated into real code by a proper monadic bind operator
interpreter and the interpreted program. In that respect, JSExplain of the exception monad.
is a double-debugger for the specification of JavaScript. Regarding the state, the standard assumes a global state. A refer-
ence interpreter could either assume a global state, modified with
ACM Reference Format: side-effects, or thread the state explicitly in purely-functional style.
Arthur Charguéraud, Alan Schmitt, and Thomas Wood. 2018. JSExplain: a
We chose the latter approach for three reasons. First, we already
Double Debugger for JavaScript. In WWW ’18 Companion: The 2018 Web
Conference Companion, April 23–27, 2018, Lyon, France. ACM, New York, NY,
need a monad for exceptions, so we may easily extend this monad
USA, 9 pages. https://doi.org/10.1145/3184558.3185969 to also account for the state. Second, starting from code with an
explicit state would make it easier to generate a corresponding
inductive definition in a formal logic (e.g., Coq), which we would
1 INTRODUCTION like to investigate in the future. Third, to ease the reading, one may
1.1 A reference interpreter for JS easily hide a state that is explicitly threaded; the converse, materi-
JavaScript (JS) has a complex semantics. As of 2017, its specifica- alizing a state that is implicit, would be much more challenging.
tion by ECMA consists of 885 pages of English prose [6] (details We thus write our reference interpreter in a purely-functional
in §1.2). Unsurprisingly, this prose-based presentation of the spec- language extended with syntactic sugar for the monadic notation
ification does not meet the needs of the JavaScript designers and to account for the state and the propagation of abrupt termination
implementers. In particular, the JavaScript standardization commit- (§2). For historical reasons, we chose a subset of OCaml as source
tee (TC39) has repeatedly expressed the need for better tools for syntax, but other languages could be used. In fact, we implemented
describing and interacting with the semantics (§1.3). a translator from our subset of OCaml to a subset of JS (a subset
Prior work on the formalization of JS semantics, notably JSCert [3] involving no side effects and no type conversions). We thereby
and KJS [11], has made some progress, yet falls short of delivering obtain a JS interpreter that is able to execute JS programs inside a
several of the features needed by TC39 (§1.4). In this work, we JS virtual machine—JS fans should be delighted. To further improve
aim at addressing these requests: we revisit the JSCert semantics accessibility to JS programmers, we also translate the source code
by giving it a presentation more accessible to the JavaScript com- of our interpreter into a human-readable JS-style syntax, which we
munity. Our presentation aims to be well-suited for writing and call pseudo-JS, and that essentially consists of JS syntax augmented
reading the specifications, executing test cases, checking coverage, with a monadic notation and with basic pattern matching.
and interatively debugging the specification (§1.5). Our reference semantics for JS is inherently executable. We may
The JS specification is essentially describing a reference inter- thus execute our interpreter on test suites, either by compiling and
preter. Although it consists of English prose, the ECMA standard executing the OCaml code, or by executing the JS translation of
reads almost like pseudo-code. Most ambiguities and unclear para- that code. It is indeed useful to be able to check that the evaluation
graphs that were present in ECMA3 and ECMA5 were progressively of examples from the JS test suites against our reference semantics
resolved in subsequent editions. Thus, turning ECMA pseudo-code produces the desired output.
into real code, i.e., code expressed in a real programming language, Even more interesting is the possibility to investigate, step by
is not so hard. Yet, there are two nontrivial aspects: dealing with the step, the evaluation of the interpreter on a given test case. Such
representation of the state, and dealing with abrupt termination, investigation allows to understand why the evaluation of a partic-
such as exceptions, return, break, and continue statements. ular test case produces a particular output—given the complexity
of JS, even an expert may easily get puzzled by the output value
This paper is published under the Creative Commons Attribution 4.0 International of a particular piece of code. Furthermore, interactive execution
(CC BY 4.0) license. Authors reserve their rights to disseminate the work on their makes it easier for the contributor of a new JS feature to add new
personal and corporate Web sites with the appropriate attribution.
WWW’18 Companion, April 23–27, 2018, Lyons, France test cases and to check that these tests trigger the new features and
© 2018 IW3C2 (International World Wide Web Conference Committee), published correctly interact with existing features.
under Creative Commons CC BY 4.0 License. In this paper, we present a tool, called JSExplain, for investigating
ACM ISBN 978-1-4503-5640-4/18/04.
https://doi.org/10.1145/3184558.3185969 JS executions. This tool can be thought as a double debugger, which
WWW’18 Companion, April 23–27, 2018, Lyons, France Arthur Charguéraud, Alan Schmitt, and Thomas Wood
displays both the state of the interpreted program and that of the Evaluation of: AdditiveExpression : AdditiveExpression +
interpreter program. In particular, our tool supports conditional MultiplicativeExpression
breakpoints expressed simultaneously on the interpreter program
1. Let lref be the result of evaluating AdditiveExpression.
and the interpreted program. To implement this tool, we generate
2. Let lval be GetValue(lref).
a version of our interpreter that is instrumented for producing
3. Let rref be the result of evaluating MultiplicativeExpression.
execution traces (§3), and we provide a web-based tool to navigate
4. Let rval be GetValue(rref).
through such traces (§4). As far as we know, our tool is the first such
5. Let lprim be ToPrimitive(lval).
double debugger, i.e., debugger with specific additions for dealing
6. Let rprim be ToPrimitive(rval).
with programs that interpret other programs (§5).
7. If Type(lprim) is String or Type(rprim) is String, then
– Return the String that is the result of concatenating
1.2 English Specification of JS ToString(lprim) followed by ToString(rprim).
To illustrate the style in which the JavaScript standard (ECMA) [6] 8. Return the result of applying the addition operation to
is written, consider the description of addition, which will be our ToNumber(lprim) and ToNumber(rprim).
running example throughout the paper. In JS, the addition operator
Figure 1: ECMA5 specification of addition.
casts its arguments to integers and computes their sum, except
if one of the two arguments is a string, in which case the other
argument is cast to a string and the two strings are concatenated. Evaluation of: AdditiveExpression : AdditiveExpression +
The ECMA5 presentation (prior to June 2016) appears in Fig- MultiplicativeExpression
ure 1. First, observe that the presentation describes both the parsing
1. Let lref be the result of evaluating AdditiveExpression.
rule for addition and its evaluation rule. Presumably for improved
2. Let lval be GetValue(lref).
accessibility, the JS standard does not make explicit the notion of
3. ReturnIfAbrupt(lval).
an abstract syntax tree (AST). The semantics of addition goes as
4. Let rref be the result of evaluating MultiplicativeExpression.
follows: first evaluate the left branch to a value, then evaluate the
5. Let rval be GetValue(rref).
right branch to a value, then converts both values (which might
6. ReturnIfAbrupt(rval).
be objects) into primitive values (e.g., string, number, ...), then test
7. Let lprim be ToPrimitive(lval).
whether one of the two arguments is a string. If so, cast both ar-
8. ReturnIfAbrupt(lprim).
guments to strings and return their concatenation; otherwise cast
9. Let rprim be ToPrimitive(rval).
both arguments to numbers and return their sum.
10. ReturnIfAbrupt(rprim).
This presentation style used in ECMA5 gives no details about
11. If Type(lprim) is String or Type(rprim) is String, then
the propagation of exceptions. While the treatment of exceptions
a. let lstr be ToString(lprim).
is explicit for statements, it is left implicit for expressions. For
b. ReturnIfAbrupt(lstr).
example, if the evaluation of the left branch raises an exception, the
c. let rstr be ToString(rprim).
right branch should not be evaluated. It appeared that leaving the
d. ReturnIfAbrupt(rstr).
treatment of exceptions implicit could lead to ambiguities at what
e. Return the String that is the result of concatenating lstr
exactly should or should not be evaluated when an exception gets
and rstr.
triggered. The ECMA committee hates such ambiguities, because it
12. let lnum be ToNumber(lprim).
could (and typically does) result in different browsers exhibiting
13. ReturnIfAbrupt(lnum).
different behaviors—the nightmare of web-developers.
14. let rnum be ToNumber(rprim).
In ECMA6, such ambiguities were resolved by making the prop-
15. ReturnIfAbrupt(rnum).
agation of exceptions explicit. Figure 2 shows the updated specifi-
16. Return the result of applying the addition operation to lnum
cation for the addition operator. There are two main changes. First,
and rnum.
each piece of evaluation is described on its own line, thereby mak-
ing the evaluation order crystal clear. Second, the meta-operation Figure 2: ECMA6 specification of addition.
ReturnIfAbrupt is invoked on every intermediate result. This meta-
operation essentially corresponds to an exception monad. The
ECMA6 standards, which aims to be accessible to a large audience, specification. As detailed in Figure 4, they define the question mark
avoids the introduction of the word “monad”. Instead, it specifies symbol to be a lightweight shorthand for ReturnIfAbrupt steps. The
ReturnIfAbrupt as a “macro”, as shown in Figure 3. Essentially, ev- specification of addition in that new style is shown in Figure 5.
ery result consists of a “completion record”, which corresponds to The presentation of ECMA7 and ECMA8 (Figure 5) is both more
a sum type distinguishing normal results from exceptions. concise than that of ECMA6 (Figure 2) and more formal than that of
In all constructs except try-catch blocks, exceptions interrupt ECMA5 (Figure 1). The use of question marks is to be compared in
the normal flow of the evaluation. As a result, ECMA6 specification §2 with the monadic notation that we use for our formal semantics.
is scattered with about 1100 occurences of ReturnIfAbrupt opera-
tions. Realizing the impracticability of that style of specification, 1.3 Requests from the JS Committee
the standardization committee decided to introduce in ECMA7 an The JavaScript standardization body, part of ECMA and known
additional layer of syntactic sugar in subsequent versions of the as TC39, includes representatives from browser vendors, major
JSExplain: a Double Debugger for JavaScript WWW’18 Companion, April 23–27, 2018, Lyons, France
Evaluation of: ReturnIfAbrupt Evaluation of: AdditiveExpression : AdditiveExpression +
Algorithms steps that say MultiplicativeExpression
1. Let lref be the result of evaluating AdditiveExpression.
1. ReturnIfAbrupt(argument).
2. Let lval be ? GetValue(lref).
mean the same thing as: 3. Let rref be the result of evaluating MultiplicativeExpression.
4. Let rval be ? GetValue(rref).
1. If argument is an abrupt completion, return argument. 5. Let lprim be ? ToPrimitive(lval).
2. Else if argument is a Completion Record, let argument be 6. Let rprim be ? ToPrimitive(rval).
argument.[[value]]. 7. If Type(lprim) is String or Type(rprim) is String, then
a. let lstr be ? ToString(lprim).
Figure 3: ECMA6 interpretation of ReturnIfAbrupt. b. let rstr be ? ToString(rprim).
c. Return the String that is the result of concatenating lstr
Algorithms steps that say or are otherwise equivalent to: and rstr.
1. ReturnIfAbrupt(AbstractOperation()). 8. let lnum be ? ToNumber(lprim).
9. let rnum be ? ToNumber(rprim).
mean the same thing as: 10. Return the result of applying the addition operation to lnum
1. Let hygienicTemp be AbstractOperation(). and rnum.
2. If hygienicTemp is an abrupt completion, return hygienicTemp.
3. Else if hygienicTemp is a Completion Record, let Figure 5: ECMA7 and ECMA8 specification of addition.
hygienicTemp be hygienicTemp.[[Value]].
Where hygienicTemp is ephemeral and visible only in the steps
pertaining to ReturnIfAbrupt. • a tool able to tell which lines from the specification are not
covered by any test from the main test suite (test262 [15]);
Invocations of abstract operations and syntax-directed operations • a tool able to execute step-by-step the specification on con-
that are prefixed by ? indicate that ReturnIfAbrupt should be crete JS programs, and to inspect the value of the variables.
applied to the resulting Completion Record. For example, the step: In particular, step-by-step execution is critically needed to eval-
1. ? OperationName(). uate new features. When the committee decides that a feature pro-
posal is worth integrating, it typically does not accept the proposal
is equivalent to the following step: as is, but instead modifies the proposal in a way that is amenable
1. ReturnIfAbrupt(OperationName()). to a simple, clear specification without corner cases, carefully try-
ing to avoid harmful interactions with other existing features (or
Figure 4: ECMA7 and ECMA8 addition for ReturnIfAbrupt. planned features). During this process, at some point the commit-
tee members have in their hand a draft of the extended semantics
as well as a collection of test cases illustrating the new behaviors
actors of the web, and academics. It aims at defining a common that should be introduced. Naturally, they would like to check that
semantics that all browsers should implement. TC39 faces major their formalization of the extended semantics assigns the expected
challenges. On the one hand, it must ensure full backward com- behavior to each of the test cases.
patibility, to avoid “breaking the web”. In particular, no feature One might argue that such a task could be performed by mod-
used in the wild ever gets removed from the specification. On the ifying one of the mainstream browsers. Yet, existing JS runtimes
other hand, the committee imposes the rule that no feature may are built with efficiency in mind, with huge code bases involving
be added to the standard before it has been implemented, shipped, numerous optimizations. As such, modifying the code in any way
and tested at scale in at least two distinct major browsers. Any is too costly for committee members to investigate variations on a
member of the committee may propose new features, hence there feature request. Even if they could invest the effort, the distance
are many proposals being actively developed, at different stages of between the English prose specification and the implementation
formalization [14]. would be too large to have any confidence that the two match, i.e.,
The rapid evolution of the standard stresses the need for appro- that the behavior implemented in the code matches the behavior
priate tools to assist in the rewriting, testing, and debugging of the described by the prose.
semantics. In particular, several members with whom we have had An alternative approach to testing a new feature is to develop
interactions expressed their need for several basic tools, such as: an elaboration (local translation) of that feature into plain JS. This
• a tool for knowing whether all variables that occur in the can take the form of syntactic sugar adding a missing API, namely
specification are properly defined (bound) somewhere; a polyfill, or the form of a source to source translation, namely
• a tool to perform basic type-checking of the meta-functions a transpiler. For instance, one might translate so-called “template
and of the variables involved in the specification; literals” into simple string concatenation.
• a tool for checking that effectful operations go on a line of /* new feature */ /* plain JavaScript */
their own, to avoid ambiguity in the order of evaluation; var name = "me"; var name = "me";
• a tool for checking that the behavior is specified in all cases; `hello ${name}`; "hello " + name;
WWW’18 Companion, April 23–27, 2018, Lyons, France Arthur Charguéraud, Alan Schmitt, and Thomas Wood
While polyfills and transpilers are a simple approach to testing new 1.5 Contribution
features, they have two major limitations. First, the encoding might In this paper, we present a tool, called JSExplain, which aims at
be very invasive. For instance, the 2015 version of ECMAScript providing a formal semantics for JS that addresses the aforemen-
added proxies, and as a consequence significantly changed the inter- tioned limitations of prior work. Our contribution is two-fold. First,
nal methods of the language; the Babel [1] transpiler for proxies [2] we present a specification for JS expressed in a language that, we
is able to simulate this feature in prior version of JS, but at the cost argue, JS programmers can easily read and write (§2). Second, we
of replacing all field access operations with calls to wrapper func- present an interactive tool that supports step-by-step execution
tions. Second, the interaction of several new features implemented of the specification on an input JS program (§3 and §4). Our tool
using these approaches is very difficult to anticipate. mimics the features of a debugger, such as navigation controls, state
and variable visualization, and conditional breakpoints, but does
1.4 Formal Specifications of JS so for both the interpreter program and the interpreted program.
The language in which we display the specification consists of
In recent years, two projects, JSCert [3] and KJS [11] have proposed a subset of JS extended with syntactic sugar for monads and basic
a formal specification for a significant subset of JS. JSCert provides pattern matching. This language, which we call pseudo-JS, could
a big-step inductive definition for ECMA5, (technically, a pretty-big- be the source syntax for our specification. However, for historical
step specification [5]), formalized in the Coq proof assistant [16]. and technical reasons, we use as input syntax a subset of OCaml,
JSCert comes along with a reference interpreter, called JSRef, that which is processed using the OCaml type-checker. Our current tool
is proved correct with respect to the inductive definition. JSRef automatically converts the OCaml AST into pseudo-JS code. In the
may be extracted into executable OCaml code for executing tests. future, we might as well have our reference interpreter be directly
KJS describes a small-step semantics for JS as a set of rewriting in pseudo-JS syntax, and we could typecheck that code either by
rules, using the K framework [13]. This framework has been used converting it to OCaml or by reimplementing a basic ML type-
to formalize the semantics of several other real-world languages. It checker. A third alternative would be to use the Reason syntax [12],
provides in particular tool support for executing (syntax-directed) a JS-like syntax for OCaml programs. The only difference between
transition rules on a concrete input program. the approaches is whether TC39 committee members would prefer
At first sight, it might seem that a formal specification addresses to write OCaml style or JS style code.
all the requests from the committee. Definitions are thoroughly
type-checked; in particular, all variables must be properly bound.
Definitions, being defined in a formal language, are ambiguity- 2 SPECIFICATION LANGUAGE
free; in particular, the order of evaluation and the propagation of
2.1 Constructs of the Language
exceptions is precisely specified. The semantics can be executed on
concrete input programs; moreover, with some extra tooling, one The input syntax in which we write and display the specification is
may execute a set of programs and report on the coverage of the a purely-functional language that includes the following constructs:
specification by the tests. variables, constants, sequence, conditional, let-binding, function
Given all the nice features of formal semantics, why wouldn’t definition, function application (with support for prefix and infix
the standardization committee TC39 consider one of these formal functions), data constructors, records (including record projections,
semantics as the reference for the language? After discussing with and the “record-with” construct to build a copy of a record with
senior members from TC39, we understand that there are (at least) a number of fields updated), tuples (i.e., anonymous records), and
three main reasons why there is no chance for a formal semantics simple pattern matching (only with non-nested patterns, restricted
such as JSCert or KJS to be adopted as reference semantics. to data constructors, constants, variables, and wildcards). For con-
venience, let-bindings and functions may bind patterns (as opposed
(1) Formal specifications in Coq or in K use syntax and concepts to only variables).
that are not easily accessible to JS programmers. Yet, the We purposely aim for a specification language with a limited
specification is meant to be read by a wide audience. number of constructs and a very standard semantics, to minimize
(2) These formal languages have a cost of entry that is too high the cost of entry into that language. Note that the input code is type-
for committee members to reach the level of proficiency checked in ML. (Polymorphism is used mainly for type-checking
required for contributing new definitions all by themselves. options and lists, and operations on them.)
(3) JSCert and KJS come with specifications that can be executed, As explained earlier (§1.2), the semantics involves the propa-
yet provide no debugger-style support for interactively nav- gation of exceptions and other abrupt behaviors (break, continue,
igating through an execution and for visualizing the state and return). Their propagation can be described within our small
and the values of the variables, and thus do not help so much language, using functions and pattern matching. Nevertheless, in-
in tuning the description of new features. troducing a little bit of syntactic sugar greatly improves read-
ability. For example, we write “let%run x = e1 in e2” to mean
In the present work, we temporarily leave aside the motivation “if_run e1 (fun x -> e2)”, where if_run is a function that imple-
of giving a formal semantics to JS that one could use to formalize ments our monad.
properties of the language (e.g., security properties), and rather The monadic operator if_run admits a polymorphic type, hence
focus on trying to provide a formal semantics that meets better the functions from the specification may return objects of various types.
day-to-day needs of the TC39 committee. Nevertheless, in practice most functions from the ECMA standard
JSExplain: a Double Debugger for JavaScript WWW’18 Companion, April 23–27, 2018, Lyons, France
and run_binary_op s c op v1 v2 =
match op with
| C_binary_op_add -> run_binary_op_add s c v1 v2
...
and run_binary_op_add s0 c v1 v2 =
let%prim (s1, w1) = to_primitive_def s0 c v1 in
let%prim (s2, w2) = to_primitive_def s1 c v2 in
if (type_compare (type_of (Coq_value_prim w1)) Coq_type_string)
|| (type_compare (type_of (Coq_value_prim w2)) Coq_type_string)
then
let%string (s3, str1) = to_string s2 c (Coq_value_prim w1) in
let%string (s4, str2) = to_string s3 c (Coq_value_prim w2) in
res_out (Coq_out_ter (s4, (res_val (Coq_value_prim (Coq_prim_string (strappend str1 str2))))))
else
let%number (s3, n1) = to_number s2 c (Coq_value_prim w1) in
let%number (s4, n2) = to_number s3 c (Coq_value_prim w2) in
res_out (Coq_out_ter (s4, (res_val (Coq_value_prim (Coq_prim_number (n1 +. n2))))))
Figure 6: Current input syntax of our specification language: a subset of pure OCaml, extended with monadic notation.
are described as returning a “completion triple”, which either de- var run_binary_op = function (op, v1, v2) {
scribe abrupt termination or describe a value. In a number of cases, switch (op) {
case C_binary_op_add:
the value is in fact constrained to be of a particular type. For exam-
return (run_binary_op_add(v1, v2));
ple, if to_number produces a value, then this value is necessarily a ... }
number. The standard exploits this invariant implicitly in formula- };
tion such as “let n be the number produced by calling to_number”. var run_binary_op_add = function (v1, v2) {
In constrast, our code needs to explicitly project the number from var%prim w1 = to_primitive_def(v1);
the value returned. To that end, we introduce specialized monads var%prim w2 = to_primitive_def(v2);
such as if_number, written in practice “let%number n = e1 in e2”. if ((type_compare(type_of(w1), Type_string)
(An alternative approach would be to assign polymorphic types || type_compare(type_of(w2), Type_string))) {
to completion triples, however following this route would require var%string str1 = to_string(w1);
diverging slightly from ECMA’s specification in a number of places.) var%string str2 = to_string(w2);
return strappend(str1, str2);
Figure 6 shows the specification of addition in our reference
} else {
interpreter, in OCaml syntax extended with the monadic notation. var%number n1 = to_number(w1);
This code implements its informal equivalent from Figure 2. In var%number n2 = to_number(w2);
that code, s denotes the state, c denotes the environment (variable return (n1 + n2);
and lexical environment, in JS terminology), op corresponds to the }
operator (here, the constructor C_binary_op_add corresponds to the };
AST token describing the operator +), v1 and v2 corresponds to
the arguments, and w1 and w2 to their primitive values. The func- Figure 7: Generated code for the interpreter in pseudo-JS
tion strappend denote string concatenation, whereas “+.” denotes syntax, with implicit environments, state, and casts.
addition on floating pointer numbers (i.e., JS’s numbers).
First observe that, as explained earlier (§1.1), the state is threaded
throughout the code. We show in the next section how to hide the
state variables (§2.2). Observe also that the code also relies on a Figure 6) is well-suited as a non-ambiguous input language. Note
few auxiliary functions. The function type_compare implements that this code may be compiled using OCaml’s compiler in order to
comparison over JS types—to keep our language small and explicit, run test cases; the current version of our interpreter passes more
we do not want to assume a generic comparison function with than 5000 test cases from the official test suite (test262).
nontrivial specification. The functions to_primitive_def, to_string,
and to_number are internal functions from the specification that 2.2 Translation into Pseudo-JS Syntax
implement conversions. These operations might end up evaluating Although we believe that it is a desirable feature to have a source
arbitrary user code, and thus could perform side-effects or raise langage fully explicit, there is also virtue in pretty-printing the
exceptions, hence the need to wrap them in monadic let-bindings. source code of our interpreter in a more concise syntax. The “noise”
One important feature of this source language is that it does that appears in the formal specification (e.g. Figure 6) comes from
not involve any “implicit” mechanism. All type conversions are three main sources:
explicit in the code, so it is always perfectly clear what is meant.
In particular, there is no need to type-check the code to figure out (1) every function takes as argument the environment;
its semantics. In summary, the OCaml code of the interpreter (e.g., (2) every function takes as argument and returns a description
of the mutable state (a.k.a. heap);
WWW’18 Companion, April 23–27, 2018, Lyons, France Arthur Charguéraud, Alan Schmitt, and Thomas Wood
(3) values are typically built using numerous constructors, e.g. Figure 8 illustrates the output of translating from our OCaml
C_value_prim, which lifts a number (an OCaml value of type subset towards JS. Note that this code is not meant for human
float) into a JS value (an OCaml value of type value). consumption. We implement monadic operators as function calls,
Fortunately, we can easily eliminate these three sources of noises. introduce the return keyword where necessary, encode sum types
First, the environment is almost always passed unchanged. It as object literals with a tag field, encode tuples as arrays (encoding
may be modified only during the scope of a function call, a with tuples as object literals would work too), turn constructor appli-
construct, or a block. When it is modified, new bindings are simply cations into functions calls, implement pattern matching by first
pushed into the environment (which behaves like a stack), and switching on the tag field then binding fresh variables to denote
subsequently popped. Thus, we may assume, like the ECMA speci- the arguments of constructors.
fication does, that the environment is stored in a global state. This We thus obtain an executable JS interpreter in JS which, like our
saves the need to pass an argument called “c” around. JS interpreter in OCaml, may be used for executing test cases. One
Second, the description of the mutable state is threaded through interest of the JS version is that it may be easily executed inside
the code. The “current state” is passed as argument to every function a browser, a set up that might be more convenient for a number
that might perform side-effects, and, symmetrically, the “updated of users. One limitation, however, is that the number of steps that
state” is returned to the caller, which binds a fresh name for it. can be simulated may be limited on JS virtual machines that do
Considering that there is only one version of the state at any given not optimize tail-recursive function calls. Indeed, the execution
point of an execution, we may assume, like the ECMA specification of monadic code involves repeated calls to continuations, whose
does, that state to be stored in a global variable. This saves the need (tail-call) invocation unnecessarily grows the call stack.
to pass values called “s1”, “s2”... around. To set up our interactive debugger, we produce, from our OCaml
Third, the presence of many constructors is due to the need for source code, an instrumented version of the JS translation. This
casts. Many of these casts could, however, be viewed as “implicit instrumented code produces execution traces as a result of inter-
casts” (or “coercions”, in Coq’s terminology). For a carefully chosen preting an input JS program. These traces store information about
set of casts, defined once and for all, and for a well-typed program all the states that the interpreter goes through. In particular, each
with implicit casts, there exists a unique (non-ambiguous) way to event in the trace provides information about the code pointer and
insert casts in order to make the program type-check. Although we the instantiations of local variables from the interpreter code.
have previously argued that explicit casts are useful, as they allow More precisely, we log events at every entry point of a function,
giving a semantics that does not depend on type-checking, we now every exit point, and on every variable binding. Each event captures
argue that it may also be useful to pretty-print the code assuming the state, the stack, and the values of all local variables in scope of
implicit casts, in order to improve readability. the interpreter code at the point where the event gets triggered. To
In summary, we propose to the reader of the specification a reduce noise in the trace, we only log events in the core code of the
version that features implicit state, implicit context, and implicit interpreter, and not the code from the auxiliary libraries. Overall, an
casts. Given that we are playing the game of pretty-printing syntax, execution of the instrumented interpreter on some input JS program
we take the opportunity to switch along the way to a JS-friendly produces an array of events. This array can then be investigated
syntax, using brackets and semicolons. This target language, called using our double debugger (§4).
pseudo-JS syntax, consists of a subset of the JS syntax, extended Figure 9 shows an example snippet of code, giving an idea of the
with monadic notation, and an extended switch construct that is mechanisms at play. Note, again, that this code is not meant for hu-
able to bind variables (like OCaml’s pattern matching, but restricted man consumption. The function log_event augments the trace. Con-
to non-nested patterns for simplicity). sider for instance log_event("Main.js", 4033, ctx_747, "enter").
The pretty-printing of the addition operator in pseudo-JS syntax The first two arguments identify the position in the source file, as a
appears in Figure 7. To illustrate our extended pattern matching file name and a unique token used to recover the line numbers. The
syntax feature of pseudo-JS, we show below an excerpt from the third argument is a context describing values of the local variables,
main switch that interprets an expression. and the fourth argument describes the type of event.
When investigating the trace, we need to be able to highlight the
switch (t) { corresponding line of the interpreter code. We wish to be able to do
case Coq_expr_identifier(x):
so for the three versions of the interpreter code: the OCaml version,
var%run r = identifier_resolution(x); return (r);
the pseudo-JS version, and the plain JS version. To implement this
case Coq_expr_binary_op(e1, op, e2): ...
feature, our generator, when processing the OCaml source code,
also produces a table that maps, for each version and for each file
3 TRACE-PRODUCING EXECUTIONS of the interpreter, event tokens to line numbers.
JSExplain is a tool for interactively investigating execution traces The contexts stored in events are extended each time a function is
of our JS interpreter executing example JS programs. The interface entered, a new variable is declared, or the function returns (so as to
consists of a web page [8] that embeds a JS parser and a trace- capture the returned value). Contexts are represented as a purely-
producing version of our interpreter implemented in standard JS. functional linked list of mappings between variable names and
So far, we have shown how to translate the OCaml source into values. This representation maximizes sharing and thus minimize
pseudo-JS syntax (§2.2). In this section, we explain how to translate the memory footprint of the generated trace. The length of the trace
the OCaml source into proper JS syntax, and then how to instrument grows linearly with the number of execution steps performed. For
the JS code in a systematic way for producing execution traces. example, the simple program “var i = 0; while (i < N) { i++ }”
JSExplain: a Double Debugger for JavaScript WWW’18 Companion, April 23–27, 2018, Lyons, France
var run_binary_op_add = function (s0, c, v1, v2) {
return (if_prim(to_primitive_def(s0, c, v1), function(s1, w1) {
return (if_prim(to_primitive_def(s1, c, v2), function(s2, w2) {
if ((type_compare(type_of(Coq_value_prim(w1)), Coq_type_string())
|| type_compare(type_of(Coq_value_prim(w2)), Coq_type_string()))) {
return (if_string(to_string(s2, c, Coq_value_prim(w1)), function(s3, str1) {
return (if_string(to_string(s3, c, Coq_value_prim(w2)), function(s4, str2) {
return (res_out(Coq_out_ter(s4, res_val(
Coq_value_prim(Coq_prim_string(strappend(str1, str2))))))); }));}));
} else { ... }})); }));
};
Figure 8: Snippet of generated code for the interpreter in standard JS syntax, without trace instrumentation.
var run_binary_op_add = function (s0, c, v1, v2) {
var ctx_747 = ctx_push(ctx_empty, [{key: "s0", val: s0}, {key: "c", val: c}, {key: "v1", val: v1}, {key: "v2", val: v2}]);
log_event("JsInterpreter.js", 4033, ctx_747, "enter");
var _return_1719 = if_prim((function () {
log_event("JsInterpreter.js", 3985, ctx_747, "call");
var _return_1700 = to_primitive_def(s0, c, v1);
log_event("JsInterpreter.js", 3984, ctx_push(ctx_747, [{key: "#RETURN_VALUE#", val: _return_1700}]), "return");
return (_return_1700); }()),
function(s1, w1) { ... });
log_event("JsInterpreter.js", 4028, ctx_push(ctx_748, [{key: "#RETURN_VALUE#", val: _return_1718}]), "return");
return (_return_1718);
});
log_event("JsInterpreter.js", 4032, ctx_push(ctx_747, [{key: "#RETURN_VALUE#", val: _return_1719}]), "return");
return (_return_1719);
};
Figure 9: Snippet of generated code for the interpreter in standard JS syntax, with trace instrumentation.
AST of JS. We instrument the JS code to produce a trace of events. This
Esprima interpreted
interpreted compilation is done ahead of time and depicted by solid arrows.
program
program When hitting the run button, the flow depicted by the dotted
arrows occurs. The web page parses the code from the text area,
compiler
using the Esprima library [7]. This parser produces an AST, with
web page
Libraries nodes annotated with locations. This AST is then provided as input
Interpreter (JS) to the instrumented interpreter, which generates a trace of events.
and libraries trace This trace may then be inspected and navigated interactively.
Interpreter
(OCaml) (anno- For a given event from the execution trace, our interface high-
tated JS) lights the corresponding piece of code from the interpreter, and
annotating shows the values of the local variables, as illustrated in Figure 11. It
compiler also highlights the corresponding piece of code in the interpreted
program, as illustrated at the top of Figure 13, and displays the state
Figure 10: Architecture of JSExplain.
and the environment of the program at that point of the execution,
as illustrated in Figure 12.
generates a trace of size 2 990 for N = 1, of size 14 166 for N = 10, Recovering the information about the interpreted code is not
of size 126 126 for N = 100, and of size 1 245 726 for N = 1000. completely straightforward. For example, to recover the fragment
The fact that these numbers are large reflects the fact that the of code to highlight, we find in the trace the closest previous event
reference interpreter is inherently vastly inefficient, as it follows that contains a call to function with an argument named _term_.
the specification faithfully, without any optimization. Due to our This argument corresponds to the AST of a subexpression, and
use of functional data structures, the memory footprint of the trace this AST is decorated (by the parser) with locations. Note that, for
should be linear in the length of the trace. We have not observed efficiency reasons, we associate to each event from the trace its
the memory footprint to be a limit, but if it were we could more corresponding _term_ argument during a single pass, performed
carefully select which events should be stored. immediately after the trace is produced.
Similarly, we are able to recover the state and environment asso-
4 JSEXPLAIN: A DOUBLE DEBUGGER FOR JS ciated with the event. The state of the interpreted program consists
The global architecture of JSExplain is depicted in Figure 10. Starting of four fields: the strictness flag, the value of the this keyword,
from our JS interpreter in OCaml, we generate a JS interpreter in
WWW’18 Companion, April 23–27, 2018, Lyons, France Arthur Charguéraud, Alan Schmitt, and Thomas Wood
Figure 11: Display of the variables from the interpreter code Figure 13: Example of a conditional breakpoint, constrain-
ing the state of both the interpreter and the interpreted code.
a change in the location on the subexpression evaluated in the
interpreted code, and source cursor finds the last event in the trace
for which the associated subexpression contains the active cursor
in the “source program” text area.
The aforementioned tools are sufficient for simple explorations
of the trace, yet we have found that it is sometimes useful to reach
events at which specific conditions occur, such as being at a specific
line in the interpreter, in the interpreted code, with variables from
the interpreter or interpreted code having specific values. We thus
provide a text box to enter arbitrary breakpoint conditions to be
evaluated on events from the trace. For example, the condition in
Figure 13 reaches the next occurrence of a call to run_binary_op_add
in a context where the source variable j has value 1. The break
point condition may be any JS expression using the following API:
I_line() returns the current line of the interpreter, S_line() returns
Figure 12: Display of the state and environment of the inter- the current line of the source, I('x') returns the value of x in the
preted code. The environment includes the local variables. interpreter, S_raw('x') returns the value of x in the source (e.g. the
JS object {tag: "value_number", arg: 5}), and S('x') returns the
the lexical environment, and the variable environment. We imple- JS interpretation of the value of x in the source (e.g. the JS value 5).
mented a custom display for these elements, and also for values of
the languages, in particular for objects: one may click on an object 5 RELATED WORK
to reveal its contents and recursively explore it. There are many formal semantics of JavaScript, from pen-and-paper
We provide several ways to navigate the trace. First, we provide ones [10], to the aforementioned JSCert [3] and KJS [11]. As de-
buttons for reaching the beginning or end of the execution, and but- scribed in §1.4, these semantics are admirable but lack crucial fea-
tons for stepping one event at a time. Second, we provide, similarly tures to be actively used in the standardization effort.
to debuggers, next and previous buttons for skipping function calls, To our knowledge, the closest work to the double-debugger
as well as a finish button to reach the end of the current function. approach is the multi-level debugging approach of Kruck et al. [9].
These features are implemented by navigating the trace, keeping They present a debugger for an interpreter for domain-specific
track of the number of enter and return events. Third, we provide languages that lets developers choose the level of abstraction at
buttons for navigation based not on steps related to the interpreter which they debug their program. An abstraction is a way to display
program but instead based on steps of the interpreted program: some values (encoded in the host language, or as present in the DSL)
source previous and source next find the closest event which induces as well as showing only stack frames that represent computation
JSExplain: a Double Debugger for JavaScript WWW’18 Companion, April 23–27, 2018, Lyons, France
at the DSL level. Our technique is more general as it does not focus the possibility of automatically generating pretty-big-step [5] defini-
on domain-specific languages. tions from the reference semantics expressed in our small language,
In fact, our double-debugger approach could be easily adapted possibly using some amount of annotation to guide the process.
to interpreter for other languages than JS. To that end, it suffices to (4) To close even further the gap between a formal language and
implemented an interpreter for the desired language in the subset the English prose, we could also investigate the possibility of auto-
of OCaml that we support, and to provide code for extracting and matically generating English sentences from the code. Indeed, the
displaying the term and state associated with a given event. We prose from the ECMAScript standard is written in such a systematic
have recently followed that approach and adapted our framework manner that this should be doable, at least to some extent.
to derive a double-debugger for (a significant subset of) the OCaml
programming language. ACKNOWLEDGMENTS
Regarding the translation from OCaml to JS that we imple- We acknowledge funding from the ANR project AJACS ANR-14-
ment, one might consider using an existing, general-purpose tool. CE28-0008 and the CominLabs project SecCloud.
Js_of_ocaml [17] converts OCaml bytecode into efficient JS code.
Presumably, we could implement the logging instrumentation as an REFERENCES
OCaml source-to-source translation and then invoke Js_of_ocaml. [1] 2017. Babel. (October 25, 2017). https://babeljs.io/.
Yet, with that approach, we would need to convert the representa- [2] 2017. Babel proxy plugin. (October 25, 2017). https://www.
tion of trace events from the encoding of these values performed npmjs.com/package/babel-plugin-proxy.
by Js_of_ocaml into proper JS objects that we can display in the [3] Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa
interactive interface. This conversion is nontrivial, as some infor- Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt,
mation, such as the name of constructors, is lost in the process. As and Gareth Smith. 2014. A trusted mechanised javascript
we already implemented a translator from OCaml to pseudo-JS, it specification. In Proceedings of POPL 2014, 87–100.
was simpler to implement a translator from OCaml to plain JS. [4] 2017. Bucklescript. (October 27, 2017). https://bucklescript.
Another translator from OCaml to JS is Bucklescript [4], which github.io/bucklescript/.
was released after we started our work. Similarly to our transla- [5] Arthur Charguéraud. 2013. Pretty-big-step semantics. In Pro-
tor, Bucklescript converts OCaml code into JS code advertised as ceedings of ESOP 2013 (LNCS). Volume 7792. Springer, 41–
readable. Bucklescript also has the limitation that the names of con- 60.
structors are lost, although presumably this could be easily fixed. [6] ECMA. 2017. Ecmascript 2017 language specification (ecma-
Besides, if we wanted to revisit our implementation to base it on 262, 8th edition). (June 2017). https://www.ecma-international.
Bucklescript, for trace generation we would need to either modify org/ecma-262/8.0/index.html.
Bucklescript, which is quite complex as it covers the full OCaml [7] 2017. ECMAScript parsing infrastructure for multipurpose
language, or to reimplement trace instrumentation at the OCaml analysis. (October 26, 2017). http://esprima.org/.
level, which should be doable yet would involve a bit more work [8] 2017. JSExplain. (October 26, 2017). https://jscert.github.io/
than at the level of untyped JS code. jsexplain/branch/master/driver.html.
[9] Bastian Kruck, Stefan Lehmann, Christoph Keßler, Jakob
6 CONCLUSION AND FUTURE WORK Reschke, Tim Felgentreff, Jens Lincke, and Robert Hirschfeld.
We presented JSExplain to TC391 and the committee expressed 2016. Multi-level debugging for interpreter developers. In
strong interest. They would like us to extend our specification to MODULARITY (Companion). ACM, 91–93.
cover all of the specification. We have almost finished the formaliza- [10] Sergio Maffeis, John C. Mitchell, and Ankur Taly. 2008. An
tion of proxies, which are a challenging addition to the language as operational semantics for javascript. In Proceedings of APLAS
they change many internal methods. Although all members seem 2008 (LNCS). Volume 5356. Springer, 307–325.
to agree that the current toolset for developing the specification is [11] Daejun Park, Andrei Stefanescu, and Grigore Rosu. 2015. KJS:
inappropriate, it requires a strong leadership and a consensus to a complete formal semantics of javascript. In Proceedings of
commit to a new toolchain. Our goal is to cover the current version PLDI 2015. ACM, 346–356.
of ECMAScript, we currently cover ECMAScript 5, and to help [12] 2017. Reason. (October 27, 2017). https://reasonml.github.io/.
committee members use it to formalize new additions to JavaScript. [13] Grigore Rosu and Traian-Florin Serbanuta. 2010. An overview
There are numerous directions for future work. (1) We plan to set of the K semantic framework. Journal of Logic and Algebraic
up a modular mechanism for describing unspecified behaviors (e.g. Programming, 79, 6, 397–434.
“for-in” enumeration order) as well as browser-specific behaviors [14] 2017. TC39 proposals. (October 26, 2017). https://github.com/
(sometimes browsers deviate from the specification, for historical tc39/proposals.
reasons). (2) We could investigate the possibility of extending the [15] 2017. Test262. (October 26, 2017). https://github.com/tc39/
formalization of the standard by also covering the parsing rules of test262.
JS; currently, our semantics is expressed with respect to the AST of [16] The Coq development team. 2014. The Coq proof assistant
the input program. (3) To re-establish a link with the original JSCert reference manual. Version 8.4. http://coq.inria.fr.
inductive definition, which is useful for conducting formal proofs [17] Jérôme Vouillon and Vincent Balat. 2014. From bytecode to
about the metatheory of the langage, we would like to investigate javascript: the js_of_ocaml compiler. Software: Practice and
1 https://tc39.github.io/tc39-notes/2016-05_may-25.html#jsexplain-as--tw
Exprerience, 44, 8, 951–972.