New element section encoding in the interpreter (#109)

Author: gahaas

document/core/syntax/modules.rst

@@ -261,7 +261,7 @@ The |MELEM| component of a module defines a vector of element segments. Each act
 .. math::
    \begin{array}{llll}
    \production{element segment} & \elem &::=&
-     \{ \ETABLE~\tableidx, \EOFFSET~\expr, \EINIT~\vec(\elemexpr) \} \\&&|&
+     \{ \ETABLE~\tableidx, \EOFFSET~\expr, \ETYPE~\elemtype, \EINIT~\vec(\elemexpr) \} \\&&|&
      \{ \ETYPE~\elemtype, \EINIT~\vec(\elemexpr) \} \\
    \production{elemexpr} & \elemexpr &::=&
      \REFNULL~\END \\&&|&

document/core/text/modules.rst

@@ -293,6 +293,16 @@ An :ref:`element segment <text-elem>` can be given inline with a table definitio
        (\iff \Tid' = \Tid^? \neq \epsilon \vee \Tid' \idfresh) \\
    \end{array}
 
+.. math::
+   \begin{array}{llclll}
+   \production{module field} &
+     \text{(}~\text{table}~~\Tid^?~~\Telemtype~~\text{(}~\text{elem}~~x^n{:}\Tvec(\Texpr)~\text{)}~~\text{)} \quad\equiv \\ & \qquad
+       \text{(}~\text{table}~~\Tid'~~n~~n~~\Telemtype~\text{)}~~
+       \text{(}~\text{elem}~~\Tid'~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Tvec(\Texpr)~\text{)}
+       \\ & \qquad\qquad
+       (\iff \Tid' = \Tid^? \neq \epsilon \vee \Tid' \idfresh) \\
+   \end{array}
+
 Tables can be defined as :ref:`imports <text-import>` or :ref:`exports <text-export>` inline:
 
 .. math::
@@ -483,10 +493,13 @@ Element segments allow for an optional :ref:`table index <text-tableidx>` to ide
 .. math::
    \begin{array}{llclll}
    \production{element segment} & \Telem_I &::=&
-     \text{(}~\text{elem}~~\Tid^?~~x{:}\Ttableidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad
-       \Rightarrow\quad \{ \ETABLE~x, \EOFFSET~e, \EINIT~y^\ast \} \\ &&|&
-     \text{(}~\text{elem}~~\Tid^?~~et{:}\Telemtype~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad
-       \Rightarrow\quad \{ \ETYPE~et, \EINIT~y^\ast \} \\
+     \text{(}~\text{elem}~~\Tid^?~~\text{(}~\text{table}~~x{:}\Ttableidx_I ~\text{)}~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~(et, y^\ast){:}\Telemlist~\text{)} \\ &&& \qquad
+       \Rightarrow\quad \{ \ETABLE~x, \EOFFSET~e, \ETYPE~et, \EINIT~y^\ast \} \\ &&|&
+     \text{(}~\text{elem}~~\Tid^?~~(et, y^\ast){:}\Telemlist~\text{)} \\ &&& \qquad
+       \Rightarrow\quad \{\ETYPE~et,\EINIT~y^\ast \} \\
+   \production{elemlist}  & \Telemlist &::=&
+     \text{func}~~y^\ast{:}\Tvec(\Tfuncidx_I) \qquad\Rightarrow\quad ( \ETYPE~\FUNCREF, \EINIT~y^\ast ) \\ &&|&
+     et{:}\Telemtype~~y^\ast{:}\Tvec(\Texpr_I) \qquad\Rightarrow\quad ( \ETYPE~et, \EINIT~y^\ast ) \\
    \end{array}
 
 .. note::
@@ -506,14 +519,14 @@ As an abbreviation, a single instruction may occur in place of the offset:
      \text{(}~\text{offset}~~\Tinstr~\text{)}
    \end{array}
 
-Also, the table index can be omitted, defaulting to :math:`\T{0}`.
+Also, the table index can be omitted, defaulting to :math:`\T{0}`. If the table index is omitted, also the :math:`\text{func}` keyword can be omitted.
 
 .. math::
    \begin{array}{llclll}
    \production{element segment} &
     \text{(}~\text{elem}~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)}
        &\equiv&
-     \text{(}~\text{elem}~~0~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)}
+     \text{(}~\text{elem}~~\text{(}~\text{table}~~\text{0}~\text{)}~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)}
    \end{array}
 
 As another abbreviation, element segments may also be specified inline with :ref:`table <text-table>` definitions; see the respective section.

document/core/util/macros.def

@@ -702,6 +702,7 @@
 .. |Tmemarg| mathdef:: \xref{text/instructions}{text-memarg}{\T{memarg}}
 .. |Talign| mathdef:: \xref{text/instructions}{text-memarg}{\T{align}}
 .. |Toffset| mathdef:: \xref{text/instructions}{text-memarg}{\T{offset}}
+.. |Telemlist| mathdef:: \xref{text/instructions}{text-memarg}{\T{elemlist}}
 
 .. |Tlabel| mathdef:: \xref{text/instructions}{text-label}{\T{label}}
 .. |Tinstr| mathdef:: \xref{text/instructions}{text-instr}{\T{instr}}

document/core/valid/modules.rst

@@ -147,8 +147,8 @@ Element Segments
 
 Element segments :math:`\elem` are classified by :ref:`segment types <syntax-segtype>`.
 
-:math:`\{ \ETABLE~x, \EOFFSET~\expr, \EINIT~e^\ast \}`
-......................................................
+:math:`\{ \ETABLE~x, \EOFFSET~\expr, \ETYPE~et, \EINIT~e^\ast \}`
+.................................................................
 
 * The table :math:`C.\CTABLES[x]` must be defined in the context.
 
@@ -160,6 +160,8 @@ Element segments :math:`\elem` are classified by :ref:`segment types <syntax-seg
 
 * The expression :math:`\expr` must be :ref:`constant <valid-constant>`.
 
+* The :ref:`element type <syntax-elemtype>` :math:`et` must be |FUNCREF|.
+
 * For each :math:`e_i` in :math:`e^\ast`,
 
   * The element expression :math:`e_i` must be :ref:`valid <valid-elemexpr>`.
@@ -175,15 +177,19 @@ Element segments :math:`\elem` are classified by :ref:`segment types <syntax-seg
      \qquad
      C \vdashexprconst \expr \const
      \qquad
+     et = \FUNCREF
+     \qquad
      (C \vdashelemexpr e \ok)^\ast
    }{
-     C \vdashelem \{ \ETABLE~x, \EOFFSET~\expr, \EINIT~e^\ast \} : \SACTIVE
+     C \vdashelem \{ \ETABLE~x, \EOFFSET~\expr, \ETYPE~et, \EINIT~e^\ast \} : \SACTIVE
    }
 
 
 :math:`\{ \ETYPE~et, \EINIT~e^\ast \}`
 ......................................
 
+* The :ref:`element type <syntax-elemtype>` :math:`et` must be |FUNCREF|.
+
 * For each :math:`e_i` in :math:`e^\ast`,
 
   * The element expression :math:`e_i` must be :ref:`valid <valid-elemexpr>`.
@@ -193,6 +199,8 @@ Element segments :math:`\elem` are classified by :ref:`segment types <syntax-seg
 
 .. math::
    \frac{
+     et = \FUNCREF
+     \qquad
      (C \vdashelemexpr e \ok)^\ast
    }{
      C \vdashelem \{ \ETYPE~et, \EINIT~e^\ast \} : \SPASSIVE

interpreter/binary/decode.ml

@@ -535,6 +535,11 @@ let func_section s =
 
 (* Table section *)
 
+let elem_kind s =
+  match vs7 s with
+  | 0x00 -> FuncRefType
+  | _ -> error s (pos s - 1) "invalid elem kind"
+
 let table s =
   let ttype = table_type s in
   {ttype}
@@ -613,27 +618,10 @@ let code_section s =
 
 (* Element section *)
 
-let segment active passive s =
-  match vu32 s with
-  | 0l ->
-    let index = Source.(0l @@ Source.no_region) in
-    let offset = const s in
-    let init = active s in
-    Active {index; offset; init}
-  | 1l ->
-    let etype, data = passive s in
-    Passive {etype; data}
-  | 2l ->
-    let index = at var s in
-    let offset = const s in
-    let init = active s in
-    Active {index; offset; init}
-  | _ -> error s (pos s - 1) "invalid segment kind"
-
-let active_elem s =
+let elem_index s =
   ref_func (at var s)
 
-let passive_elem s =
+let elem_expr s =
   match u8 s with
   | 0xd0 -> end_ s; ref_null
   | 0xd2 ->
@@ -642,16 +630,45 @@ let passive_elem s =
     ref_func x
   | _ -> error s (pos s - 1) "invalid elem"
 
-let active_elem_segment s =
-  vec (at active_elem) s
+let elem_indices s =
+  vec (at elem_index) s
 
-let passive_elem_segment s =
-  let etype = elem_type s in
-  let init = vec (at passive_elem) s in
-  etype, init
+let elem_refs s =
+  vec (at elem_expr) s
 
 let table_segment s =
-  segment active_elem_segment passive_elem_segment s
+  match vu32 s with
+  | 0l ->
+    let index = Source.(0l @@ Source.no_region) in
+    let offset = const s in
+    let init = elem_indices s in
+    ActiveElem {index; offset; etype = FuncRefType; init}
+  | 1l ->
+    let etype = elem_kind s in
+    let data = elem_indices s in
+    PassiveElem {etype; data}
+  | 2l ->
+    let index = at var s in
+    let offset = const s in
+    let etype = elem_kind s in
+    let init = elem_indices s in
+    ActiveElem {index; offset; etype; init}
+  | 4l ->
+    let index = Source.(0l @@ Source.no_region) in
+    let offset = const s in
+    let init = elem_refs s in
+    ActiveElem {index; offset; etype = FuncRefType; init}
+  | 5l ->
+    let etype = elem_type s in
+    let data = elem_refs s in
+    PassiveElem {etype; data}
+  | 6l ->
+    let index = at var s in
+    let offset = const s in
+    let etype = elem_type s in
+    let init = elem_refs s in
+    ActiveElem {index; offset; etype; init}
+  | _ -> error s (pos s - 1) "invalid table segment kind"
 
 let elem_section s =
   section `ElemSection (vec (at table_segment)) [] s
@@ -660,7 +677,21 @@ let elem_section s =
 (* Data section *)
 
 let memory_segment s =
-  segment string (fun s -> (), string s) s
+  match vu32 s with
+  | 0l ->
+    let index = Source.(0l @@ Source.no_region) in
+    let offset = const s in
+    let init = string s in
+    ActiveData {index; offset; init}
+  | 1l ->
+    let data = string s in
+    PassiveData {data}
+  | 2l ->
+    let index = at var s in
+    let offset = const s in
+    let init = string s in
+    ActiveData {index; offset; init}
+  | _ -> error s (pos s - 1) "invalid memory segment kind"
 
 let data_section s =
   section `DataSection (vec (at memory_segment)) [] s

interpreter/binary/encode.ml

@@ -477,39 +477,50 @@ let encode m =
       section 10 (vec code) fs (fs <> [])
 
     (* Element section *)
-    let segment active passive seg =
-      match seg.it with
-      | Active {index; offset; init} ->
-        if index.it = 0l then
-          u8 0x00
-        else begin
-          u8 0x02; var index
-        end;
-        const offset; active init
-      | Passive {etype; data} ->
-        u8 0x01; passive etype data
-
-    let active_elem el =
+    let elem_expr el =
+      match el.it with
+      | RefNull -> u8 0xd0; end_ ()
+      | RefFunc x -> u8 0xd2; var x; end_ ()
+
+    let elem_index el =
       match el.it with
       | RefNull -> assert false
       | RefFunc x -> var x
 
-    let passive_elem el =
-      match el.it with
-      | RefNull -> u8 0xd0; end_ ()
-      | RefFunc x -> u8 0xd2; var x; end_ ()
+    let elem_indices data = vec elem_index data
+
+    let all_func_ref l = not (List.exists (fun elem -> elem.it = RefNull) l)
 
     let table_segment seg =
-      let active init = vec active_elem init in
-      let passive etype data = elem_type etype; vec passive_elem data in
-      segment active passive seg
+      match seg.it with
+      | ActiveElem {index = {it = 0l;_}; offset; init; _}
+        when all_func_ref init ->
+        u8 0x00; const offset; elem_indices init
+      | PassiveElem {data; _}
+        when all_func_ref data ->
+        u8 0x01; u8 0x00; elem_indices data
+      | ActiveElem {index; offset; init; _}
+        when all_func_ref init ->
+        u8 0x02; var index; const offset; u8 0x00; elem_indices init
+      | ActiveElem {index = {it = 0l;_}; offset; etype; init} ->
+        u8 0x04; const offset; vec elem_expr init
+      | PassiveElem {etype; data} ->
+        u8 0x05; elem_type etype; vec elem_expr data
+      | ActiveElem {index; offset; etype; init} ->
+        u8 0x06; var index; const offset; elem_type etype; vec elem_expr init
 
     let elem_section elems =
       section 9 (vec table_segment) elems (elems <> [])
 
     (* Data section *)
     let memory_segment seg =
-      segment string (fun _ s -> string s) seg
+      match seg.it with
+      | ActiveData {index = {it = 0l;_}; offset; init} ->
+        u8 0x00; const offset; string init
+      | PassiveData {data} ->
+        u8 0x01; string data
+      | ActiveData {index; offset; init} ->
+        u8 0x02; var index; const offset; string init
 
     let data_section datas =
       section 11 (vec memory_segment) datas (datas <> [])

interpreter/exec/eval.ml

@@ -448,13 +448,13 @@ let elem_list inst init =
 
 let create_elem (inst : module_inst) (seg : table_segment) : elem_inst =
   match seg.it with
-  | Active _ -> ref None
-  | Passive {data; _} -> ref (Some (elem_list inst data))
+  | ActiveElem _ -> ref None
+  | PassiveElem {data; _} -> ref (Some (elem_list inst data))
 
 let create_data (inst : module_inst) (seg : memory_segment) : data_inst =
   match seg.it with
-  | Active _ -> ref None
-  | Passive {data; _} -> ref (Some data)
+  | ActiveData _ -> ref None
+  | PassiveData {data} -> ref (Some data)
 
 
 let init_func (inst : module_inst) (func : func_inst) =
@@ -464,25 +464,25 @@ let init_func (inst : module_inst) (func : func_inst) =
 
 let init_table (inst : module_inst) (seg : table_segment) =
   match seg.it with
-  | Active {index; offset = const; init} ->
+  | ActiveElem {index; offset = const; init; _} ->
     let tab = table inst index in
     let offset = i32 (eval_const inst const) const.at in
     let elems = elem_list inst init in
     let len = Int32.of_int (List.length elems) in
     (try Table.init tab elems offset 0l len
     with Table.Bounds -> Link.error seg.at "elements segment does not fit table")
-  | Passive _ -> ()
+  | PassiveElem _ -> ()
 
 let init_memory (inst : module_inst) (seg : memory_segment) =
   match seg.it with
-  | Active {index; offset = const; init} ->
+  | ActiveData {index; offset = const; init} ->
     let mem = memory inst index in
     let offset' = i32 (eval_const inst const) const.at in
     let offset = I64_convert.extend_i32_u offset' in
     let len = Int32.of_int (String.length init) in
     (try Memory.init mem init offset 0L len
     with Memory.Bounds -> Link.error seg.at "data segment does not fit memory")
-  | Passive _ -> ()
+  | PassiveData _ -> ()
 
 
 let add_import (m : module_) (ext : extern) (im : import) (inst : module_inst)

interpreter/syntax/ast.ml

@@ -140,18 +140,21 @@ and memory' =
   mtype : memory_type;
 }
 
-type ('data, 'ty) segment = ('data, 'ty) segment' Source.phrase
-and ('data, 'ty) segment' =
-  | Active of {index : var; offset : const; init : 'data}
-  | Passive of {etype : 'ty; data : 'data}
-
 type elem = elem' Source.phrase
 and elem' =
   | RefNull
   | RefFunc of var
 
-type table_segment = (elem list, elem_type) segment
-type memory_segment = (string, unit) segment
+
+type table_segment = table_segment' Source.phrase
+and table_segment' =
+  | ActiveElem of {index : var; offset : const; etype : elem_type; init : elem list}
+  | PassiveElem of {etype : elem_type; data : elem list}
+
+type memory_segment = memory_segment' Source.phrase
+and memory_segment' =
+  | ActiveData of {index : var; offset : const; init : string}
+  | PassiveData of {data : string}
 
 
 (* Modules *)
@@ -264,3 +267,4 @@ let string_of_name n =
   in
   List.iter escape n;
   Buffer.contents b
+