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 002964b9..eb46eb68 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -729,7 +729,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 ac61429a..b23cdb7d 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 f2ad64f3..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 @@ -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..4337cf86 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 ` 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. * 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 4a1c937e..f8895000 100644 --- a/interpreter/README.md +++ b/interpreter/README.md @@ -262,10 +262,15 @@ global: ( global ? * ) ( global ? ( import ) ) ;; = (import ? (global )) table: ( table ? ) ( table ? ( export ) <...> ) ;; = (export (table )) (table ? <...>) - ( table ? ( import ) ) ;; = (import ? (table )) + ( table ? ( import ) ) ;; = (import (table ? )) ( table ? ( export )* ( elem * ) ) ;; = (table ? ( export )* ) (elem (i32.const 0) *) +elem: ( elem ? (offset * ) * ) + ( elem ? * ) ;; = (elem ? (offset ) *) + ( elem ? declare * ) elem: ( elem ? ( table )? * ) ( elem ? ( table )? func * ) ;; = (elem ? ( table )? funcref (ref.func )*) + ( elem ? declare? * ) + ( elem ? declare? func * ) ;; = (elem ? declare? funcref (ref.func )*) offset: ( offset * ) ;; = ( offset ) item: ( item * ) 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 8fc03360..58802850 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -573,7 +573,7 @@ let create_export (inst : module_inst) (ex : export) : export_inst = | TableExport x -> ExternTable (table inst x) | MemoryExport x -> ExternMemory (memory inst x) | GlobalExport x -> ExternGlobal (global inst x) - in name, ext + in (name, ext) let create_elem (inst : module_inst) (seg : elem_segment) : elem_inst = let {etype; einit; _} = seg.it in @@ -600,31 +600,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 79181e80..543469d8 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 39e1474c..af322f67 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} @@ -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/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 ce32cc62..6fc76e93 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 a74a4431..3a1c3f11 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 } | "item" { ITEM } | "import" { IMPORT } diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 8220539a..305765c6 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 ITEM IMPORT EXPORT +%token TABLE ELEM MEMORY DATA DECLARE OFFSET ITEM IMPORT EXPORT %token MODULE BIN QUOTE %token SCRIPT REGISTER INVOKE GET %token ASSERT_MALFORMED ASSERT_INVALID ASSERT_SOFT_INVALID ASSERT_UNLINKABLE @@ -687,6 +687,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/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..d7d7f295 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -26,12 +26,15 @@ type context = locals : value_type list; results : value_type list; labels : stack_type list; + refs : Free.t; } let empty_context = { types = []; funcs = []; tables = []; memories = []; globals = []; datas = []; elems = []; - locals = []; results = []; labels = [] } + locals = []; results = []; labels = []; + refs = Free.empty + } let lookup category list x = try Lib.List32.nth list x.it with Failure _ -> @@ -47,6 +50,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 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.refs.Free.funcs x + (* Stack typing *) @@ -334,6 +344,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type = | RefFunc x -> let _ft = func c x in + refer_func c x; [] --> [RefType FuncRefType] | Const v -> @@ -479,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 @@ -491,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 @@ -545,7 +558,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 + refs = Free.list Free.elem elems; + types = List.map (fun ty -> ty.it) types; + } in let c1 = { c0 with diff --git a/test/core/elem.wast b/test/core/elem.wast index b594acd6..6661c9a8 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 bf6356fb..49d55723 100644 --- a/test/core/linking.wast +++ b/test/core/linking.wast @@ -129,6 +129,7 @@ "incompatible import type" ) + (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..e9033a3b 100644 --- a/test/core/ref_func.wast +++ b/test/core/ref_func.wast @@ -5,7 +5,9 @@ (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 $g (param $x i32) (result i32) + (i32.add (local.get $x) (i32.const 1)) + ) (global anyref (ref.func $f)) (global anyref (ref.func $g)) @@ -13,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)) ) @@ -27,6 +39,7 @@ (func (export "set-g") (global.set $v (ref.func $g))) (table $t 1 funcref) + (elem declare func $f $g) (func (export "call-f") (param $x i32) (result i32) (table.set $t (i32.const 0) (ref.func $f)) @@ -62,3 +75,12 @@ ) "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 158df3ca..91fc096f 100644 --- a/test/core/table_grow.wast +++ b/test/core/table_grow.wast @@ -38,6 +38,7 @@ ;; Reject growing to size outside i32 value range (module (table $t 0x10 anyref) + (elem declare func $f) (func $f (export "grow") (result i32) (table.grow $t (ref.func $f) (i32.const 0xffff_fff0)) ) @@ -82,6 +83,7 @@ (func (export "grow") (param i32) (result i32) (table.grow $t (ref.null) (local.get 0)) ) + (elem declare func 1) (func (export "check-table-null") (param i32 i32) (result anyref) (local anyref) (local.set 2 (ref.func 1))