Formalizing JavaScript

Dave Herman
Northeastern University

Background

Background:

How can formal methods help?

Introducing JavaScript

Expressions

e::=λx.e
| (e e)
| x

(At some level, anyway.)

Expressions

e::=function(x) e
| e(e)
| x
| e ? e : e
| c

Evaluation Contexts

E::=E(e)
| v(E)
| E ? e : e
|

Are We There Yet?

...

10.1.6 Activation Object

When control enters an execution context for function code, an object called the activation object is created and associated with the execution context. The activation object is initialised with a property with name arguments and attributes { DontDelete }. The initial value of this property is the arguments object described below.

The activation object is then used as the variable object for the purposes of variable instantiation. The activation object is purely a specification mechanism. It is impossible for an ECMAScript program to access the activation object. It can access members of the activation object, but not the activation object itself. When the call operation is applied to a Reference value whose base object is an activation object, null is used as the this value of the call.

...
Evaluation Contexts
or, Algebra, the Ultimate Interface

Evaluation Contexts

E::=E(e)
| v(E)
| E ? e : e
|

Evaluation Contexts

E::=E[(e)]
| E[v()]
| E[? e : e]
|

Evaluation Contexts

F::=(e)
| v()
| ? e : e

E::=| F[E]← outside-in

E::=| E[F]← inside-out

Evaluation Contexts

E : expr expr

E[e]E(e) (application)

E1[E2]E1 E2 (composition)

(E1 E2) E3 = E1 (E2 E3)

Evaluation Contexts

Who needs parentheses?

E::=| F E
E::=| E F

These grammars generate equivalent sets of contexts.

Okay, That’s not JavaScript

e::=function(x) e
| e(e)
| x
| e ? e : e
| c

A Little More Honest

e::=function(x) s
| e(e)
| x
| e ? e : e
| c
s::=e;
| { s ... }
| return e;
| if (e) s s

What Type of Context is This?

if () return v;

It’s the context of an expression.

It produces a statement.

expr → stmt

Outside-in

E::=E(e)
| v(E)
| E ? e : e
|
| call S
S::=S s ...
| ·
| E;
| return E;
| if (E) s s

Outside-in

Outside-in:

Inside-out

E::=E[(e)]
| E[v()]
| E[? e : e]
|
| S[;]
| S[return;]
| S[if () s s]
S::=S[· s ...]
| ·
| E[call ·]

Inside-out

Inside-out:

Why the Inversion?

Why use the inside-out formulation?

Let’s Modularize This Definition

E::=E[(e)]
| E[v()]
| E[? e : e]
|
| S[;]
| S[return;]
| S[if () s s]
S::=S[· s ...]
| ·
| E[call ·]

Context Frames

F::=(e)
| v()
| ? e : e
| ;
| return;
| if () s s
| · s ...
| call ·

Context Frames, Sorted

Fe e::=(e)
| v()
| ? e : e

Fe s::=;
| return;
| if () s s

Fs e::=call ·

Fs s::=· s ...

Context Frames, Sorted

Fe e, Fs s : context builders

Fe s, Fs e : context adapters

The (Mutual) Recursion

S::=·
| S Fs s
| E Fs e S

E::=
| E Fe e
| S Fe s E

For statement top-level, leave out □

For expression top-level, leave out ·

Another Step

So far:

Modularizing the Recursion

“Small” contexts:

S::=· | S Fs s
E::=| E Fe e

Boundaries:

A::=S Fe s E← activation frames!
A Fs e A ... Fs e A← call stack!

Putting It All Together

S::=· | S Fs s
E::=| E Fe e← local expression stack (bounded)
A::=S Fe s E

Assuming statement top-level:

S::=(A Fs e )* S
E::=(A Fs e )* A

Abstract Machine Derivations

What was this derivation?

Evaluation Rules

Abstract Machine Configurations

The CEKD machine:

ExampleTypeInterpretation
<e, ρ, A, A*>expression configurationevaluating expression e
<s, ρ, S, A*>statement configurationexecuting statement s
<v, A, A*>value configurationpopping result v

Procedure Calls

<e0(e), ρ, A, D><e0, ρ, A (e)ρ, D>
<v, A (e)ρ, D><e, ρ, A v(), D>
<v, A (function(x) s, ρ)(), D><s, ρ[v/x], ·, D A>
<return e;, ρ, S, D><e, ρ, S return;, D>
<v, S return;, D A><v, A, D>

But what about tail calls?

Tail Calls

For this simple calculus:

  1. <return e;, ρ, S, D A> <e, ρ, A, D>
  2. get rid of return;

(complicated somewhat by try)

Stratego

Executable Semantics

Motivation:

Another Motivation

A social motivation for an executable semantics:

Why Not Use A Functional Language?

Requirements:

Stratego

Rewriting Rules

  EvalLit :
    Machine {
       Expr:  expr,
       Scope: scope,
       Frame: frame,
       Stack: stack,
       Heap:  heap
    }
  ->
    Machine {
       Result: <LiteralValue> expr,
       Frame:  frame,
       Stack:  stack,
       Heap:   heap
    }
  where <IsLiteral> expr

Custom Syntax

  EvalFunction :
    Machine {
       Expr:  #( function($@args)$body ),
       Scope: scope,
       Frame: frame,
       Stack: stack,
       Heap:  heap
    }
  ->
    Machine {
       Result: ObjectVal(loc),
       Frame:  frame,
       Stack:  stack,
       Heap:   heap'
    }
  where obj := Object(None,
                      Some(Closure(#( function($@args)$body ), scope)),
                      Table([]))
      ; (loc, heap') := <Allocate1>(obj, heap)

Machine Interface

  Start :
    expr -> Machine {
               Expr:  expr,
               Scope: [ ScopeObject([("this", 1)]) ],
               Frame: [],
               Stack: [],
               Heap:  [(0, Object(None, None, Table([]))),
                       (1, ObjectVal(0))]
            }

  Finish :
    Machine {
       Result: val,
       Frame:  [],
       Stack:  [],
       Heap:   heap
    } -> <GetValue>(val, heap)

Interpreter

  eval = EvalLit + EvalFunction + PushCall + ...
  apply = PopCaller + PopCallee + ...

  step = eval + apply + Finish

  eval-program =
    parse
    ; pretty-print
    ; Start
    ; repeat(newline; pretty-print; step)

  main =
      parse-command-line
      ; read-input-text
      ; eval-program

Demo