From b4d490841320930963d4ce641440f98f8c8fbe02 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 23 May 2019 20:35:32 +0200 Subject: [PATCH 1/7] [interpreter] Implement anonymous exports --- interpreter/binary/decode.ml | 17 +++++++++++++++-- interpreter/binary/encode.ml | 21 ++++++++++++++++++--- interpreter/exec/eval.ml | 21 ++++++++++++--------- interpreter/script/js.ml | 8 ++++++-- interpreter/script/run.ml | 7 +++++-- interpreter/syntax/ast.ml | 2 +- interpreter/text/arrange.ml | 6 ++++-- interpreter/text/parser.mly | 9 +++++++-- interpreter/util/lib.ml | 1 + interpreter/util/lib.mli | 1 + interpreter/valid/valid.ml | 23 +++++++++++++++++++---- test/core/linking.wast | 6 ++++++ test/core/ref_func.wast | 11 +++++++++-- 13 files changed, 104 insertions(+), 29 deletions(-) diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index c9702621..e3871a90 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -512,6 +512,7 @@ let id s = | 10 -> `CodeSection | 11 -> `DataSection | 12 -> `DataCountSection + | 13 -> `AnonSection | _ -> error s (pos s) "invalid section id" ) bo @@ -600,7 +601,7 @@ let export_desc s = | _ -> error s (pos s - 1) "invalid export kind" let export s = - let name = name s in + let name = Some (name s) in let edesc = at export_desc s in {name; edesc} @@ -608,6 +609,16 @@ let export_section s = section `ExportSection (vec (at export)) [] s +(* Anonymous export section *) + +let anon s = + let edesc = at export_desc s in + {name = None; edesc} + +let anon_section s = + section `AnonSection (vec (at anon)) [] s + + (* Start section *) let start_section s = @@ -761,7 +772,9 @@ let module_ s = iterate custom_section s; let globals = global_section s in iterate custom_section s; - let exports = export_section s in + let exports' = export_section s in + iterate custom_section s; + let exports = exports' @ anon_section s in iterate custom_section s; let start = start_section s in iterate custom_section s; diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 690697c7..e630b85b 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -463,11 +463,25 @@ let encode m = | GlobalExport x -> u8 3; var x let export ex = - let {name = n; edesc} = ex.it in - name n; export_desc edesc + let {name = n_opt; edesc} = ex.it in + match n_opt with + | None -> assert false + | Some n -> name n; export_desc edesc let export_section exs = - section 7 (vec export) exs (exs <> []) + let exs' = List.filter (fun ex -> ex.it.name <> None) exs in + section 7 (vec export) exs' (exs' <> []) + + (* Anonymous export section *) + let anon ex = + let {name = n_opt; edesc} = ex.it in + match n_opt with + | None -> export_desc edesc + | Some _ -> assert false + + let anon_section exs = + let exs' = List.filter (fun ex -> ex.it.name = None) exs in + section 13 (vec anon) exs' (exs' <> []) (* Start section *) let start_section xo = @@ -565,6 +579,7 @@ let encode m = memory_section m.it.memories; global_section m.it.globals; export_section m.it.exports; + anon_section m.it.exports; start_section m.it.start; elem_section m.it.elems; data_count_section m.it.datas m; diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 7a9039fe..f941bdaa 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -533,15 +533,18 @@ let create_global (inst : module_inst) (glob : global) : global_inst = let v = eval_const inst ginit in Global.alloc gtype v -let create_export (inst : module_inst) (ex : export) : export_inst = +let create_export (inst : module_inst) (ex : export) : export_inst option = let {name; edesc} = ex.it in - let ext = - match edesc.it with - | FuncExport x -> ExternFunc (func inst x) - | TableExport x -> ExternTable (table inst x) - | MemoryExport x -> ExternMemory (memory inst x) - | GlobalExport x -> ExternGlobal (global inst x) - in name, ext + match name with + | None -> None + | Some n -> + let ext = + match edesc.it with + | FuncExport x -> ExternFunc (func inst x) + | TableExport x -> ExternTable (table inst x) + | MemoryExport x -> ExternMemory (memory inst x) + | GlobalExport x -> ExternGlobal (global inst x) + in Some (n, ext) let create_elem (inst : module_inst) (seg : elem_segment) : elem_inst = let {etype; einit; _} = seg.it in @@ -620,7 +623,7 @@ let init (m : module_) (exts : extern list) : module_inst = in let inst = { inst2 with - exports = List.map (create_export inst2) exports; + exports = Lib.List.map_filter (create_export inst2) exports; elems = List.map (create_elem inst2) elems; datas = List.map (create_data inst2) datas; } diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml index 461c94df..e78800b9 100644 --- a/interpreter/script/js.ml +++ b/interpreter/script/js.ml @@ -186,7 +186,11 @@ type modules = {mutable env : exports Map.t; mutable current : int} let exports m : exports = List.fold_left - (fun map exp -> NameMap.add exp.it.name (export_type m exp) map) + (fun map exp -> + match exp.it.name with + | None -> map + | Some n -> NameMap.add n (export_type m exp) map + ) NameMap.empty m.it.exports let modules () : modules = {env = Map.empty; current = 0} @@ -345,7 +349,7 @@ let wrap item_name wrap_action wrap_assertion at = ) 0l imports @@ at in let edesc = FuncExport item @@ at in - let exports = [{name = Utf8.decode "run"; edesc} @@ at] in + let exports = [{name = Some (Utf8.decode "run"); edesc} @@ at] in let body = [ Block ([], action @ assertion @ [Return @@ at]) @@ at; Unreachable @@ at ] diff --git a/interpreter/script/run.ml b/interpreter/script/run.ml index 11764e43..5613d8ec 100644 --- a/interpreter/script/run.ml +++ b/interpreter/script/run.ml @@ -230,8 +230,11 @@ let print_export m ex = | ExternMemoryType t -> "memory", string_of_memory_type t | ExternGlobalType t -> "global", string_of_global_type t in - Printf.printf " export %s \"%s\" : %s\n" - category (Ast.string_of_name ex.it.Ast.name) annotation + match ex.it.Ast.name with + | None -> () + | Some n -> + Printf.printf " export %s \"%s\" : %s\n" + category (Ast.string_of_name n) annotation let print_module x_opt m = Printf.printf "module%s :\n" diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml index 5926bffd..5ed0ca24 100644 --- a/interpreter/syntax/ast.ml +++ b/interpreter/syntax/ast.ml @@ -182,7 +182,7 @@ and export_desc' = type export = export' Source.phrase and export' = { - name : name; + name : name option; edesc : export_desc; } diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 72420679..ac2580d1 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -380,8 +380,10 @@ let export_desc d = | GlobalExport x -> Node ("global", [atom var x]) let export ex = - let {name = n; edesc} = ex.it in - Node ("export", [atom name n; export_desc edesc]) + let {name = n_opt; edesc} = ex.it in + match n_opt with + | None -> Node ("export", [export_desc edesc]) + | Some n -> Node ("export", [atom name n; export_desc edesc]) let global off i g = let {gtype; ginit} = g.it in diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 2f36c3f5..0bbfb1ba 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -824,13 +824,18 @@ export_desc : | LPAR GLOBAL var RPAR { fun c -> GlobalExport ($3 c global) } export : + | LPAR EXPORT export_desc RPAR + { let at = at () and at3 = ati 3 in + fun c -> {name = None; edesc = $3 c @@ at3} @@ at } | LPAR EXPORT name export_desc RPAR { let at = at () and at4 = ati 4 in - fun c -> {name = $3; edesc = $4 c @@ at4} @@ at } + fun c -> {name = Some $3; edesc = $4 c @@ at4} @@ at } inline_export : + | LPAR EXPORT RPAR + { let at = at () in fun d c -> {name = None; edesc = d @@ at} @@ at } | LPAR EXPORT name RPAR - { let at = at () in fun d c -> {name = $3; edesc = d @@ at} @@ at } + { let at = at () in fun d c -> {name = Some $3; edesc = d @@ at} @@ at } /* Modules */ diff --git a/interpreter/util/lib.ml b/interpreter/util/lib.ml index 675890cb..c4e0c361 100644 --- a/interpreter/util/lib.ml +++ b/interpreter/util/lib.ml @@ -1,5 +1,6 @@ module Fun = struct + let id x = x let curry f x y = f (x, y) let uncurry f (x, y) = f x y diff --git a/interpreter/util/lib.mli b/interpreter/util/lib.mli index a44253e5..1cadd9c9 100644 --- a/interpreter/util/lib.mli +++ b/interpreter/util/lib.mli @@ -2,6 +2,7 @@ module Fun : sig + val id : 'a -> 'a val curry : ('a * 'b -> 'c) -> ('a -> 'b -> 'c) val uncurry : ('a -> 'b -> 'c) -> ('a * 'b -> 'c) diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 9edbc1e1..93564718 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -26,12 +26,13 @@ type context = locals : value_type list; results : value_type list; labels : stack_type list; + exports : export_desc' list; } let empty_context = { types = []; funcs = []; tables = []; memories = []; globals = []; datas = []; elems = []; - locals = []; results = []; labels = [] } + locals = []; results = []; labels = []; exports = [] } let lookup category list x = try Lib.List32.nth list x.it with Failure _ -> @@ -47,6 +48,13 @@ let elem (c : context) x = lookup "elem segment" c.elems x let local (c : context) x = lookup "local" c.locals x let label (c : context) x = lookup "label" c.labels x +let export category (c : context) f x = + if not (List.mem x.it (Lib.List.map_filter f c.exports)) then + error x.at ("unexported " ^ category ^ " " ^ Int32.to_string x.it) + +let export_func (c : context) x = + export "function" c (function (FuncExport x) -> Some x.it | _ -> None) x + (* Stack typing *) @@ -334,6 +342,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type = | RefFunc x -> let _ft = func c x in + export_func c x; [] --> [RefType FuncRefType] | Const v -> @@ -535,8 +544,11 @@ let check_export (c : context) (set : NameSet.t) (ex : export) : NameSet.t = | MemoryExport x -> ignore (memory c x) | GlobalExport x -> ignore (global c x) ); - require (not (NameSet.mem name set)) ex.at "duplicate export name"; - NameSet.add name set + match name with + | None -> set + | Some n -> + require (not (NameSet.mem n set)) ex.at "duplicate export name"; + NameSet.add n set let check_module (m : module_) = let @@ -545,7 +557,10 @@ let check_module (m : module_) = in let c0 = List.fold_right check_import imports - {empty_context with types = List.map (fun ty -> ty.it) types} + { empty_context with + exports = List.map (fun ex -> ex.it.edesc.it) exports; + types = List.map (fun ty -> ty.it) types; + } in let c1 = { c0 with diff --git a/test/core/linking.wast b/test/core/linking.wast index bf6356fb..59b0a19d 100644 --- a/test/core/linking.wast +++ b/test/core/linking.wast @@ -129,6 +129,12 @@ "incompatible import type" ) + +(module $Mglobal-ex + (func $f (export)) + (global (export "g") anyref (ref.func $f)) +) + (assert_unlinkable (module (global (import "Mref_ex" "g-var-null") (mut funcref))) "incompatible import type" diff --git a/test/core/ref_func.wast b/test/core/ref_func.wast index 393d3f82..efde8c9e 100644 --- a/test/core/ref_func.wast +++ b/test/core/ref_func.wast @@ -4,8 +4,10 @@ (register "M") (module - (func $f (import "M" "f") (param i32) (result i32)) - (func $g (param $x i32) (result i32) (i32.add (local.get $x) (i32.const 1))) + (func $f (export) (import "M" "f") (param i32) (result i32)) + (func $g (export "") (param $x i32) (result i32) + (i32.add (local.get $x) (i32.const 1)) + ) (global anyref (ref.func $f)) (global anyref (ref.func $g)) @@ -62,3 +64,8 @@ ) "unknown function 7" ) + +(assert_invalid + (module (func $f (drop (ref.func $f)))) + "unexported function" +) From cb8c034aa203eb70d38b4cfe03df0fa903525c2d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 30 May 2019 08:43:22 +0200 Subject: [PATCH 2/7] [interpreter] Implement refer section --- interpreter/binary/decode.ml | 20 +++---- interpreter/binary/encode.ml | 24 ++++----- interpreter/exec/eval.ml | 23 ++++---- interpreter/script/js.ml | 8 +-- interpreter/script/run.ml | 7 +-- interpreter/syntax/ast.ml | 10 +++- interpreter/text/arrange.ml | 11 ++-- interpreter/text/lexer.mll | 1 + interpreter/text/parser.mly | 100 +++++++++++++++++++++-------------- interpreter/valid/valid.ml | 28 +++++----- test/core/linking.wast | 2 +- test/core/ref_func.wast | 6 +-- test/core/table_grow.wast | 4 +- 13 files changed, 130 insertions(+), 114 deletions(-) diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index e3871a90..b9cd4cde 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -512,7 +512,7 @@ let id s = | 10 -> `CodeSection | 11 -> `DataSection | 12 -> `DataCountSection - | 13 -> `AnonSection + | 13 -> `ReferSection | _ -> error s (pos s) "invalid section id" ) bo @@ -601,7 +601,7 @@ let export_desc s = | _ -> error s (pos s - 1) "invalid export kind" let export s = - let name = Some (name s) in + let name = name s in let edesc = at export_desc s in {name; edesc} @@ -611,12 +611,12 @@ let export_section s = (* Anonymous export section *) -let anon s = - let edesc = at export_desc s in - {name = None; edesc} +let refer s = + let rdesc = at export_desc s in + {rdesc} -let anon_section s = - section `AnonSection (vec (at anon)) [] s +let refer_section s = + section `ReferSection (vec (at refer)) [] s (* Start section *) @@ -772,9 +772,9 @@ let module_ s = iterate custom_section s; let globals = global_section s in iterate custom_section s; - let exports' = export_section s in + let exports = export_section s in iterate custom_section s; - let exports = exports' @ anon_section s in + let refers = refer_section s in iterate custom_section s; let start = start_section s in iterate custom_section s; @@ -797,7 +797,7 @@ let module_ s = 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; datas; start} + in {types; tables; memories; globals; funcs; imports; exports; refers; elems; datas; start} let decode name bs = at module_ (stream name bs) diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index e630b85b..09a0037d 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -463,25 +463,19 @@ let encode m = | GlobalExport x -> u8 3; var x let export ex = - let {name = n_opt; edesc} = ex.it in - match n_opt with - | None -> assert false - | Some n -> name n; export_desc edesc + let {name = n; edesc} = ex.it in + name n; export_desc edesc let export_section exs = - let exs' = List.filter (fun ex -> ex.it.name <> None) exs in - section 7 (vec export) exs' (exs' <> []) + section 7 (vec export) exs (exs <> []) (* Anonymous export section *) - let anon ex = - let {name = n_opt; edesc} = ex.it in - match n_opt with - | None -> export_desc edesc - | Some _ -> assert false + let refer ref = + let {rdesc} = ref.it in + export_desc rdesc - let anon_section exs = - let exs' = List.filter (fun ex -> ex.it.name = None) exs in - section 13 (vec anon) exs' (exs' <> []) + let refer_section refs = + section 13 (vec refer) refs (refs <> []) (* Start section *) let start_section xo = @@ -579,7 +573,7 @@ let encode m = memory_section m.it.memories; global_section m.it.globals; export_section m.it.exports; - anon_section m.it.exports; + refer_section m.it.refers; start_section m.it.start; elem_section m.it.elems; data_count_section m.it.datas m; diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index f941bdaa..720725b4 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -533,18 +533,15 @@ let create_global (inst : module_inst) (glob : global) : global_inst = let v = eval_const inst ginit in Global.alloc gtype v -let create_export (inst : module_inst) (ex : export) : export_inst option = +let create_export (inst : module_inst) (ex : export) : export_inst = let {name; edesc} = ex.it in - match name with - | None -> None - | Some n -> - let ext = - match edesc.it with - | FuncExport x -> ExternFunc (func inst x) - | TableExport x -> ExternTable (table inst x) - | MemoryExport x -> ExternMemory (memory inst x) - | GlobalExport x -> ExternGlobal (global inst x) - in Some (n, ext) + let ext = + match edesc.it with + | FuncExport x -> ExternFunc (func inst x) + | TableExport x -> ExternTable (table inst x) + | MemoryExport x -> ExternMemory (memory inst x) + | GlobalExport x -> ExternGlobal (global inst x) + in (name, ext) let create_elem (inst : module_inst) (seg : elem_segment) : elem_inst = let {etype; einit; _} = seg.it in @@ -603,7 +600,7 @@ let run_start start = let init (m : module_) (exts : extern list) : module_inst = let { imports; tables; memories; globals; funcs; types; - exports; elems; datas; start + exports; refers; elems; datas; start } = m.it in if List.length exts <> List.length imports then @@ -623,7 +620,7 @@ let init (m : module_) (exts : extern list) : module_inst = in let inst = { inst2 with - exports = Lib.List.map_filter (create_export inst2) exports; + exports = List.map (create_export inst2) exports; elems = List.map (create_elem inst2) elems; datas = List.map (create_data inst2) datas; } diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml index e78800b9..461c94df 100644 --- a/interpreter/script/js.ml +++ b/interpreter/script/js.ml @@ -186,11 +186,7 @@ type modules = {mutable env : exports Map.t; mutable current : int} let exports m : exports = List.fold_left - (fun map exp -> - match exp.it.name with - | None -> map - | Some n -> NameMap.add n (export_type m exp) map - ) + (fun map exp -> NameMap.add exp.it.name (export_type m exp) map) NameMap.empty m.it.exports let modules () : modules = {env = Map.empty; current = 0} @@ -349,7 +345,7 @@ let wrap item_name wrap_action wrap_assertion at = ) 0l imports @@ at in let edesc = FuncExport item @@ at in - let exports = [{name = Some (Utf8.decode "run"); edesc} @@ at] in + let exports = [{name = Utf8.decode "run"; edesc} @@ at] in let body = [ Block ([], action @ assertion @ [Return @@ at]) @@ at; Unreachable @@ at ] diff --git a/interpreter/script/run.ml b/interpreter/script/run.ml index 5613d8ec..11764e43 100644 --- a/interpreter/script/run.ml +++ b/interpreter/script/run.ml @@ -230,11 +230,8 @@ let print_export m ex = | ExternMemoryType t -> "memory", string_of_memory_type t | ExternGlobalType t -> "global", string_of_global_type t in - match ex.it.Ast.name with - | None -> () - | Some n -> - Printf.printf " export %s \"%s\" : %s\n" - category (Ast.string_of_name n) annotation + Printf.printf " export %s \"%s\" : %s\n" + category (Ast.string_of_name ex.it.Ast.name) annotation let print_module x_opt m = Printf.printf "module%s :\n" diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml index 5ed0ca24..435d68d2 100644 --- a/interpreter/syntax/ast.ml +++ b/interpreter/syntax/ast.ml @@ -182,10 +182,16 @@ and export_desc' = type export = export' Source.phrase and export' = { - name : name option; + name : name; edesc : export_desc; } +type refer = refer' Source.phrase +and refer' = +{ + rdesc : export_desc; +} + type import_desc = import_desc' Source.phrase and import_desc' = | FuncImport of var @@ -214,6 +220,7 @@ and module_' = datas : data_segment list; imports : import list; exports : export list; + refers : refer list; } @@ -231,6 +238,7 @@ let empty_module = datas = []; imports = []; exports = []; + refers = []; } open Source diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index ac2580d1..b2a5d427 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -380,10 +380,12 @@ let export_desc d = | GlobalExport x -> Node ("global", [atom var x]) let export ex = - let {name = n_opt; edesc} = ex.it in - match n_opt with - | None -> Node ("export", [export_desc edesc]) - | Some n -> Node ("export", [atom name n; export_desc edesc]) + let {name = n; edesc} = ex.it in + Node ("export", [atom name n; export_desc edesc]) + +let refer an = + let {rdesc} = an.it in + Node ("ref", [export_desc rdesc]) let global off i g = let {gtype; ginit} = g.it in @@ -410,6 +412,7 @@ let module_with_var_opt x_opt m = listi (global !gx) m.it.globals @ listi (func_with_index !fx) m.it.funcs @ list export m.it.exports @ + list refer m.it.refers @ opt start m.it.start @ list elem m.it.elems @ list data m.it.datas diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index 9511a8e3..8a95d903 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -160,6 +160,7 @@ rule token = parse | '"'character*'\\'_ { error_nest (Lexing.lexeme_end_p lexbuf) lexbuf "illegal escape" } + | "ref" { REF } | "anyref" { ANYREF } | "funcref" { FUNCREF } | "nullref" { NULLREF } diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 0bbfb1ba..68967adc 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -174,7 +174,7 @@ let inline_type_explicit (c : context) x ft at = %token MEMORY_SIZE MEMORY_GROW MEMORY_FILL MEMORY_COPY MEMORY_INIT DATA_DROP %token LOAD STORE OFFSET_EQ_NAT ALIGN_EQ_NAT %token CONST UNARY BINARY TEST COMPARE CONVERT -%token REF_ANY REF_NULL REF_FUNC REF_HOST REF_IS_NULL +%token REF REF_ANY REF_NULL REF_FUNC REF_HOST REF_IS_NULL %token FUNC START TYPE PARAM RESULT LOCAL GLOBAL %token TABLE ELEM MEMORY DATA OFFSET IMPORT EXPORT %token MODULE BIN QUOTE @@ -570,26 +570,29 @@ func_fields : | type_use func_fields_body { fun c x at -> let t = inline_type_explicit c ($1 c type_) (fst $2) at in - [{(snd $2 (enter_func c)) with ftype = t} @@ at], [], [] } + [{(snd $2 (enter_func c)) with ftype = t} @@ at], [], [], [] } | func_fields_body /* Sugar */ { fun c x at -> let t = inline_type c (fst $1) at in - [{(snd $1 (enter_func c)) with ftype = t} @@ at], [], [] } + [{(snd $1 (enter_func c)) with ftype = t} @@ at], [], [], [] } | inline_import type_use func_fields_import /* Sugar */ { fun c x at -> let t = inline_type_explicit c ($2 c type_) $3 at in [], [{ module_name = fst $1; item_name = snd $1; - idesc = FuncImport t @@ at } @@ at ], [] } + idesc = FuncImport t @@ at } @@ at ], [], [] } | inline_import func_fields_import /* Sugar */ { fun c x at -> let t = inline_type c $2 at in [], [{ module_name = fst $1; item_name = snd $1; - idesc = FuncImport t @@ at } @@ at ], [] } + idesc = FuncImport t @@ at } @@ at ], [], [] } | inline_export func_fields /* Sugar */ - { fun c x at -> - let fns, ims, exs = $2 c x at in fns, ims, $1 (FuncExport x) c :: exs } + { fun c x at -> let fns, ims, exs, refs = $2 c x at in + fns, ims, $1 (FuncExport x) c :: exs, refs } + | inline_refer func_fields /* Sugar */ + { fun c x at -> let fns, ims, exs, refs = $2 c x at in + fns, ims, exs, $1 (FuncExport x) c :: refs } func_fields_import : /* Sugar */ | func_fields_import_result { $1 } @@ -700,15 +703,18 @@ table : table_fields : | table_type - { fun c x at -> [{ttype = $1} @@ at], [], [], [] } + { fun c x at -> [{ttype = $1} @@ at], [], [], [], [] } | inline_import table_type /* Sugar */ { fun c x at -> [], [], [{ module_name = fst $1; item_name = snd $1; - idesc = TableImport $2 @@ at } @@ at], [] } + idesc = TableImport $2 @@ at } @@ at], [], [] } | inline_export table_fields /* Sugar */ - { fun c x at -> let tabs, elems, ims, exs = $2 c x at in - tabs, elems, ims, $1 (TableExport x) c :: exs } + { fun c x at -> let tabs, elems, ims, exs, refs = $2 c x at in + tabs, elems, ims, $1 (TableExport x) c :: exs, refs } + | inline_refer table_fields /* Sugar */ + { fun c x at -> let tabs, elems, ims, exs, refs = $2 c x at in + tabs, elems, ims, exs, $1 (TableExport x) c :: refs } | ref_type LPAR ELEM elem_var_list RPAR /* Sugar */ { fun c x at -> let offset = [i32_const (0l @@ at) @@ at] @@ at in @@ -717,7 +723,7 @@ table_fields : let emode = Active {index = x; offset} @@ at in [{ttype = TableType ({min = size; max = Some size}, $1)} @@ at], [{etype = FuncRefType; einit; emode} @@ at], - [], [] } + [], [], [] } | ref_type LPAR ELEM elem_expr elem_expr_list RPAR /* Sugar */ { fun c x at -> let offset = [i32_const (0l @@ at) @@ at] @@ at in @@ -726,7 +732,7 @@ table_fields : let emode = Active {index = x; offset} @@ at in [{ttype = TableType ({min = size; max = Some size}, $1)} @@ at], [{etype = FuncRefType; einit; emode} @@ at], - [], [] } + [], [], [] } data : | LPAR DATA bind_var_opt string_list RPAR @@ -752,22 +758,25 @@ memory : memory_fields : | memory_type - { fun c x at -> [{mtype = $1} @@ at], [], [], [] } + { fun c x at -> [{mtype = $1} @@ at], [], [], [], [] } | inline_import memory_type /* Sugar */ { fun c x at -> [], [], [{ module_name = fst $1; item_name = snd $1; - idesc = MemoryImport $2 @@ at } @@ at], [] } + idesc = MemoryImport $2 @@ at } @@ at], [], [] } | inline_export memory_fields /* Sugar */ - { fun c x at -> let mems, data, ims, exs = $2 c x at in - mems, data, ims, $1 (MemoryExport x) c :: exs } + { fun c x at -> let mems, data, ims, exs, refs = $2 c x at in + mems, data, ims, $1 (MemoryExport x) c :: exs, refs } + | inline_refer memory_fields /* Sugar */ + { fun c x at -> let mems, data, ims, exs, refs = $2 c x at in + mems, data, ims, exs, $1 (MemoryExport x) c :: refs } | LPAR DATA string_list RPAR /* Sugar */ { fun c x at -> let offset = [i32_const (0l @@ at) @@ at] @@ at in let size = Int32.(div (add (of_int (String.length $3)) 65535l) 65536l) in [{mtype = MemoryType {min = size; max = Some size}} @@ at], [{dinit = $3; dmode = Active {index = x; offset} @@ at} @@ at], - [], [] } + [], [], [] } global : | LPAR GLOBAL bind_var_opt global_fields RPAR @@ -777,15 +786,18 @@ global : global_fields : | global_type const_expr - { fun c x at -> [{gtype = $1; ginit = $2 c} @@ at], [], [] } + { fun c x at -> [{gtype = $1; ginit = $2 c} @@ at], [], [], [] } | inline_import global_type /* Sugar */ { fun c x at -> [], [{ module_name = fst $1; item_name = snd $1; - idesc = GlobalImport $2 @@ at } @@ at], [] } + idesc = GlobalImport $2 @@ at } @@ at], [], [] } | inline_export global_fields /* Sugar */ - { fun c x at -> let globs, ims, exs = $2 c x at in - globs, ims, $1 (GlobalExport x) c :: exs } + { fun c x at -> let globs, ims, exs, refs = $2 c x at in + globs, ims, $1 (GlobalExport x) c :: exs, refs } + | inline_refer global_fields /* Sugar */ + { fun c x at -> let globs, ims, exs, refs = $2 c x at in + globs, ims, exs, $1 (GlobalExport x) c :: refs } /* Imports & Exports */ @@ -824,18 +836,22 @@ export_desc : | LPAR GLOBAL var RPAR { fun c -> GlobalExport ($3 c global) } export : - | LPAR EXPORT export_desc RPAR - { let at = at () and at3 = ati 3 in - fun c -> {name = None; edesc = $3 c @@ at3} @@ at } | LPAR EXPORT name export_desc RPAR { let at = at () and at4 = ati 4 in - fun c -> {name = Some $3; edesc = $4 c @@ at4} @@ at } + fun c -> {name = $3; edesc = $4 c @@ at4} @@ at } inline_export : - | LPAR EXPORT RPAR - { let at = at () in fun d c -> {name = None; edesc = d @@ at} @@ at } | LPAR EXPORT name RPAR - { let at = at () in fun d c -> {name = Some $3; edesc = d @@ at} @@ at } + { let at = at () in fun d c -> {name = $3; edesc = d @@ at} @@ at } + +refer : + | LPAR REF export_desc RPAR + { let at = at () and at3 = ati 3 in + fun c -> {rdesc = $3 c @@ at3} @@ at } + +inline_refer : + | LPAR REF RPAR + { let at = at () in fun d c -> {rdesc = d @@ at} @@ at } /* Modules */ @@ -863,32 +879,34 @@ module_fields1 : { fun c -> ignore ($1 c); $2 c } | global module_fields { fun c -> let gf = $1 c in let mf = $2 c in - fun () -> let globs, ims, exs = gf () in let m = mf () in + fun () -> let globs, ims, exs, refs = gf () in let m = mf () in if globs <> [] && m.imports <> [] then error (List.hd m.imports).at "import after global definition"; - { m with globals = globs @ m.globals; - imports = ims @ m.imports; exports = exs @ m.exports } } + { m with globals = globs @ m.globals; imports = ims @ m.imports; + exports = exs @ m.exports; refers = refs @ m.refers } } | table module_fields { fun c -> let tf = $1 c in let mf = $2 c in - fun () -> let tabs, elems, ims, exs = tf () in let m = mf () in + fun () -> let tabs, elems, ims, exs, refs = tf () in let m = mf () in if tabs <> [] && m.imports <> [] then error (List.hd m.imports).at "import after table definition"; { m with tables = tabs @ m.tables; elems = elems @ m.elems; - imports = ims @ m.imports; exports = exs @ m.exports } } + imports = ims @ m.imports; exports = exs @ m.exports; + refers = refs @ m.refers } } | memory module_fields { fun c -> let mmf = $1 c in let mf = $2 c in - fun () -> let mems, data, ims, exs = mmf () in let m = mf () in + fun () -> let mems, data, ims, exs, refs = mmf () in let m = mf () in if mems <> [] && m.imports <> [] then error (List.hd m.imports).at "import after memory definition"; { m with memories = mems @ m.memories; datas = data @ m.datas; - imports = ims @ m.imports; exports = exs @ m.exports } } + imports = ims @ m.imports; exports = exs @ m.exports; + refers = refs @ m.refers } } | func module_fields { fun c -> let ff = $1 c in let mf = $2 c in - fun () -> let funcs, ims, exs = ff () in let m = mf () in + fun () -> let funcs, ims, exs, refs = ff () in let m = mf () in if funcs <> [] && m.imports <> [] then error (List.hd m.imports).at "import after function definition"; - { m with funcs = funcs @ m.funcs; - imports = ims @ m.imports; exports = exs @ m.exports } } + { m with funcs = funcs @ m.funcs; imports = ims @ m.imports; + exports = exs @ m.exports; refers = refs @ m.refers } } | elem module_fields { fun c -> let ef = $1 c in let mf = $2 c in fun () -> let elems = ef () in let m = mf () in @@ -911,6 +929,10 @@ module_fields1 : { fun c -> let mf = $2 c in fun () -> let m = mf () in {m with exports = $1 c :: m.exports} } + | refer module_fields + { fun c -> let mf = $2 c in + fun () -> let m = mf () in + {m with refers = $1 c :: m.refers} } module_var_opt : | /* empty */ { None } diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 93564718..c96ae222 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -26,13 +26,13 @@ type context = locals : value_type list; results : value_type list; labels : stack_type list; - exports : export_desc' list; + refers : export_desc' list; } let empty_context = { types = []; funcs = []; tables = []; memories = []; globals = []; datas = []; elems = []; - locals = []; results = []; labels = []; exports = [] } + locals = []; results = []; labels = []; refers = [] } let lookup category list x = try Lib.List32.nth list x.it with Failure _ -> @@ -48,12 +48,13 @@ let elem (c : context) x = lookup "elem segment" c.elems x let local (c : context) x = lookup "local" c.locals x let label (c : context) x = lookup "label" c.labels x -let export category (c : context) f x = - if not (List.mem x.it (Lib.List.map_filter f c.exports)) then - error x.at ("unexported " ^ category ^ " " ^ Int32.to_string x.it) +let refer category (c : context) f x = + if not (List.mem x.it (Lib.List.map_filter f c.refers)) then + error x.at + ("undeclared " ^ category ^ " reference " ^ Int32.to_string x.it) -let export_func (c : context) x = - export "function" c (function (FuncExport x) -> Some x.it | _ -> None) x +let refer_func (c : context) x = + refer "function" c (function (FuncExport x) -> Some x.it | _ -> None) x (* Stack typing *) @@ -342,7 +343,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type = | RefFunc x -> let _ft = func c x in - export_func c x; + refer_func c x; [] --> [RefType FuncRefType] | Const v -> @@ -544,21 +545,18 @@ let check_export (c : context) (set : NameSet.t) (ex : export) : NameSet.t = | MemoryExport x -> ignore (memory c x) | GlobalExport x -> ignore (global c x) ); - match name with - | None -> set - | Some n -> - require (not (NameSet.mem n set)) ex.at "duplicate export name"; - NameSet.add n set + require (not (NameSet.mem name set)) ex.at "duplicate export name"; + NameSet.add name set let check_module (m : module_) = let { types; imports; tables; memories; globals; funcs; start; elems; datas; - exports } = m.it + exports; refers } = m.it in let c0 = List.fold_right check_import imports { empty_context with - exports = List.map (fun ex -> ex.it.edesc.it) exports; + refers = List.map (fun ex -> ex.it.rdesc.it) refers; types = List.map (fun ty -> ty.it) types; } in diff --git a/test/core/linking.wast b/test/core/linking.wast index 59b0a19d..65999c72 100644 --- a/test/core/linking.wast +++ b/test/core/linking.wast @@ -131,7 +131,7 @@ (module $Mglobal-ex - (func $f (export)) + (func $f (ref)) (global (export "g") anyref (ref.func $f)) ) diff --git a/test/core/ref_func.wast b/test/core/ref_func.wast index efde8c9e..e9b84b1b 100644 --- a/test/core/ref_func.wast +++ b/test/core/ref_func.wast @@ -4,8 +4,8 @@ (register "M") (module - (func $f (export) (import "M" "f") (param i32) (result i32)) - (func $g (export "") (param $x i32) (result i32) + (func $f (ref) (import "M" "f") (param i32) (result i32)) + (func $g (ref) (param $x i32) (result i32) (i32.add (local.get $x) (i32.const 1)) ) @@ -67,5 +67,5 @@ (assert_invalid (module (func $f (drop (ref.func $f)))) - "unexported function" + "undeclared function reference" ) diff --git a/test/core/table_grow.wast b/test/core/table_grow.wast index 158df3ca..c0b14520 100644 --- a/test/core/table_grow.wast +++ b/test/core/table_grow.wast @@ -38,7 +38,7 @@ ;; Reject growing to size outside i32 value range (module (table $t 0x10 anyref) - (func $f (export "grow") (result i32) + (func $f (ref) (export "grow") (result i32) (table.grow $t (ref.func $f) (i32.const 0xffff_fff0)) ) ) @@ -82,7 +82,7 @@ (func (export "grow") (param i32) (result i32) (table.grow $t (ref.null) (local.get 0)) ) - (func (export "check-table-null") (param i32 i32) (result anyref) + (func (ref) (export "check-table-null") (param i32 i32) (result anyref) (local anyref) (local.set 2 (ref.func 1)) (block From aea2230607f07f47711ef52991fe63f502e4a314 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 25 Sep 2019 12:12:54 +0200 Subject: [PATCH 3/7] [interpreter] Implement declaration segments --- interpreter/binary/decode.ml | 15 +----- interpreter/binary/encode.ml | 9 ---- interpreter/exec/eval.ml | 2 +- interpreter/syntax/ast.ml | 8 ---- interpreter/syntax/free.ml | 10 ++-- interpreter/syntax/free.mli | 2 + interpreter/text/arrange.ml | 5 -- interpreter/text/lexer.mll | 1 - interpreter/text/parser.mly | 91 +++++++++++++----------------------- interpreter/valid/valid.ml | 17 +++---- test/core/linking.wast | 3 +- test/core/ref_func.wast | 5 +- test/core/table_grow.wast | 6 ++- 13 files changed, 59 insertions(+), 115 deletions(-) diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index b9cd4cde..c9702621 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -512,7 +512,6 @@ let id s = | 10 -> `CodeSection | 11 -> `DataSection | 12 -> `DataCountSection - | 13 -> `ReferSection | _ -> error s (pos s) "invalid section id" ) bo @@ -609,16 +608,6 @@ let export_section s = section `ExportSection (vec (at export)) [] s -(* Anonymous export section *) - -let refer s = - let rdesc = at export_desc s in - {rdesc} - -let refer_section s = - section `ReferSection (vec (at refer)) [] s - - (* Start section *) let start_section s = @@ -774,8 +763,6 @@ let module_ s = iterate custom_section s; let exports = export_section s in iterate custom_section s; - let refers = refer_section s in - iterate custom_section s; let start = start_section s in iterate custom_section s; let elems = elem_section s in @@ -797,7 +784,7 @@ let module_ s = 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; refers; elems; datas; start} + in {types; tables; memories; globals; funcs; imports; exports; elems; datas; start} let decode name bs = at module_ (stream name bs) diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 09a0037d..690697c7 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -469,14 +469,6 @@ let encode m = let export_section exs = section 7 (vec export) exs (exs <> []) - (* Anonymous export section *) - let refer ref = - let {rdesc} = ref.it in - export_desc rdesc - - let refer_section refs = - section 13 (vec refer) refs (refs <> []) - (* Start section *) let start_section xo = section 8 (opt var) xo (xo <> None) @@ -573,7 +565,6 @@ let encode m = memory_section m.it.memories; global_section m.it.globals; export_section m.it.exports; - refer_section m.it.refers; start_section m.it.start; elem_section m.it.elems; data_count_section m.it.datas m; diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 720725b4..99d17836 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -600,7 +600,7 @@ let run_start start = let init (m : module_) (exts : extern list) : module_inst = let { imports; tables; memories; globals; funcs; types; - exports; refers; elems; datas; start + exports; elems; datas; start } = m.it in if List.length exts <> List.length imports then diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml index 435d68d2..5926bffd 100644 --- a/interpreter/syntax/ast.ml +++ b/interpreter/syntax/ast.ml @@ -186,12 +186,6 @@ and export' = edesc : export_desc; } -type refer = refer' Source.phrase -and refer' = -{ - rdesc : export_desc; -} - type import_desc = import_desc' Source.phrase and import_desc' = | FuncImport of var @@ -220,7 +214,6 @@ and module_' = datas : data_segment list; imports : import list; exports : export list; - refers : refer list; } @@ -238,7 +231,6 @@ let empty_module = datas = []; imports = []; exports = []; - refers = []; } open Source diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml index 39e1474c..5f612f07 100644 --- a/interpreter/syntax/free.ml +++ b/interpreter/syntax/free.ml @@ -62,9 +62,9 @@ let list free xs = List.fold_left union empty (List.map free xs) let rec instr (e : instr) = match e.it with | Unreachable | Nop | Drop | Select _ -> empty - | Const _ | Test _ | Compare _ | Unary _ | Binary _ | Convert _ -> empty | RefNull | RefIsNull -> empty | RefFunc x -> funcs (var x) + | Const _ | Test _ | Compare _ | Unary _ | Binary _ | Convert _ -> empty | Block (_, es) | Loop (_, es) -> block es | If (_, es1, es2) -> block es1 ++ block es2 | Br x | BrIf x -> labels (var x) @@ -74,15 +74,15 @@ let rec instr (e : instr) = | CallIndirect (x, y) -> tables (var x) ++ types (var y) | LocalGet x | LocalSet x | LocalTee x -> locals (var x) | GlobalGet x | GlobalSet x -> globals (var x) - | Load _ | Store _ | MemorySize | MemoryGrow | MemoryCopy | MemoryFill -> - memories zero - | MemoryInit x -> memories zero ++ datas (var x) | TableGet x | TableSet x | TableSize x | TableGrow x | TableFill x -> tables (var x) | TableCopy (x, y) -> tables (var x) ++ tables (var y) | TableInit (x, y) -> tables (var x) ++ elems (var y) - | DataDrop x -> datas (var x) | ElemDrop x -> elems (var x) + | Load _ | Store _ | MemorySize | MemoryGrow | MemoryCopy | MemoryFill -> + memories zero + | MemoryInit x -> memories zero ++ datas (var x) + | DataDrop x -> datas (var x) and block (es : instr list) = let free = list instr es in {free with labels = shift free.labels} diff --git a/interpreter/syntax/free.mli b/interpreter/syntax/free.mli index 288a27b6..dc01edc0 100644 --- a/interpreter/syntax/free.mli +++ b/interpreter/syntax/free.mli @@ -32,3 +32,5 @@ val import : Ast.import -> t val start : Ast.var option -> t val module_ : Ast.module_ -> t + +val list : ('a -> t) -> 'a list -> t diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index b2a5d427..72420679 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -383,10 +383,6 @@ let export ex = let {name = n; edesc} = ex.it in Node ("export", [atom name n; export_desc edesc]) -let refer an = - let {rdesc} = an.it in - Node ("ref", [export_desc rdesc]) - let global off i g = let {gtype; ginit} = g.it in Node ("global $" ^ nat (off + i), global_type gtype :: list instr ginit.it) @@ -412,7 +408,6 @@ let module_with_var_opt x_opt m = listi (global !gx) m.it.globals @ listi (func_with_index !fx) m.it.funcs @ list export m.it.exports @ - list refer m.it.refers @ opt start m.it.start @ list elem m.it.elems @ list data m.it.datas diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index 8a95d903..9511a8e3 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -160,7 +160,6 @@ rule token = parse | '"'character*'\\'_ { error_nest (Lexing.lexeme_end_p lexbuf) lexbuf "illegal escape" } - | "ref" { REF } | "anyref" { ANYREF } | "funcref" { FUNCREF } | "nullref" { NULLREF } diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 68967adc..2f36c3f5 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -174,7 +174,7 @@ let inline_type_explicit (c : context) x ft at = %token MEMORY_SIZE MEMORY_GROW MEMORY_FILL MEMORY_COPY MEMORY_INIT DATA_DROP %token LOAD STORE OFFSET_EQ_NAT ALIGN_EQ_NAT %token CONST UNARY BINARY TEST COMPARE CONVERT -%token REF REF_ANY REF_NULL REF_FUNC REF_HOST REF_IS_NULL +%token REF_ANY REF_NULL REF_FUNC REF_HOST REF_IS_NULL %token FUNC START TYPE PARAM RESULT LOCAL GLOBAL %token TABLE ELEM MEMORY DATA OFFSET IMPORT EXPORT %token MODULE BIN QUOTE @@ -570,29 +570,26 @@ func_fields : | type_use func_fields_body { fun c x at -> let t = inline_type_explicit c ($1 c type_) (fst $2) at in - [{(snd $2 (enter_func c)) with ftype = t} @@ at], [], [], [] } + [{(snd $2 (enter_func c)) with ftype = t} @@ at], [], [] } | func_fields_body /* Sugar */ { fun c x at -> let t = inline_type c (fst $1) at in - [{(snd $1 (enter_func c)) with ftype = t} @@ at], [], [], [] } + [{(snd $1 (enter_func c)) with ftype = t} @@ at], [], [] } | inline_import type_use func_fields_import /* Sugar */ { fun c x at -> let t = inline_type_explicit c ($2 c type_) $3 at in [], [{ module_name = fst $1; item_name = snd $1; - idesc = FuncImport t @@ at } @@ at ], [], [] } + idesc = FuncImport t @@ at } @@ at ], [] } | inline_import func_fields_import /* Sugar */ { fun c x at -> let t = inline_type c $2 at in [], [{ module_name = fst $1; item_name = snd $1; - idesc = FuncImport t @@ at } @@ at ], [], [] } + idesc = FuncImport t @@ at } @@ at ], [] } | inline_export func_fields /* Sugar */ - { fun c x at -> let fns, ims, exs, refs = $2 c x at in - fns, ims, $1 (FuncExport x) c :: exs, refs } - | inline_refer func_fields /* Sugar */ - { fun c x at -> let fns, ims, exs, refs = $2 c x at in - fns, ims, exs, $1 (FuncExport x) c :: refs } + { fun c x at -> + let fns, ims, exs = $2 c x at in fns, ims, $1 (FuncExport x) c :: exs } func_fields_import : /* Sugar */ | func_fields_import_result { $1 } @@ -703,18 +700,15 @@ table : table_fields : | table_type - { fun c x at -> [{ttype = $1} @@ at], [], [], [], [] } + { fun c x at -> [{ttype = $1} @@ at], [], [], [] } | inline_import table_type /* Sugar */ { fun c x at -> [], [], [{ module_name = fst $1; item_name = snd $1; - idesc = TableImport $2 @@ at } @@ at], [], [] } + idesc = TableImport $2 @@ at } @@ at], [] } | inline_export table_fields /* Sugar */ - { fun c x at -> let tabs, elems, ims, exs, refs = $2 c x at in - tabs, elems, ims, $1 (TableExport x) c :: exs, refs } - | inline_refer table_fields /* Sugar */ - { fun c x at -> let tabs, elems, ims, exs, refs = $2 c x at in - tabs, elems, ims, exs, $1 (TableExport x) c :: refs } + { fun c x at -> let tabs, elems, ims, exs = $2 c x at in + tabs, elems, ims, $1 (TableExport x) c :: exs } | ref_type LPAR ELEM elem_var_list RPAR /* Sugar */ { fun c x at -> let offset = [i32_const (0l @@ at) @@ at] @@ at in @@ -723,7 +717,7 @@ table_fields : let emode = Active {index = x; offset} @@ at in [{ttype = TableType ({min = size; max = Some size}, $1)} @@ at], [{etype = FuncRefType; einit; emode} @@ at], - [], [], [] } + [], [] } | ref_type LPAR ELEM elem_expr elem_expr_list RPAR /* Sugar */ { fun c x at -> let offset = [i32_const (0l @@ at) @@ at] @@ at in @@ -732,7 +726,7 @@ table_fields : let emode = Active {index = x; offset} @@ at in [{ttype = TableType ({min = size; max = Some size}, $1)} @@ at], [{etype = FuncRefType; einit; emode} @@ at], - [], [], [] } + [], [] } data : | LPAR DATA bind_var_opt string_list RPAR @@ -758,25 +752,22 @@ memory : memory_fields : | memory_type - { fun c x at -> [{mtype = $1} @@ at], [], [], [], [] } + { fun c x at -> [{mtype = $1} @@ at], [], [], [] } | inline_import memory_type /* Sugar */ { fun c x at -> [], [], [{ module_name = fst $1; item_name = snd $1; - idesc = MemoryImport $2 @@ at } @@ at], [], [] } + idesc = MemoryImport $2 @@ at } @@ at], [] } | inline_export memory_fields /* Sugar */ - { fun c x at -> let mems, data, ims, exs, refs = $2 c x at in - mems, data, ims, $1 (MemoryExport x) c :: exs, refs } - | inline_refer memory_fields /* Sugar */ - { fun c x at -> let mems, data, ims, exs, refs = $2 c x at in - mems, data, ims, exs, $1 (MemoryExport x) c :: refs } + { fun c x at -> let mems, data, ims, exs = $2 c x at in + mems, data, ims, $1 (MemoryExport x) c :: exs } | LPAR DATA string_list RPAR /* Sugar */ { fun c x at -> let offset = [i32_const (0l @@ at) @@ at] @@ at in let size = Int32.(div (add (of_int (String.length $3)) 65535l) 65536l) in [{mtype = MemoryType {min = size; max = Some size}} @@ at], [{dinit = $3; dmode = Active {index = x; offset} @@ at} @@ at], - [], [], [] } + [], [] } global : | LPAR GLOBAL bind_var_opt global_fields RPAR @@ -786,18 +777,15 @@ global : global_fields : | global_type const_expr - { fun c x at -> [{gtype = $1; ginit = $2 c} @@ at], [], [], [] } + { fun c x at -> [{gtype = $1; ginit = $2 c} @@ at], [], [] } | inline_import global_type /* Sugar */ { fun c x at -> [], [{ module_name = fst $1; item_name = snd $1; - idesc = GlobalImport $2 @@ at } @@ at], [], [] } + idesc = GlobalImport $2 @@ at } @@ at], [] } | inline_export global_fields /* Sugar */ - { fun c x at -> let globs, ims, exs, refs = $2 c x at in - globs, ims, $1 (GlobalExport x) c :: exs, refs } - | inline_refer global_fields /* Sugar */ - { fun c x at -> let globs, ims, exs, refs = $2 c x at in - globs, ims, exs, $1 (GlobalExport x) c :: refs } + { fun c x at -> let globs, ims, exs = $2 c x at in + globs, ims, $1 (GlobalExport x) c :: exs } /* Imports & Exports */ @@ -844,15 +832,6 @@ inline_export : | LPAR EXPORT name RPAR { let at = at () in fun d c -> {name = $3; edesc = d @@ at} @@ at } -refer : - | LPAR REF export_desc RPAR - { let at = at () and at3 = ati 3 in - fun c -> {rdesc = $3 c @@ at3} @@ at } - -inline_refer : - | LPAR REF RPAR - { let at = at () in fun d c -> {rdesc = d @@ at} @@ at } - /* Modules */ @@ -879,34 +858,32 @@ module_fields1 : { fun c -> ignore ($1 c); $2 c } | global module_fields { fun c -> let gf = $1 c in let mf = $2 c in - fun () -> let globs, ims, exs, refs = gf () in let m = mf () in + fun () -> let globs, ims, exs = gf () in let m = mf () in if globs <> [] && m.imports <> [] then error (List.hd m.imports).at "import after global definition"; - { m with globals = globs @ m.globals; imports = ims @ m.imports; - exports = exs @ m.exports; refers = refs @ m.refers } } + { m with globals = globs @ m.globals; + imports = ims @ m.imports; exports = exs @ m.exports } } | table module_fields { fun c -> let tf = $1 c in let mf = $2 c in - fun () -> let tabs, elems, ims, exs, refs = tf () in let m = mf () in + fun () -> let tabs, elems, ims, exs = tf () in let m = mf () in if tabs <> [] && m.imports <> [] then error (List.hd m.imports).at "import after table definition"; { m with tables = tabs @ m.tables; elems = elems @ m.elems; - imports = ims @ m.imports; exports = exs @ m.exports; - refers = refs @ m.refers } } + imports = ims @ m.imports; exports = exs @ m.exports } } | memory module_fields { fun c -> let mmf = $1 c in let mf = $2 c in - fun () -> let mems, data, ims, exs, refs = mmf () in let m = mf () in + fun () -> let mems, data, ims, exs = mmf () in let m = mf () in if mems <> [] && m.imports <> [] then error (List.hd m.imports).at "import after memory definition"; { m with memories = mems @ m.memories; datas = data @ m.datas; - imports = ims @ m.imports; exports = exs @ m.exports; - refers = refs @ m.refers } } + imports = ims @ m.imports; exports = exs @ m.exports } } | func module_fields { fun c -> let ff = $1 c in let mf = $2 c in - fun () -> let funcs, ims, exs, refs = ff () in let m = mf () in + fun () -> let funcs, ims, exs = ff () in let m = mf () in if funcs <> [] && m.imports <> [] then error (List.hd m.imports).at "import after function definition"; - { m with funcs = funcs @ m.funcs; imports = ims @ m.imports; - exports = exs @ m.exports; refers = refs @ m.refers } } + { m with funcs = funcs @ m.funcs; + imports = ims @ m.imports; exports = exs @ m.exports } } | elem module_fields { fun c -> let ef = $1 c in let mf = $2 c in fun () -> let elems = ef () in let m = mf () in @@ -929,10 +906,6 @@ module_fields1 : { fun c -> let mf = $2 c in fun () -> let m = mf () in {m with exports = $1 c :: m.exports} } - | refer module_fields - { fun c -> let mf = $2 c in - fun () -> let m = mf () in - {m with refers = $1 c :: m.refers} } module_var_opt : | /* empty */ { None } diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index c96ae222..1634ea4c 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -26,13 +26,15 @@ type context = locals : value_type list; results : value_type list; labels : stack_type list; - refers : export_desc' list; + refs : Free.t; } let empty_context = { types = []; funcs = []; tables = []; memories = []; globals = []; datas = []; elems = []; - locals = []; results = []; labels = []; refers = [] } + locals = []; results = []; labels = []; + refs = Free.empty + } let lookup category list x = try Lib.List32.nth list x.it with Failure _ -> @@ -48,13 +50,12 @@ let elem (c : context) x = lookup "elem segment" c.elems x let local (c : context) x = lookup "local" c.locals x let label (c : context) x = lookup "label" c.labels x -let refer category (c : context) f x = - if not (List.mem x.it (Lib.List.map_filter f c.refers)) then +let refer category (s : Free.Set.t) x = + if not (Free.Set.mem x.it s) then error x.at ("undeclared " ^ category ^ " reference " ^ Int32.to_string x.it) -let refer_func (c : context) x = - refer "function" c (function (FuncExport x) -> Some x.it | _ -> None) x +let refer_func (c : context) x = refer "function" c.refs.Free.funcs x (* Stack typing *) @@ -551,12 +552,12 @@ 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; datas; - exports; refers } = m.it + exports } = m.it in let c0 = List.fold_right check_import imports { empty_context with - refers = List.map (fun ex -> ex.it.rdesc.it) refers; + refs = Free.list Free.elem elems; types = List.map (fun ty -> ty.it) types; } in diff --git a/test/core/linking.wast b/test/core/linking.wast index 65999c72..1fdce190 100644 --- a/test/core/linking.wast +++ b/test/core/linking.wast @@ -131,7 +131,8 @@ (module $Mglobal-ex - (func $f (ref)) + (func $f) + (table $dummy funcref (elem $f)) ;; TODO (global (export "g") anyref (ref.func $f)) ) diff --git a/test/core/ref_func.wast b/test/core/ref_func.wast index e9b84b1b..225ec36a 100644 --- a/test/core/ref_func.wast +++ b/test/core/ref_func.wast @@ -4,8 +4,8 @@ (register "M") (module - (func $f (ref) (import "M" "f") (param i32) (result i32)) - (func $g (ref) (param $x i32) (result i32) + (func $f (import "M" "f") (param i32) (result i32)) + (func $g (param $x i32) (result i32) (i32.add (local.get $x) (i32.const 1)) ) @@ -29,6 +29,7 @@ (func (export "set-g") (global.set $v (ref.func $g))) (table $t 1 funcref) + (table $dummy funcref (elem $f $g)) ;; TODO (func (export "call-f") (param $x i32) (result i32) (table.set $t (i32.const 0) (ref.func $f)) diff --git a/test/core/table_grow.wast b/test/core/table_grow.wast index c0b14520..c5db8aef 100644 --- a/test/core/table_grow.wast +++ b/test/core/table_grow.wast @@ -38,7 +38,8 @@ ;; Reject growing to size outside i32 value range (module (table $t 0x10 anyref) - (func $f (ref) (export "grow") (result i32) + (table $dummy funcref (elem $f)) ;; TODO + (func $f (export "grow") (result i32) (table.grow $t (ref.func $f) (i32.const 0xffff_fff0)) ) ) @@ -82,7 +83,8 @@ (func (export "grow") (param i32) (result i32) (table.grow $t (ref.null) (local.get 0)) ) - (func (ref) (export "check-table-null") (param i32 i32) (result anyref) + (table $dummy funcref (elem 1)) ;; TODO + (func (export "check-table-null") (param i32 i32) (result anyref) (local anyref) (local.set 2 (ref.func 1)) (block From 069e4fd9032303ddb39b721fef2036893253a9b5 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 14 Jan 2020 17:37:46 +0100 Subject: [PATCH 4/7] Implement declarative segment syntax --- interpreter/binary/decode.ml | 13 +++++++++++++ interpreter/binary/encode.ml | 6 ++++++ interpreter/exec/eval.ml | 11 +++++++---- interpreter/syntax/ast.ml | 1 + interpreter/syntax/free.ml | 2 +- interpreter/text/arrange.ml | 13 +++++++------ interpreter/text/lexer.mll | 1 + interpreter/text/parser.mly | 7 ++++++- interpreter/valid/valid.ml | 2 ++ test/core/elem.wast | 35 +++++++++++++++++++++++++++++++++++ test/core/linking.wast | 6 ------ test/core/ref_func.wast | 16 +++++++++++++++- test/core/table_grow.wast | 4 ++-- 13 files changed, 96 insertions(+), 21 deletions(-) diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index c9702621..61e94212 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -651,6 +651,9 @@ let active_zero s = let offset = const s in Active {index; offset} +let declarative s = + Declarative + let elem_index s = let x = at var s in [Source.(ref_func x @@ x.at)] @@ -676,6 +679,11 @@ let elem s = let etype = elem_kind s in let einit = vec (at elem_index) s in {etype; einit; emode} + | 0x03l -> + let emode = at declarative s in + let etype = elem_kind s in + let einit = vec (at elem_index) s in + {etype; einit; emode} | 0x04l -> let emode = at active_zero s in let einit = vec const s in @@ -690,6 +698,11 @@ let elem s = let etype = ref_type s in let einit = vec const s in {etype; einit; emode} + | 0x07l -> + let emode = at declarative s in + let etype = ref_type s in + let einit = vec const s in + {etype; einit; emode} | _ -> error s (pos s - 1) "invalid elements segment kind" let elem_section s = diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 690697c7..6910cf42 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -524,6 +524,8 @@ let encode m = | Active {index; offset} -> vu32 0x02l; var index; const offset; elem_kind etype; vec elem_index einit + | Declarative -> + vu32 0x03l; elem_kind etype; vec elem_index einit else match emode.it with | Passive -> @@ -532,6 +534,8 @@ let encode m = vu32 0x04l; const offset; vec const einit | Active {index; offset} -> vu32 0x06l; var index; const offset; ref_type etype; vec const einit + | Declarative -> + vu32 0x07l; ref_type etype; vec const einit let elem_section elems = section 9 (vec elem) elems (elems <> []) @@ -546,6 +550,8 @@ let encode m = vu32 0x00l; const offset; string dinit | Active {index; offset} -> vu32 0x02l; var index; const offset; string dinit + | Declarative -> + assert false let data_section datas = section 11 (vec data) datas (datas <> []) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 99d17836..e1e0a6d8 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -568,31 +568,34 @@ let init_func (inst : module_inst) (func : func_inst) = | _ -> assert false let run_elem i elem = + let at = elem.it.emode.at in + let x = i @@ at in match elem.it.emode.it with | Passive -> [] | Active {index; offset} -> - let at = elem.it.emode.at in - let x = i @@ at in offset.it @ [ Const (I32 0l @@ at) @@ at; Const (I32 (Lib.List32.length elem.it.einit) @@ at) @@ at; TableInit (index, x) @@ at; ElemDrop x @@ at ] + | Declarative -> + [ElemDrop x @@ at] let run_data i data = + let at = data.it.dmode.at in + let x = i @@ at in match data.it.dmode.it with | Passive -> [] | Active {index; offset} -> assert (index.it = 0l); - let at = data.it.dmode.at in - let x = i @@ at in offset.it @ [ Const (I32 0l @@ at) @@ at; Const (I32 (Int32.of_int (String.length data.it.dinit)) @@ at) @@ at; MemoryInit x @@ at; DataDrop x @@ at ] + | Declarative -> assert false let run_start start = [Call start @@ start.at] diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml index 5926bffd..864c5666 100644 --- a/interpreter/syntax/ast.ml +++ b/interpreter/syntax/ast.ml @@ -151,6 +151,7 @@ type segment_mode = segment_mode' Source.phrase and segment_mode' = | Passive | Active of {index : var; offset : const} + | Declarative type elem_segment = elem_segment' Source.phrase and elem_segment' = diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml index 5f612f07..af322f67 100644 --- a/interpreter/syntax/free.ml +++ b/interpreter/syntax/free.ml @@ -96,7 +96,7 @@ let memory (m : memory) = empty let segment_mode f (m : segment_mode) = match m.it with - | Passive -> empty + | Passive | Declarative -> empty | Active {index; offset} -> f (var index) ++ const offset let elem (s : elem_segment) = diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 72420679..2c5ccc85 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -334,10 +334,11 @@ let segment_mode category mode = | Active {index; offset} -> (if index.it = 0l then [] else [Node (category, [atom var index])]) @ [const "offset" offset] + | Declarative -> [Atom "declare"] -let elem seg = +let elem i seg = let {etype; einit; emode} = seg.it in - Node ("elem", + Node ("elem $" ^ nat i, segment_mode "table" emode @ if is_elem_kind etype && List.for_all is_elem_index einit then atom elem_kind etype :: list elem_index einit @@ -345,9 +346,9 @@ let elem seg = atom ref_type etype :: list (const "item") einit ) -let data seg = +let data i seg = let {dinit; dmode} = seg.it in - Node ("data", segment_mode "memory" dmode @ break_bytes dinit) + Node ("data $" ^ nat i, segment_mode "memory" dmode @ break_bytes dinit) (* Modules *) @@ -409,8 +410,8 @@ let module_with_var_opt x_opt m = listi (func_with_index !fx) m.it.funcs @ list export m.it.exports @ opt start m.it.start @ - list elem m.it.elems @ - list data m.it.datas + listi elem m.it.elems @ + listi data m.it.datas ) let binary_module_with_var_opt x_opt bs = diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index 9511a8e3..ac480e64 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -348,6 +348,7 @@ rule token = parse | "memory" { MEMORY } | "elem" { ELEM } | "data" { DATA } + | "declare" { DECLARE } | "offset" { OFFSET } | "import" { IMPORT } | "export" { EXPORT } diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 2f36c3f5..6c1acee1 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -176,7 +176,7 @@ let inline_type_explicit (c : context) x ft at = %token CONST UNARY BINARY TEST COMPARE CONVERT %token REF_ANY REF_NULL REF_FUNC REF_HOST REF_IS_NULL %token FUNC START TYPE PARAM RESULT LOCAL GLOBAL -%token TABLE ELEM MEMORY DATA OFFSET IMPORT EXPORT +%token TABLE ELEM MEMORY DATA DECLARE OFFSET IMPORT EXPORT %token MODULE BIN QUOTE %token SCRIPT REGISTER INVOKE GET %token ASSERT_MALFORMED ASSERT_INVALID ASSERT_SOFT_INVALID ASSERT_UNLINKABLE @@ -679,6 +679,11 @@ elem : fun () -> { etype = (fst $6); einit = (snd $6) c; emode = Active {index = $4 c table; offset = $5 c} @@ at } @@ at } + | LPAR ELEM bind_var_opt DECLARE elem_list RPAR + { let at = at () in + fun c -> ignore ($3 c anon_elem bind_elem); + fun () -> + { etype = (fst $5); einit = (snd $5) c; emode = Declarative @@ at } @@ at } | LPAR ELEM bind_var_opt offset elem_list RPAR /* Sugar */ { let at = at () in fun c -> ignore ($3 c anon_elem bind_elem); diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 1634ea4c..d7d7f295 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -490,6 +490,7 @@ let check_elem_mode (c : context) (t : ref_type) (mode : segment_mode) = require (match_ref_type t et) mode.at "type mismatch in active element segment"; check_const c offset (NumType I32Type) + | Declarative -> () let check_elem (c : context) (seg : elem_segment) = let {etype; einit; emode} = seg.it in @@ -502,6 +503,7 @@ let check_data_mode (c : context) (mode : segment_mode) = | Active {index; offset} -> ignore (memory c index); check_const c offset (NumType I32Type) + | Declarative -> assert false let check_data (c : context) (seg : data_segment) = let {dinit; dmode} = seg.it in diff --git a/test/core/elem.wast b/test/core/elem.wast index bb622ee6..5ff16f9c 100644 --- a/test/core/elem.wast +++ b/test/core/elem.wast @@ -63,6 +63,17 @@ (elem $a24 (i32.const 0) funcref (ref.func $f) (ref.null)) (elem $a25 (i32.const 0) func $f $f) (elem $a26 (i32.const 0) $f $f) + + ;; Declarative + (elem declare funcref) + (elem declare funcref (ref.func $f) (ref.func $f) (ref.null) (ref.func $g)) + (elem declare func) + (elem declare func $f $f $g $g) + + (elem $d1 declare funcref) + (elem $d2 declare funcref (ref.func $f) (ref.func $f) (ref.null) (ref.func $g)) + (elem $d3 declare func) + (elem $d4 declare func $f $f $g $g) ) (module @@ -71,6 +82,8 @@ (table $t funcref (elem (ref.func $f) (ref.null) (ref.func $g))) ) + + ;; Basic use (module @@ -294,6 +307,28 @@ "out of bounds" ) +;; Implicitly dropped elements + +(module + (table 10 funcref) + (elem $e (i32.const 0) func $f) + (func $f) + (func (export "init") + (table.init $e (i32.const 0) (i32.const 0) (i32.const 1)) + ) +) +(assert_trap (invoke "init") "out of bounds") + +(module + (table 10 funcref) + (elem $e declare func $f) + (func $f) + (func (export "init") + (table.init $e (i32.const 0) (i32.const 0) (i32.const 1)) + ) +) +(assert_trap (invoke "init") "out of bounds") + ;; Element without table (assert_invalid diff --git a/test/core/linking.wast b/test/core/linking.wast index 1fdce190..49d55723 100644 --- a/test/core/linking.wast +++ b/test/core/linking.wast @@ -130,12 +130,6 @@ ) -(module $Mglobal-ex - (func $f) - (table $dummy funcref (elem $f)) ;; TODO - (global (export "g") anyref (ref.func $f)) -) - (assert_unlinkable (module (global (import "Mref_ex" "g-var-null") (mut funcref))) "incompatible import type" diff --git a/test/core/ref_func.wast b/test/core/ref_func.wast index 225ec36a..e9033a3b 100644 --- a/test/core/ref_func.wast +++ b/test/core/ref_func.wast @@ -15,6 +15,16 @@ (global funcref (ref.func $g)) (global $v (mut funcref) (ref.func $f)) + (global funcref (ref.func $gf1)) + (global funcref (ref.func $gf2)) + (func (drop (ref.func $ff1)) (drop (ref.func $ff2))) + (elem declare func $gf1 $ff1) + (elem declare funcref (ref.func $gf2) (ref.func $ff2)) + (func $gf1) + (func $gf2) + (func $ff1) + (func $ff2) + (func (export "is_null-f") (result i32) (ref.is_null (ref.func $f)) ) @@ -29,7 +39,7 @@ (func (export "set-g") (global.set $v (ref.func $g))) (table $t 1 funcref) - (table $dummy funcref (elem $f $g)) ;; TODO + (elem declare func $f $g) (func (export "call-f") (param $x i32) (result i32) (table.set $t (i32.const 0) (ref.func $f)) @@ -66,6 +76,10 @@ "unknown function 7" ) +(assert_invalid + (module (func $f) (global funcref (ref.func $f))) + "undeclared function reference" +) (assert_invalid (module (func $f (drop (ref.func $f)))) "undeclared function reference" diff --git a/test/core/table_grow.wast b/test/core/table_grow.wast index c5db8aef..91fc096f 100644 --- a/test/core/table_grow.wast +++ b/test/core/table_grow.wast @@ -38,7 +38,7 @@ ;; Reject growing to size outside i32 value range (module (table $t 0x10 anyref) - (table $dummy funcref (elem $f)) ;; TODO + (elem declare func $f) (func $f (export "grow") (result i32) (table.grow $t (ref.func $f) (i32.const 0xffff_fff0)) ) @@ -83,7 +83,7 @@ (func (export "grow") (param i32) (result i32) (table.grow $t (ref.null) (local.get 0)) ) - (table $dummy funcref (elem 1)) ;; TODO + (elem declare func 1) (func (export "check-table-null") (param i32 i32) (result anyref) (local anyref) (local.set 2 (ref.func 1)) From 8c9270f813fc92a1548f08de4fc9ccccee082644 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 15 Jan 2020 09:45:24 +0100 Subject: [PATCH 5/7] Add spec --- document/core/binary/modules.rst | 10 +++++++--- document/core/exec/modules.rst | 4 +++- document/core/syntax/modules.rst | 14 +++++++++----- document/core/text/modules.rst | 4 +++- document/core/util/macros.def | 6 ++++-- document/core/valid/conventions.rst | 4 +++- document/core/valid/instructions.rst | 4 ++++ document/core/valid/modules.rst | 22 ++++++++++++++++++---- interpreter/README.md | 1 + 9 files changed, 52 insertions(+), 17 deletions(-) diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index e947fc30..706044fc 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -333,20 +333,24 @@ It decodes into a vector of :ref:`element segments ` that represent &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|& \hex{02}~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx) &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|& + \hex{03}~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx) + &\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|& \hex{04}~~e{:}\Bexpr~~\X{el}^\ast{:}\Bvec(\Bexpr) &\Rightarrow& \{ \ETYPE~\FUNCREF, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|& \hex{05}~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr) &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|& \hex{06}~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr) - &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ + &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|& + \hex{07}~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr) + &\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EDECLARATIVE \} \\ \production{element kind} & \Belemkind &::=& \hex{00} &\Rightarrow& \FUNCREF \\ \end{array} .. note:: The initial byte can be interpreted as a bitfield. - Bit 0 indicates a passive segment, - bit 1 indicates the presence of an explicit table index for an active segment, + Bit 0 indicates a passive or declarative segment, + bit 1 indicates the presence of an explicit table index for an active segment and otherwise distinguishes passive from declarative segments, bit 2 indicates the use of element type and element :ref:`expressions ` instead of element kind and element indices. Additional element kinds may be added in future versions of WebAssembly. diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 1211356d..9450ecb4 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -726,7 +726,9 @@ where: \begin{array}{@{}l} \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EPASSIVE\}) \quad=\quad \epsilon \\ \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EACTIVE \{\ETABLE~0, \EOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad - \instr^\ast~(\I32.\CONST~0)~(\I32.\CONST~n)~(\TABLEINIT~i)~(\ELEMDROP~i) \\[1ex] + \instr^\ast~(\I32.\CONST~0)~(\I32.\CONST~n)~(\TABLEINIT~i)~(\ELEMDROP~i) \\ + \F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\reff^n, \EMODE~\EDECLARATIVE\}) \quad=\\ \qquad + (\ELEMDROP~i) \\[1ex] \F{rundata}_i(\{\DINIT~b^n, DMODE~\DPASSIVE\}) \quad=\quad \epsilon \\ \F{rundata}_i(\{\DINIT~b^n, DMODE~\DACTIVE \{\DMEM~0, \DOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad \instr^\ast~(\I32.\CONST~0)~(\I32.\CONST~n)~(\MEMORYINIT~i)~(\DATADROP~i) \\ diff --git a/document/core/syntax/modules.rst b/document/core/syntax/modules.rst index 91562bce..f0973d81 100644 --- a/document/core/syntax/modules.rst +++ b/document/core/syntax/modules.rst @@ -106,10 +106,10 @@ Conventions * The meta variables :math:`x, y` range over indices in any of the other index spaces. -* The notation :math:`\F{idx}(A)` denotes the set of indices from index space :math:`\X{idx}` occurring free in :math:`A`. +* The notation :math:`\F{idx}(A)` denotes the set of indices from index space :math:`\X{idx}` occurring free in :math:`A`. We sometimes reinterpret this set as the :ref:`vector ` of its elements. .. note:: - For example, if :math:`\instr^\ast` is :math:`(\DATADROP~x) (\MEMORYINIT~y)`, then :math:`\freedataidx(\instr^\ast) = \{x, y\}`. + For example, if :math:`\instr^\ast` is :math:`(\DATADROP~x) (\MEMORYINIT~y)`, then :math:`\freedataidx(\instr^\ast) = \{x, y\}`, or equivalently, the vector :math:`x~y`. .. index:: ! type definition, type index, function type @@ -242,10 +242,12 @@ Globals are referenced through :ref:`global indices `, starting with the smallest index not referencing a global :ref:`import `. -.. index:: ! element, active, passive, element index, table, table index, expression, constant, function index, vector +.. index:: ! element, ! element mode, ! active, ! passive, ! declarative, element index, table, table index, expression, constant, function index, vector pair: abstract syntax; element + pair: abstract syntax; element mode single: table; element single: element; segment + single: element; mode .. _syntax-elem: .. _syntax-elemmode: @@ -257,9 +259,10 @@ The initial contents of a table is uninitialized. *Element segments* can be used The |MELEMS| component of a module defines a vector of element segments. Each element segment defines an :ref:`reference type ` and a corresponding list of :ref:`constant ` element :ref:`expressions `. -Element segments have a mode that identifies them as either *passive* or *active*. +Element segments have a mode that identifies them as either *passive*, *active*, or *declarative*. A passive element segment's elements can be copied to a table using the |TABLEINIT| instruction. An active element segment copies its elements into a table during :ref:`instantiation `, as specified by a :ref:`table index ` and a :ref:`constant ` :ref:`expression ` defining an offset into that table. +A declarative element segment is not available at runtime but merely serves to forward-declare references that are formed in code with instructions like :math:`REFFUNC`. .. math:: \begin{array}{llll} @@ -267,7 +270,8 @@ An active element segment copies its elements into a table during :ref:`instanti \{ \ETYPE~\reftype, \EINIT~\vec(\expr), \EMODE~\elemmode \} \\ \production{element segment mode} & \elemmode &::=& \EPASSIVE \\&&|& - \EACTIVE~\{ \ETABLE~\tableidx, \EOFFSET~\expr \} \\ + \EACTIVE~\{ \ETABLE~\tableidx, \EOFFSET~\expr \} \\&&|& + \EDECLARATIVE \\ \end{array} The |EOFFSET| is given by a :ref:`constant ` :ref:`expression `. diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 57f4c630..599b2d90 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -501,7 +501,9 @@ Element segments allow for an optional :ref:`table index ` to ide \text{(}~\text{elem}~~\Tid^?~~(et, y^\ast){:}\Telemlist~\text{)} \\ &&& \qquad \Rightarrow\quad \{ \ETYPE~et, \EINIT~y^\ast, \EMODE~\EPASSIVE \} \\ &&|& \text{(}~\text{elem}~~\Tid^?~~x{:}\Ttableuse_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~(et, y^\ast){:}\Telemlist~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \ETYPE~et, \EINIT~y^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ + \Rightarrow\quad \{ \ETYPE~et, \EINIT~y^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&& + \text{(}~\text{elem}~~\Tid^?~~\text{declare}~~(et, y^\ast){:}\Telemlist~\text{)} \\ &&& \qquad + \Rightarrow\quad \{ \ETYPE~et, \EINIT~y^\ast, \EMODE~\EDECLARATIVE \} \\ \production{element list} & \Telemlist &::=& t{:}\Treftype~~y^\ast{:}\Tvec(\Telemexpr_I) \qquad\Rightarrow\quad ( \ETYPE~t, \EINIT~y^\ast ) \\ \production{element expression} & \Telemexpr &::=& diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 87b5ca28..eb1e57be 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -273,8 +273,9 @@ .. |ETYPE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{type}} .. |EINIT| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{init}} .. |EMODE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{mode}} -.. |EPASSIVE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{passive}} -.. |EACTIVE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{active}} +.. |EPASSIVE| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\K{passive}} +.. |EACTIVE| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\K{active}} +.. |EDECLARATIVE| mathdef:: \xref{syntax/modules}{syntax-elemmode}{\K{declarative}} .. |ETABLE| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{table}} .. |EOFFSET| mathdef:: \xref{syntax/modules}{syntax-elem}{\K{offset}} @@ -782,6 +783,7 @@ .. |CLOCALS| mathdef:: \xref{valid/conventions}{context}{\K{locals}} .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}} .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}} +.. |CREFS| mathdef:: \xref{valid/conventions}{context}{\K{refs}} .. Judgments diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 7f132d7e..9c0a4046 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -43,6 +43,7 @@ which collects relevant information about the surrounding :ref:`module ` that occur in element segments and can hence be used to form references elsewhere. In other words, a context contains a sequence of suitable :ref:`types ` for each :ref:`index space `, describing each defined entry in that space. @@ -64,7 +65,8 @@ More concretely, contexts are defined as :ref:`records ` :math: & \CDATAS & {\ok}^\ast, \\ & \CLOCALS & \valtype^\ast, \\ & \CLABELS & \resulttype^\ast, \\ - & \CRETURN & \resulttype^? ~\} \\ + & \CRETURN & \resulttype^?, \\ + & \CREFS & \funcidx^\ast ~\} \\ \end{array} \end{array} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 9a27e944..843a736a 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -198,11 +198,15 @@ Reference Instructions * The function :math:`C.\CFUNCS[x]` must be defined in the context. +* The :ref:`function index ` :math:`x` must be contained in :math:`C.\CREFS`. + * The instruction is valid with type :math:`[] \to [\FUNCREF]`. .. math:: \frac{ C.\CFUNCS[x] = \functype + \qquad + x \in C.\CREFS }{ C \vdashinstr \REFFUNC~x : [] \to [\FUNCREF] } diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 461b9a55..4d303ca5 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -217,6 +217,18 @@ Element segments :math:`\elem` are not classified by any type but merely checked C; \X{et} \vdashelemmode \EACTIVE~\{ \ETABLE~x, \EOFFSET~\expr \} \ok } +:math:`\EDECLARATIVE` +..................... + +* The element mode is valid for any :ref:`reference type ` :math:`\X{et}`. + +.. math:: + \frac{ + }{ + C; \X{et} \vdashelemmode \EDECLARATIVE \ok + } + + .. index:: data, memory, memory index, expression, byte pair: validation; data @@ -278,7 +290,7 @@ Data segments :math:`\data` are not classified by any type but merely checked fo \qquad C \vdashexprconst \expr \const }{ - C \vdashelemmode \EACTIVE~\{ \DMEM~x, \DOFFSET~\expr \} \ok + C \vdashelemmode \DACTIVE~\{ \DMEM~x, \DOFFSET~\expr \} \ok } @@ -529,6 +541,8 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C.\CRETURN` is empty. + * :math:`C.\CREFS` is the set :math:`\freefuncidx(\module.\MELEMS)`, i.e., the set of :ref:`function indices ` occrring in any of the module's :ref:`element segments `. + * Let :math:`C'` be the :ref:`context ` where :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\X{it}^\ast)` and all other fields are empty. * Under the context :math:`C`: @@ -614,7 +628,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \qquad \X{igt}^\ast = \etglobals(\X{it}^\ast) \\ - C = \{ \CTYPES~\functype^\ast, \CFUNCS~\X{ift}^\ast~\X{ft}^\ast, \CTABLES~\X{itt}^\ast~\X{tt}^\ast, \CMEMS~\X{imt}^\ast~\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast~\X{gt}^\ast, \CELEMS~{\ok}^{N_e}, \CDATAS~{\ok}^{N_d} \} + C = \{ \CTYPES~\functype^\ast, \CFUNCS~\X{ift}^\ast~\X{ft}^\ast, \CTABLES~\X{itt}^\ast~\X{tt}^\ast, \CMEMS~\X{imt}^\ast~\X{mt}^\ast, \CGLOBALS~\X{igt}^\ast~\X{gt}^\ast, \CELEMS~{\ok}^{N_e}, \CDATAS~{\ok}^{N_d}, \CREFS~\freefuncidx(\elem^{N_e}) \} \\ C' = \{ \CGLOBALS~\X{igt}^\ast \} \qquad @@ -630,8 +644,8 @@ Instead, the context :math:`C` for validation of the module's content is constru \MTABLES~\table^\ast, \MMEMS~\mem^\ast, \MGLOBALS~\global^\ast, \\ - \MELEMS~\elem^\ast, - \MDATAS~\data^\ast, + \MELEMS~\elem^{N_e}, + \MDATAS~\data^{N_d}, \MSTART~\start^?, \MIMPORTS~\import^\ast, \MEXPORTS~\export^\ast \} : \X{it}^\ast \to \X{et}^\ast \\ diff --git a/interpreter/README.md b/interpreter/README.md index f38f5720..c420fa96 100644 --- a/interpreter/README.md +++ b/interpreter/README.md @@ -266,6 +266,7 @@ table: ( table ? ) ( table ? ( export )* ( elem * ) ) ;; = (table ? ( export )* ) (elem (i32.const 0) *) elem: ( elem ? (offset * ) * ) ( elem ? * ) ;; = (elem ? (offset ) *) + ( elem ? declare * ) memory: ( memory ? ) ( memory ? ( export ) <...> ) ;; = (export (memory ))+ (memory ? <...>) ( memory ? ( import ) ) ;; = (import ? (memory )) From ec7407657d8d18412c3d1ecc53d0a31e81672a08 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 16 Jan 2020 06:14:03 +0100 Subject: [PATCH 6/7] Typo --- document/core/valid/modules.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 4d303ca5..4337cf86 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -541,7 +541,7 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C.\CRETURN` is empty. - * :math:`C.\CREFS` is the set :math:`\freefuncidx(\module.\MELEMS)`, i.e., the set of :ref:`function indices ` occrring in any of the module's :ref:`element segments `. + * :math:`C.\CREFS` is the set :math:`\freefuncidx(\module.\MELEMS)`, i.e., the set of :ref:`function indices ` occurring in any of the module's :ref:`element segments `. * Let :math:`C'` be the :ref:`context ` where :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\X{it}^\ast)` and all other fields are empty. From 48f710553db11f8cd9e94c4760919b088ff2e375 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 16 Jan 2020 17:11:29 +0100 Subject: [PATCH 7/7] Https links --- document/core/util/macros.def | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 0951e009..4151d7a5 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -3,20 +3,20 @@ .. External Standards .. ------------------ -.. |WasmDraft| replace:: http://webassembly.github.io/spec/core/ -.. _WasmDraft: http://webassembly.github.io/spec/core/ +.. |WasmDraft| replace:: https://webassembly.github.io/reference-types/core/ +.. _WasmDraft: https://webassembly.github.io/reference-types/core/ -.. |WasmIssues| replace:: http://github.com/webassembly/spec/issues/ -.. _WasmIssues: http://github.com/webassembly/spec/issues/ +.. |WasmIssues| replace:: https://github.com/webassembly/reference-types/issues/ +.. _WasmIssues: https://github.com/webassembly/reference-types/issues/ .. |IEEE754| replace:: IEEE 754-2019 .. _IEEE754: https://ieeexplore.ieee.org/document/8766229 .. |Unicode| replace:: Unicode -.. _Unicode: http://www.unicode.org/versions/latest/ +.. _Unicode: https://www.unicode.org/versions/latest/ .. |ASCII| replace:: ASCII -.. _ASCII: http://webstore.ansi.org/RecordDetail.aspx?sku=INCITS+4-1986%5bR2012%5d +.. _ASCII: https://webstore.ansi.org/RecordDetail.aspx?sku=INCITS+4-1986%5bR2012%5d .. External Definitions