Martin Bodin — Thesis Companion

Mash-ups

This webpage is by default not a mash-up, but it is nevertheless possible to include various programs from various sources. If you are using a browser extension such as Collusion, this webpage would suddenly be linked to various other websites. Warning: by clicking on the following link, various scripts from various authors will be included in this webpage; in particular, any private information present in the JavaScript heap will be accessible to them. Furthermore, the page might become unstable. The added programs include programs such as Google Analytics, social programs (see the bottom of this webpage), and programs such as TogetherJS. Some of these programs may store cookies or track your browser once included in this webpage: proceed with caution.

Effect of the new-construct

This file corresponds to Figure 1.6 of the dissertation.

One of the pitfalls of the with-construct

This file corresponds to Program 1.1 of the dissertation. The attacking file sets Object.prototype.f to a function constant to 18. This changes the behaviour of Program 1.2 (among others), as explained in Section 1.2.3.2 of the dissertation. Note that running the attacking file after the main file, then running the main file again will also result in 42, as the first execution of the main file already assign a global function f, which shadows the function f of the prototype of objects.

A program equivalent to "Bodin" in the default environment

This file corresponds to Program 1.2 of the dissertation. Note that this program uses some assumptions about the initial heap; these assumptions are valid in most real-world interpreters, but are necessarily not in EcmaScript.

A program with potentially unexpected implicit type conversions

This file corresponds to Program 1.3 of the dissertation. Warning: this program changes Array.prototype.toString, which will likely interact with the results given by the other programs of this webpage.

A common parsing pitfall

These files corresponds to Programs 1.6a and 1.6b of the dissertation.

A JavaScript program without lexical scoping

This file corresponds to Program 1.7 of the dissertation.

JavaScript queries

All the program run in this webpage are run in the same environment. This small buffer enables the reader to check its own inputs. This can also be useful to check the state of the heap of JSRef, if it is the chosen interpreter (see below).

The JSCert project

What is presented in Chapter 2 of the dissertation presents the effort which I have been part of during the JSCert project. The webpage of this project can be informative for the interested reader. The second link points to the Coq files of the project repository. Most snippets of Chapter 2 come from this repository.

JSExplain

JSExplain is a project born from JSCert. It is meant to show a step by step execution of a JavaScript program, as it is executed in the EcmaScript specification. This webpage is an opportunity to run JSRef directly in the browser: just write any JavaScript program in the upper left text box, click on the Run button, then on the End button, and the output from JSRef will be indicated at the bottom of the page, as well as the current state of the environment in the upper right interactive box.

JSRef

This page uses eval to run JavaScript programs. Alternatively, it is possible to use JSRef directly in this webpage: JSRef has been extracted into OCaml, then converted into JavaScript.

Note that JSRef uses a distinct heap from eval (expressed as a JavaScript data structure). The heap of JSRef is persistent between the different executions run in this webpage (including if you switch back and forth to eval): to reset the JavaScript environment, consider reloading the webpage.

Also note that the choices of the initial heap in JSRef may be very different from what usual browsers choose; for instance, the implicit prototype of the global object is set to null and does not link to the prototype of Object.

Completion triples as they were defined in an early version of JSCert

This file corresponds to Program 2.2a of the dissertation.

Current JSCert completion triples

This file corresponds to Program 2.2b of the dissertation.

Return values of various while statements

This file corresponds to Program 2.4 of the dissertation. Disclaimer: there is only one test (S12.6.2_A5.js) in Test262 testing the while-construct in combination with both eval and break, specifically aiming at checking the value part of the returned completion triple. This example is much more complex than the previously mentioned test, and a lot of browsers still fail on this particular example.

A snippet of JSCert AST

This file corresponds to Program 2.6 of the dissertation.

Definition of some intermediary terms in JSCert

This file corresponds to Program 2.7 of the dissertation.

Rules red-stat-abort and red-stat-while-6-abort in JSCert

This file corresponds to Program 2.8 of the dissertation. The rule red-stat-while-6-abort of the dissertation is named red_stat_while_6_normal in the Coq development.

Definition of the initial heap in JsInit.v

This file corresponds to Program 2.9 of the dissertation.

Definition in JSRef of the potentially looping features of JavaScript

This file corresponds to Program 2.10 of the dissertation.

Two monadic operators of JSRef

This file corresponds to Program 2.11 of the dissertation.

JSRef semantics of while-loops

This file corresponds to Program 2.12 of the dissertation.

Proof of correctness for the while construct

This file corresponds to Program 2.14 of the dissertation.

Snippet of the JavaScript prelude of the testing architecture

This file corresponds to Program 2.17 of the dissertation.

Example of test in Test262

This file corresponds to Program 2.18 of the dissertation.

The for-in construct in KJS

This file corresponds to Program 2.21 of the dissertation.

The function @EnumerateAllProperties builds a map (indicated by the type @m). The notation .Map represents an empty map. In general, maps are a list of association statements of the form P |-> OP. The pattern matching of Line 3,118 (rule @ForInAux(L:Exp, O:Oid, @m(P:Var |-> OP:Oid Ps:Map), S:Stmt)) thus extracts (to my understanding of K) the first element P |-> OP of a map, leaving the maps Ps to be analysed afterwards.

Concrete semantics

This file shows the concrete semantics defined in this chapter. It corresponds to the rules of Figure 3.4 of the dissertation.

Concrete semantics

This file shows the concrete semantics defined in this chapter. It corresponds to the rules of Figure 4.2 of the dissertation.

Coq Material

Most of the Coq material of this chapter can be found at this webpage. It corresponds to the supplementary material of a publication published during this thesis. The language presented in the thesis dissertation is an attempt to unify several languages built during this thesis. In particular, the two languages presented in this webpage slightly differ from the one presented in the dissertation.

Flat analyser

This analyser is a flat analyser (see Section 4.6.3 of the dissertation) made from a language close to the one presented in this chapter. As stated in the dissertation, flat analysers are close to interpreters. To make it runnable in the browser, the Coq analyser has been extracted to OCaml, then compiled into JavaScript.

The language presented in the thesis dissertation is an attempt to unify several languages built during this thesis. As a consequence, the different abstract interpreters presented here have slightly different syntax and semantics.

Sign analyser

This analyser is an analyser based on the sign abstract domain (see Section 3.2.2 of the dissertation) made from a language close to the one presented in this chapter. It is based on exactly the same language than the flat analyser above. To make it runnable in the browser, the Coq analyser has been extracted to OCaml, then compiled into JavaScript.

Abstract semantics

This file shows the abstract semantics defined in this chapter. It corresponds to the rules shown in Section 4.4.1.1 of the dissertation.

Concrete semantics of functions

This file shows the concrete semantics of the extended semantics defined in Section 4.7.1 of this chapter. It corresponds to the rules of Figures 4.15 and 4.17 of the dissertation.

Coq Material

The Coq material of this chapter can be found in this archive. It can also be found in the Coq material of the next chapter.

Concrete semantics

This file shows the concrete semantics defined in this chapter. It corresponds to the rules of Figure 6.2 of the dissertation.

Coq Material

The Coq material of this chapter can be found in this archive. The language presented in the thesis dissertation is an attempt to unify several languages built during this thesis. In particular, the language presented in this archive slightly differs from the one presented in the dissertation.

Flat analyser

This analyser is a flat analyser (see Section 4.6.3 of the dissertation) made from a language close to the one presented in this chapter. As stated in the dissertation, flat analysers are close to interpreters. To make it runnable in the browser, the Coq analyser has been extracted to OCaml, then compiled into JavaScript.

The language presented in the thesis dissertation is an attempt to unify several languages built during this thesis. As a consequence, the different abstract interpreters presented here have slightly different syntax and semantics.

Abstract semantics

This file shows the abstract semantics defined in this chapter. It corresponds to the rules of Figure 6.14 of the dissertation.

About the correctness of the frame rules

We have claimed in Section 6.4.5 of the dissertation to have shown that the frame rules are not provable correct as-is in our formalism. This document presents this proof.