[spec/interpreter/test] Declarative element segments (#73)

Author: rossberg

document/core/binary/modules.rst

@@ -333,20 +333,24 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` 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 <binary-expr>` instead of element kind and element indices.
 
    Additional element kinds may be added in future versions of WebAssembly.

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) \\

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 <syntax-vec>` 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 <syntax-globalidx>`,
 starting with the smallest index not referencing a global :ref:`import <syntax-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,17 +259,19 @@ 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 <syntax-reftype>` and a corresponding list of :ref:`constant <valid-constant>` element :ref:`expressions <syntax-expr>`.
 
-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 <exec-instantiation>`, as specified by a :ref:`table index <syntax-tableidx>` and a :ref:`constant <valid-constant>` :ref:`expression <syntax-expr>` 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}
    \production{element segment} & \elem &::=&
      \{ \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 <valid-constant>` :ref:`expression <syntax-expr>`.

document/core/text/modules.rst

@@ -501,7 +501,9 @@ Element segments allow for an optional :ref:`table index <text-tableidx>` 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 &::=&

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

document/core/valid/conventions.rst

@@ -43,6 +43,7 @@ which collects relevant information about the surrounding :ref:`module <syntax-m
 * *Locals*: the list of locals declared in the current function (including parameters), represented by their value type.
 * *Labels*: the stack of labels accessible from the current position, represented by their result type.
 * *Return*: the return type of the current function, represented as an optional result type that is absent when no return is allowed, as in free-standing expressions.
+* *References*: the list of :ref:`function indices <syntax-funcidx>` 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 <syntax-type>` for each :ref:`index space <syntax-index>`,
 describing each defined entry in that space.
@@ -64,7 +65,8 @@ More concretely, contexts are defined as :ref:`records <notation-record>` :math:
         & \CDATAS & {\ok}^\ast, \\
         & \CLOCALS & \valtype^\ast, \\
         & \CLABELS & \resulttype^\ast, \\
-        & \CRETURN & \resulttype^? ~\} \\
+        & \CRETURN & \resulttype^?, \\
+        & \CREFS & \funcidx^\ast ~\} \\
      \end{array}
    \end{array}
 

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 <syntax-funcidx>` :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]
    }

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 <syntax-reftype>` :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 <syntax-funcidx>` occurring in any of the module's :ref:`element segments <syntax-elem>`.
+
 * Let :math:`C'` be the :ref:`context <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 \\

interpreter/README.md

@@ -262,10 +262,15 @@ global:  ( global <name>? <global_type> <instr>* )
          ( global <name>? ( import <string> <string> ) <global_type> )      ;; = (import <name>? <string> <string> (global <global_type>))
 table:   ( table <name>? <table_type> )
          ( table <name>? ( export <string> ) <...> )                        ;; = (export <string> (table <N>)) (table <name>? <...>)
-         ( table <name>? ( import <string> <string> ) <table_type> )        ;; = (import <name>? <string> <string> (table <table_type>))
+         ( table <name>? ( import <string> <string> ) <table_type> )        ;; = (import <string> <string> (table <name>? <table_type>))
          ( table <name>? ( export <string> )* <ref_type> ( elem <var>* ) )  ;; = (table <name>? ( export <string> )* <size> <size> <ref_type>) (elem (i32.const 0) <var>*)
+elem:    ( elem <var>? (offset <instr>* ) <var>* )
+         ( elem <var>? <expr> <var>* )                                      ;; = (elem <var>? (offset <expr>) <var>*)
+         ( elem <var>? declare <ref_type> <var>* )
 elem:    ( elem <name>? ( table <var> )? <offset> <ref_type> <item>* )
          ( elem <name>? ( table <var> )? <offset> func <var>* )             ;; = (elem <name>? ( table <var> )? <offset> funcref (ref.func <var>)*)
+         ( elem <var>? declare? <ref_type> <var>* )
+         ( elem <name>? declare? func <var>* )                               ;; = (elem <name>? declare? funcref (ref.func <var>)*)
 offset:  ( offset <instr>* )
          <expr>                                                             ;; = ( offset <expr> )
 item:    ( item <instr>* )

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 =

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 <> [])

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]

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' =