Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.

Initial support for exceptions in spec interpreter #28

Closed
wants to merge 3 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions interpreter/spec/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,10 @@ and instr' =
| Unary of unop (* unary numeric operator *)
| Binary of binop (* binary numeric operator *)
| Convert of cvtop (* conversion *)
| Throw of var (* throw exception *)
| Try of stack_type * instr list * catch list * catch_all option (* try ... catch ... catch_all block *)
and catch = (var * instr list) Source.phrase
and catch_all = instr list Source.phrase


(* Globals & Functions *)
Expand Down Expand Up @@ -175,6 +179,12 @@ and import' =
idesc : import_desc;
}

type exception_ = exception_' Source.phrase
and exception_' =
{
etype : func_type;
}

type module_ = module_' Source.phrase
and module_' =
{
Expand All @@ -188,6 +198,7 @@ and module_' =
data : string segment list;
imports : import list;
exports : export list;
exceptions : exception_ list;
}


Expand All @@ -205,6 +216,7 @@ let empty_module =
data = [];
imports = [];
exports = [];
exceptions = [];
}

open Source
Expand Down
67 changes: 59 additions & 8 deletions interpreter/spec/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,17 @@ let region s left right =
let error s pos msg = raise (Code (region s pos pos, msg))
let require b s pos msg = if not b then error s pos msg

let current_scope = ref "binary"
let with_scope scope f =
let old_scope = !current_scope in
current_scope := scope;
try let result = f () in
current_scope := old_scope;
result
with e -> current_scope := old_scope; raise e

let guard f s =
try f s with EOS -> error s (len s) "unexpected end of binary or function"
try f s with EOS -> error s (len s) ("unexpected end of " ^ !current_scope)

let get = guard get
let get_string n = guard (get_string n)
Expand Down Expand Up @@ -196,6 +205,7 @@ let memop s =
Int32.to_int align, offset

let rec instr s =
with_scope "instr" (fun () ->
let pos = pos s in
match op s with
| 0x00 -> unreachable
Expand Down Expand Up @@ -223,9 +233,18 @@ let rec instr s =
end_ s;
if_ ts es1 []
end
| 0x06 ->
let ts = stack_type s in
let es = instr_block s in
let cs = catches s in
end_ s;
try_ ts es cs

| 0x08 ->
throw_ (at var s)

| 0x05 -> error s pos "misplaced ELSE opcode"
| 0x06| 0x07 | 0x08 | 0x09 | 0x0a as b -> illegal s pos b
| 0x07 | 0x09 | 0x0a as b -> illegal s pos b
| 0x0b -> error s pos "misplaced END opcode"

| 0x0c -> br (at var s)
Expand Down Expand Up @@ -427,17 +446,36 @@ let rec instr s =
| 0xbe -> f32_reinterpret_i32
| 0xbf -> f64_reinterpret_i64

| b -> illegal s pos b
| b -> illegal s pos b)

and instr_block s = List.rev (instr_block' s [])
and instr_block s =
with_scope "block" (fun () ->
let es = instr_block' s [] in
List.rev es)
and instr_block' s es =
match peek s with
| None | Some (0x05 | 0x0b) -> es
| None | Some (0x05 | 0x07 | 0x0b) -> es
| _ ->
let pos = pos s in
let e' = instr s in
instr_block' s (Source.(e' @@ region s pos pos) :: es)

(* TODO(eholk): For now catches only can handle a single catch_all *)
and catches s =
match (List.rev (catches' s [])) with
| c :: _ -> c
| _ -> error s (len s) "too many catches"
and catches' s cs =
match peek s with
| None | Some (0x0b) -> cs
| Some (0x05) ->
expect 0x05 s "CATCH or CATCH_ALL opcode expected";
let c = (at (fun s -> instr_block s) s) in
c :: catches' s cs
| Some (0x07) ->
error s (len s) "catch is not yet implemented"
| Some (b) -> illegal s (len s) b

let const s =
let c = at instr_block s in
end_ s;
Expand All @@ -462,6 +500,7 @@ let id s =
| 9 -> `ElemSection
| 10 -> `CodeSection
| 11 -> `DataSection
| 13 -> `ExceptionSection
| _ -> error s (pos s) "invalid section id"
) bo

Expand All @@ -480,6 +519,15 @@ let type_section s =
section `TypeSection (vec func_type) [] s


(* Exception Section *)

let exception_ s =
{ etype = func_type s }

let exception_section s =
section `ExceptionSection (vec (at exception_)) [] s


(* Import section *)

let import_desc s =
Expand Down Expand Up @@ -570,10 +618,11 @@ let local s =
Lib.List.make n t

let code _ s =
with_scope "function" (fun () ->
let locals = List.flatten (vec local s) in
let body = instr_block s in
end_ s;
{locals; body; ftype = Source.((-1l) @@ Source.no_region)}
{locals; body; ftype = Source.((-1l) @@ Source.no_region)})

let code_section s =
section `CodeSection (vec (at (sized code))) [] s
Expand Down Expand Up @@ -639,6 +688,8 @@ let module_ s =
iterate custom_section s;
let exports = export_section s in
iterate custom_section s;
let exceptions = exception_section s in
iterate custom_section s;
let start = start_section s in
iterate custom_section s;
let elems = elem_section s in
Expand All @@ -652,8 +703,8 @@ let module_ s =
s (len s) "function and code section have inconsistent lengths";
let funcs =
List.map2 Source.(fun t f -> {f.it with ftype = t} @@ f.at)
func_types func_bodies
in {types; tables; memories; globals; funcs; imports; exports; elems; data; start}
func_types func_bodies in
{types; tables; memories; globals; funcs; imports; exports; elems; data; start; exceptions}


let decode name bs = at module_ (stream name bs)
15 changes: 15 additions & 0 deletions interpreter/spec/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -362,6 +362,14 @@ let encode m =
| Convert (F64 F64Op.DemoteF64) -> assert false
| Convert (F64 F64Op.ReinterpretInt) -> op 0xbf

| Throw x -> op 0x08; var x
| Try (ts, es, cs, ca) ->
op 0x06; stack_type ts; list instr es;
(match ca with
| Some es -> op 0x05; list instr es.it
| None -> ());
end_ ()

let const c =
list instr c.it; end_ ()

Expand All @@ -380,6 +388,12 @@ let encode m =
let type_section ts =
section 1 (vec func_type) ts (ts <> [])

(* Exception Section *)
let exception_ x =
func_type x.it.etype
let exception_section xs =
section 13 (vec exception_) xs (xs <> [])

(* Import section *)
let import_desc d =
match d.it with
Expand Down Expand Up @@ -497,6 +511,7 @@ let encode m =
export_section m.it.exports;
start_section m.it.start;
elem_section m.it.elems;
exception_section m.it.exceptions;
code_section m.it.funcs;
data_section m.it.data
end
Expand Down
53 changes: 43 additions & 10 deletions interpreter/spec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -39,15 +39,33 @@ let numeric_error at = function

type 'a stack = 'a list

type etag = int32
type handlers = (etag * instr list) list * instr list option

let empty_handlers : handlers = [], None

let rec handler_for handlers x =
match handlers with
| [], Some catch_all -> Some (catch_all, 0)
| [], None -> None
| (y, es) :: _, _ when y = x -> Some (es, 0)
| _ :: handlers, catch_all -> handler_for (handlers, catch_all) x

let handlers_from catches catch_all =
[], match catch_all with
| Some {it = instrs; _} -> Some instrs
| None -> None

type admin_instr = admin_instr' phrase
and admin_instr' =
| Plain of instr'
| Trapped of string
| Break of int32 * value stack
| Label of stack_type * instr list * value stack * admin_instr list
| Label of stack_type * instr list * value stack * admin_instr list * handlers
| Local of instance * value ref list * value stack * admin_instr list
| Invoke of closure

| Thrown of int32 * value stack

type config =
{
locals : value ref list;
Expand Down Expand Up @@ -121,10 +139,10 @@ let rec step (inst : instance) (c : config) : config =
vs, []

| Block (ts, es'), vs ->
vs, [Label (ts, [], [], List.map plain es') @@ e.at]
vs, [Label (ts, [], [], List.map plain es', empty_handlers) @@ e.at]

| Loop (ts, es'), vs ->
vs, [Label ([], [e' @@ e.at], [], List.map plain es') @@ e.at]
vs, [Label ([], [e' @@ e.at], [], List.map plain es', empty_handlers) @@ e.at]

| If (ts, es1, es2), I32 0l :: vs' ->
vs', [Plain (Block (ts, es2)) @@ e.at]
Expand Down Expand Up @@ -243,6 +261,12 @@ let rec step (inst : instance) (c : config) : config =
(try Eval_numeric.eval_cvtop cvtop v :: vs', []
with exn -> vs', [Trapped (numeric_error e.at exn) @@ e.at])

| Throw x, vs ->
[], [Thrown (x.it, vs) @@ e.at]

| Try (ts, es', catches, catch_all), vs ->
vs, [Label (ts, [], [], List.map plain es', handlers_from catches catch_all) @@ e.at]

| _ ->
let s1 = string_of_values (List.rev vs) in
let s2 = string_of_value_types (List.map type_of (List.rev vs)) in
Expand All @@ -256,22 +280,31 @@ let rec step (inst : instance) (c : config) : config =
| Break (k, vs'), vs ->
Crash.error e.at "undefined label"

| Label (ts, es0, vs', []), vs ->
| Label (ts, es0, vs', [], handlers), vs ->
vs' @ vs, []

| Label (ts, es0, vs', {it = Trapped msg; at} :: es'), vs ->
(* TODO(eholk): Should this case trigger catch_all? *)
| Label (ts, es0, vs', {it = Trapped msg; at} :: es', handlers), vs ->
vs, [Trapped msg @@ at]

| Label (ts, es0, vs', {it = Break (0l, vs0); at} :: es'), vs ->
| Label (ts, es0, vs', {it = Thrown (tag, exn_args); at} :: es', handlers), vs ->
(match handler_for handlers tag with
| Some (instrs, arg_count) -> take arg_count exn_args e.at @ vs, List.map plain instrs
| None -> vs, [Thrown (tag, exn_args) @@ at])

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

| Label (ts, es0, vs', {it = Break (k, vs0); at} :: es'), vs ->
| Label (ts, es0, vs', {it = Break (k, vs0); at} :: es', handlers), vs ->
vs, [Break (Int32.sub k 1l, vs0) @@ at]

| Label (ts, es0, values, instrs), vs ->
| Label (ts, es0, values, instrs, handlers), vs ->
let c' = step inst {c with values; instrs; depth = c.depth + 1} in
vs, [Label (ts, es0, c'.values, c'.instrs) @@ e.at]
vs, [Label (ts, es0, c'.values, c'.instrs, handlers) @@ e.at]

| Thrown _, vs ->
vs, [Trapped "webassembly exception" @@ e.at]

| Local (inst', locals, vs', []), vs ->
vs' @ vs, []

Expand Down
4 changes: 3 additions & 1 deletion interpreter/spec/operators.ml
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,9 @@ let br_table xs x = BrTable (xs, x)
let return = Return
let if_ ts es1 es2 = If (ts, es1, es2)
let select = Select

let throw_ x = Throw x
let try_ tts tes ces = Try (tts, tes, [], Some ces)

let call x = Call x
let call_indirect x = CallIndirect x

Expand Down
20 changes: 18 additions & 2 deletions interpreter/spec/valid.ml
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,12 @@ type context =
locals : value_type list;
results : value_type list;
labels : stack_type list;
exceptions : func_type list;
}

let context m =
{ module_ = m; types = []; funcs = []; tables = []; memories = [];
globals = []; locals = []; results = []; labels = [] }
globals = []; locals = []; results = []; labels = []; exceptions = [] }

let lookup category list x =
try Lib.List32.nth list x.it with Failure _ ->
Expand All @@ -42,6 +43,7 @@ let global (c : context) x = lookup "global" c.globals x
let label (c : context) x = lookup "label" c.labels x
let table (c : context) x = lookup "table" c.tables x
let memory (c : context) x = lookup "memory" c.memories x
let exception_ (c : context) x = lookup "exception" c.exceptions x


(* Stack typing *)
Expand Down Expand Up @@ -286,6 +288,19 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
let t1, t2 = type_cvtop e.at cvtop in
[t1] --> [t2]

| Throw x ->
let FuncType (ins, out) = exception_ c x in
ins -->... []

| Try (ts, tes, _, ces) ->
check_arity (List.length ts) e.at;
check_block {c with labels = ts :: c.labels} tes ts e.at;
(* TODO(eholk): check catches *)
let _ = match ces with
| Some ces -> check_block {c with labels = ts :: c.labels} ces.it ts ces.at
| None -> ()
in [] --> ts

and check_seq (c : context) (es : instr list) : infer_stack_type =
match es with
| [] ->
Expand Down Expand Up @@ -428,14 +443,15 @@ let check_export (c : context) (set : NameSet.t) (ex : export) : NameSet.t =
let check_module (m : module_) =
let
{ types; imports; tables; memories; globals; funcs; start; elems; data;
exports } = m.it
exports; exceptions } = m.it
in
let c0 = List.fold_right check_import imports {(context m) with types} in
let c1 =
{ c0 with
funcs = c0.funcs @ List.map (fun f -> type_ c0 f.it.ftype) funcs;
tables = c0.tables @ List.map (fun tab -> tab.it.ttype) tables;
memories = c0.memories @ List.map (fun mem -> mem.it.mtype) memories;
exceptions = c0.exceptions @ List.map (fun exc -> exc.it.etype) exceptions;
}
in
let c =
Expand Down
Loading