Skip to content

Commit

Permalink
Implement reduction and text format (WebAssembly#6)
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg authored Feb 22, 2021
2 parents 7704c23 + dfb8dad commit 6b0b593
Show file tree
Hide file tree
Showing 18 changed files with 746 additions and 86 deletions.
15 changes: 11 additions & 4 deletions interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -225,7 +225,7 @@ let global_type s =
let def_type s =
match peek s with
| Some 0x60 -> FuncDefType (func_type s)
| Some 0x61 -> ContDefType (cont_type s)
| Some 0x5f -> ContDefType (cont_type s)
| None -> ignore (vs7 s); assert false (* force error *)
| _ -> error s (pos s) "malformed type definition"

Expand Down Expand Up @@ -553,9 +553,14 @@ let rec instr s =
| 0xd4 -> br_on_null (at var s)

| 0xe0 -> cont_new (at var s)
| 0xe1 -> cont_suspend (at var s)
| 0xe2 -> cont_throw (at var s)
| 0xe3 -> cont_resume (vec var_pair s)
| 0xe1 -> suspend (at var s)
| 0xe2 -> resume (vec var_pair s)
| 0xe3 -> resume_throw (at var s)
| 0xe4 ->
let bt = block_type s in
let es' = instr_block s in
end_ s;
guard bt es'

| 0xfc as b ->
(match vu32 s with
Expand Down Expand Up @@ -656,6 +661,7 @@ let import_desc s =
| 0x01 -> TableImport (table_type s)
| 0x02 -> MemoryImport (memory_type s)
| 0x03 -> GlobalImport (global_type s)
| 0x04 -> EventImport (event_type s)
| _ -> error s (pos s - 1) "malformed import kind"

let import s =
Expand Down Expand Up @@ -723,6 +729,7 @@ let export_desc s =
| 0x01 -> TableExport (at var s)
| 0x02 -> MemoryExport (at var s)
| 0x03 -> GlobalExport (at var s)
| 0x04 -> EventExport (at var s)
| _ -> error s (pos s - 1) "malformed export kind"

let export s =
Expand Down
7 changes: 4 additions & 3 deletions interpreter/binary/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -215,9 +215,10 @@ let encode m =
| FuncBind x -> op 0x16; var x

| ContNew x -> op 0xe0; var x
| ContSuspend x -> op 0xe1; var x
| ContThrow x -> op 0xe2; var x
| ContResume xls -> op 0xe3; vec var_pair xls
| Suspend x -> op 0xe1; var x
| Resume xls -> op 0xe2; vec var_pair xls
| ResumeThrow x -> op 0xe3; var x
| Guard (bt, es) -> op 0xe4; block_type bt; list instr es; end_ ()

| Drop -> op 0x1a
| Select None -> op 0x1b
Expand Down
182 changes: 146 additions & 36 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,14 @@ open Source
module Link = Error.Make ()
module Trap = Error.Make ()
module Exception = Error.Make ()
module Suspension = Error.Make ()
module Exhaustion = Error.Make ()
module Crash = Error.Make ()

exception Link = Link.Error
exception Trap = Trap.Error
exception Exception = Exception.Error
exception Suspension = Suspension.Error
exception Exhaustion = Exhaustion.Error
exception Crash = Crash.Error (* failure that cannot happen in valid code *)

Expand Down Expand Up @@ -44,7 +46,7 @@ let numeric_error at = function
| exn -> raise exn


(* Administrative Expressions & Configurations *)
(* Administrative Expressions & Continuations *)

type 'a stack = 'a list

Expand All @@ -61,15 +63,48 @@ and admin_instr' =
| Plain of instr'
| Refer of ref_
| Invoke of func_inst
| Label of int * instr list * code
| Local of int * value list * code
| Frame of int * frame * code
| Catch of int * event_inst option * instr list * code
| Handle of (event_inst * idx) list option * code
| Trapping of string
| Throwing of event_inst * value stack
| Suspending of event_inst * value stack * ctxt
| Returning of value stack
| ReturningInvoke of value stack * func_inst
| Breaking of int32 * value stack
| Label of int * instr list * code
| Local of int * value list * code
| Frame of int * frame * code
| Catch of int * event_inst option * instr list * code

and ctxt = code -> code

type cont = int * ctxt (* TODO: represent type properly *)
type ref_ += ContRef of cont

let () =
let type_of_ref' = !Value.type_of_ref' in
Value.type_of_ref' := function
| ContRef _ -> BotHeapType (* TODO *)
| r -> type_of_ref' r

let () =
let string_of_ref' = !Value.string_of_ref' in
Value.string_of_ref' := function
| ContRef _ -> "cont"
| r -> string_of_ref' r

let plain e = Plain e.it @@ e.at

let is_jumping e =
match e.it with
| Trapping _ | Throwing _ | Suspending _
| Returning _ | ReturningInvoke _ | Breaking _ ->
true
| _ -> false

let compose (vs1, es1) (vs2, es2) = vs1 @ vs2, es1 @ es2


(* Configurations *)

type config =
{
Expand All @@ -81,14 +116,6 @@ type config =
let frame inst = {inst; locals = []}
let config inst vs es = {frame = frame inst; code = vs, es; budget = 300}

let plain e = Plain e.it @@ e.at

let is_jumping e =
match e.it with
| Trapping _ | Throwing _ | Returning _ | ReturningInvoke _ | Breaking _ ->
true
| _ -> false

let lookup category list x =
try Lib.List32.nth list x.it with Failure _ ->
Crash.error x.at ("undefined " ^ category ^ " " ^ Int32.to_string x.it)
Expand Down Expand Up @@ -191,12 +218,12 @@ let rec step (c : config) : config =
vs', [Plain (Block (bt, es1)) @@ e.at]

| Let (bt, locals, es'), vs ->
let vs0, vs' = split (List.length locals) vs e.at in
let locs, vs' = split (List.length locals) vs e.at in
let FuncType (ts1, ts2) = block_type c.frame.inst bt e.at in
let vs1, vs2 = split (List.length ts1) vs' e.at in
vs2, [
Local (List.length ts2, List.rev vs0,
(vs1, [Plain (Block (bt, es')) @@ e.at])
let args, vs'' = split (List.length ts1) vs' e.at in
vs'', [
Local (List.length ts2, List.rev locs,
(args, [Plain (Block (bt, es')) @@ e.at])
) @@ e.at
]

Expand All @@ -209,7 +236,10 @@ let rec step (c : config) : config =
vs', [Catch (n2, exno, es2, ([], [Label (n2, [], (args, List.map plain es1)) @@ e.at])) @@ e.at]

| Throw x, vs ->
[], [Throwing (event c.frame.inst x, vs) @@ e.at]
let evt = event c.frame.inst x in
let EventType (FuncType (ts, _), _) = Event.type_of evt in
let vs0, vs' = split (List.length ts) vs e.at in
vs', [Throwing (evt, vs0) @@ e.at]

| Br x, vs ->
[], [Breaking (x.it, vs) @@ e.at]
Expand Down Expand Up @@ -278,6 +308,47 @@ let rec step (c : config) : config =
let f' = Func.alloc_closure (type_ c.frame.inst x) f args in
Ref (FuncRef f') :: vs', []

| ContNew x, Ref (NullRef _) :: vs ->
vs, [Trapping "null function reference" @@ e.at]

| ContNew x, Ref (FuncRef f) :: vs ->
let FuncType (ts, _) = Func.type_of f in
let ctxt code = compose code ([], [Invoke f @@ e.at]) in
Ref (ContRef (List.length ts, ctxt)) :: vs, []

| Suspend x, vs ->
let evt = event c.frame.inst x in
let EventType (FuncType (ts, _), _) = Event.type_of evt in
let args, vs' = split (List.length ts) vs e.at in
vs', [Suspending (evt, args, fun code -> code) @@ e.at]

| Resume xls, Ref (NullRef _) :: vs ->
vs, [Trapping "null continuation reference" @@ e.at]

| Resume xls, Ref (ContRef (n, ctxt)) :: vs ->
let hs = List.map (fun (x, l) -> event c.frame.inst x, l) xls in
let args, vs' = split n vs e.at in
vs', [Handle (Some hs, ctxt (args, [])) @@ e.at]

| ResumeThrow x, Ref (NullRef _) :: vs ->
vs, [Trapping "null continuation reference" @@ e.at]

| ResumeThrow x, Ref (ContRef (n, ctxt)) :: vs ->
let evt = event c.frame.inst x in
let EventType (FuncType (ts, _), _) = Event.type_of evt in
let args, vs' = split (List.length ts) vs e.at in
let vs1', es1' = ctxt (args, [Plain (Throw x) @@ e.at]) in
vs1' @ vs', es1'

| Guard (bt, es'), vs ->
let FuncType (ts1, _) = block_type c.frame.inst bt e.at in
let args, vs' = split (List.length ts1) vs e.at in
vs', [
Handle (None,
(args, [Plain (Block (bt, es')) @@ e.at])
) @@ e.at
]

| Drop, v :: vs' ->
vs', []

Expand Down Expand Up @@ -557,6 +628,10 @@ let rec step (c : config) : config =
| Label (n, es0, (vs', [])), vs ->
vs' @ vs, []

| Label (n, es0, (vs', {it = Suspending (evt, vs1, ctxt); at} :: es')), vs ->
let ctxt' code = [], [Label (n, es0, compose (ctxt code) (vs', es')) @@ e.at] in
vs, [Suspending (evt, vs1, ctxt') @@ at]

| Label (n, es0, (vs', {it = Breaking (0l, vs0); at} :: es')), vs ->
take n vs0 e.at @ vs, List.map plain es0

Expand All @@ -573,6 +648,10 @@ let rec step (c : config) : config =
| Local (n, vs0, (vs', [])), vs ->
vs' @ vs, []

| Local (n, vs0, (vs', {it = Suspending (evt, vs1, ctxt); at} :: es')), vs ->
let ctxt' code = [], [Local (n, vs0, compose (ctxt code) (vs', es')) @@ e.at] in
vs, [Suspending (evt, vs1, ctxt') @@ at]

| Local (n, vs0, (vs', e' :: es')), vs when is_jumping e' ->
vs, [e']

Expand All @@ -585,6 +664,10 @@ let rec step (c : config) : config =
| Frame (n, frame', (vs', [])), vs ->
vs' @ vs, []

| Frame (n, frame', (vs', {it = Suspending (evt, vs1, ctxt); at} :: es')), vs ->
let ctxt' code = [], [Frame (n, frame', compose (ctxt code) (vs', es')) @@ e.at] in
vs, [Suspending (evt, vs1, ctxt') @@ at]

| Frame (n, frame', (vs', {it = Returning vs0; at} :: es')), vs ->
take n vs0 e.at @ vs, []

Expand Down Expand Up @@ -630,14 +713,16 @@ let rec step (c : config) : config =
| Catch (n, exno, es0, (vs', [])), vs ->
vs' @ vs, []

| Catch (n, exno, es0, (vs', {it = Suspending (evt, vs1, ctxt); at} :: es')), vs ->
let ctxt' code = [], [Catch (n, exno, es0, compose (ctxt code) (vs', es')) @@ e.at] in
vs, [Suspending (evt, vs1, ctxt') @@ at]

| Catch (n, None, es0, (vs', {it = Throwing (exn, vs0); at} :: _)), vs ->
vs, [Label (n, [], ([], List.map plain es0)) @@ e.at]

| Catch (n, Some exn, es0, (vs', {it = Throwing (exn0, vs0); at} :: _)), vs
when exn0 == exn ->
let EventType (FuncType (ts, _), _) = Event.type_of exn in
let n' = List.length ts in
vs, [Label (n, [], (take n' vs0 at, List.map plain es0)) @@ e.at]
vs, [Label (n, [], (vs0, List.map plain es0)) @@ e.at]

| Catch (n, exno, es0, (vs', e' :: es')), vs when is_jumping e' ->
vs, [e']
Expand All @@ -646,15 +731,36 @@ let rec step (c : config) : config =
let c' = step {c with code = code'} in
vs, [Catch (n, exno, es0, c'.code) @@ e.at]

| Returning _, vs
| ReturningInvoke _, vs ->
Crash.error e.at "undefined frame"
| Handle (hso, (vs', [])), vs ->
vs' @ vs, []

| Handle (None, (vs', {it = Suspending _; at} :: es')), vs ->
vs, [Trapping "guard suspended" @@ at]

| Handle (Some hs, (vs', {it = Suspending (evt, vs1, ctxt); at} :: es')), vs
when List.mem_assq evt hs ->
let EventType (FuncType (_, ts), _) = Event.type_of evt in
let ctxt' code = compose (ctxt code) (vs', es') in
[Ref (ContRef (List.length ts, ctxt'))] @ vs1 @ vs,
[Plain (Br (List.assq evt hs)) @@ e.at]

| Breaking (k, vs'), vs ->
Crash.error e.at "undefined label"
| Handle (hso, (vs', {it = Suspending (evt, vs1, ctxt); at} :: es')), vs ->
let ctxt' code = [], [Handle (hso, compose (ctxt code) (vs', es')) @@ e.at] in
vs, [Suspending (evt, vs1, ctxt') @@ at]

| Trapping _, vs
| Throwing _, vs ->
| Handle (hso, (vs', e' :: es')), vs when is_jumping e' ->
vs, [e']

| Handle (hso, code'), vs ->
let c' = step {c with code = code'} in
vs, [Handle (hso, c'.code) @@ e.at]

| Trapping _, _
| Throwing _, _
| Suspending _, _
| Returning _, _
| ReturningInvoke _, _
| Breaking _, _ ->
assert false

in {c with code = vs', es' @ List.tl es}
Expand All @@ -665,13 +771,17 @@ let rec eval (c : config) : value stack =
| vs, [] ->
vs

| vs, {it = Trapping msg; at} :: _ ->
Trap.error at msg

| vs, {it = Throwing _; at} :: _ ->
Exception.error at "uncaught exception"

| vs, es ->
| vs, e::_ when is_jumping e ->
(match e.it with
| Trapping msg -> Trap.error e.at msg
| Throwing _ -> Exception.error e.at "unhandled exception"
| Suspending _ -> Suspension.error e.at "unhandled event"
| Returning _ | ReturningInvoke _ -> Crash.error e.at "undefined frame"
| Breaking _ -> Crash.error e.at "undefined label"
| _ -> assert false
)

| _ ->
eval (step c)


Expand Down
1 change: 1 addition & 0 deletions interpreter/exec/eval.mli
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ open Instance
exception Link of Source.region * string
exception Trap of Source.region * string
exception Exception of Source.region * string
exception Suspension of Source.region * string
exception Exhaustion of Source.region * string
exception Crash of Source.region * string

Expand Down
10 changes: 10 additions & 0 deletions interpreter/script/js.ml
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,14 @@ function assert_exception(action) {
throw new Error("Wasm exception expected");
}

function assert_suspension(action) {
try { action() } catch (e) {
/* TODO: Not clear how to observe form JS */
return;
}
throw new Error("Wasm exception expected");
}

let StackOverflow;
try { (function f() { 1 + f() })() } catch (e) { StackOverflow = e.constructor }

Expand Down Expand Up @@ -536,6 +544,8 @@ let of_assertion mods ass =
of_assertion' mods act "assert_trap" [] None
| AssertException (act, _) ->
of_assertion' mods act "assert_exception" [] None
| AssertSuspension (act, _) ->
of_assertion' mods act "assert_suspension" [] None
| AssertExhaustion (act, _) ->
of_assertion' mods act "assert_exhaustion" [] None

Expand Down
7 changes: 7 additions & 0 deletions interpreter/script/run.ml
Original file line number Diff line number Diff line change
Expand Up @@ -446,6 +446,13 @@ let run_assertion ass =
| _ -> Assert.error ass.at "expected exception"
)

| AssertSuspension (act, re) ->
trace ("Asserting suspension...");
(match run_action act with
| exception Eval.Suspension (_, msg) -> assert_message ass.at "runtime" msg re
| _ -> Assert.error ass.at "expected suspension"
)

| AssertExhaustion (act, re) ->
trace ("Asserting exhaustion...");
(match run_action act with
Expand Down
Loading

0 comments on commit 6b0b593

Please sign in to comment.