DOKK Library

JSExplain: a Double Debugger for JavaScript

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                                      

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.                                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.                                              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)
                     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))))))
                     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                                           When hitting the run button, the flow depicted by the dotted
                                                                          arrows occurs. The web page parses the code from the text area,
                                                                          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.
      (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).
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        
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       
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).
level, which should be doable yet would involve a bit more work             [8]   2017. JSExplain. (October 26, 2017).
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).
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).
(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).
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.
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
                                                                                  Exprerience, 44, 8, 951–972.