[spec/interpreter/test] Fix binary & validation for table.copy/init

document/core/appendix/index-rules.rst

@@ -26,8 +26,8 @@ Construct                                        Judgement
 :ref:`Table <valid-table>`                       :math:`C \vdashtable \table : \tabletype`
 :ref:`Memory <valid-mem>`                        :math:`C \vdashmem \mem : \memtype`
 :ref:`Global <valid-global>`                     :math:`C \vdashglobal \global : \globaltype`
-:ref:`Element segment <valid-elem>`              :math:`C \vdashelem \elem \ok`
-:ref:`Element mode <valid-elemmode>`             :math:`C \vdashelemmode \elemmode \ok`
+:ref:`Element segment <valid-elem>`              :math:`C \vdashelem \elem : \reftype`
+:ref:`Element mode <valid-elemmode>`             :math:`C \vdashelemmode \elemmode : \reftype`
 :ref:`Data segment <valid-data>`                 :math:`C \vdashdata \data \ok`
 :ref:`Data mode <valid-datamode>`                :math:`C \vdashdatamode \datamode \ok`
 :ref:`Start function <valid-start>`              :math:`C \vdashstart \start \ok`

document/core/binary/instructions.rst

@@ -157,9 +157,9 @@ Table Instructions
      \hex{FC}~\hex{0F}~~x{:}\Btableidx &\Rightarrow& \TABLEGROW~x \\ &&|&
      \hex{FC}~\hex{10}~~x{:}\Btableidx &\Rightarrow& \TABLESIZE~x \\ &&|&
      \hex{FC}~\hex{11}~~x{:}\Btableidx &\Rightarrow& \TABLEFILL~x \\
-     \hex{FC}~\hex{0C}~~\hex{00}~x{:}\Belemidx &\Rightarrow& \TABLEINIT~x \\ &&|&
+     \hex{FC}~\hex{0C}~~x{:}\Btableidx~~y{:}\Belemidx &\Rightarrow& \TABLEINIT~x~y \\ &&|&
      \hex{FC}~\hex{0D}~~x{:}\Belemidx &\Rightarrow& \ELEMDROP~x \\ &&|&
-     \hex{FC}~\hex{0E}~~\hex{00}~~\hex{00} &\Rightarrow& \TABLECOPY \\
+     \hex{FC}~\hex{0E}~~x{:}\Btableidx~~y{:}\Btableidx &\Rightarrow& \TABLECOPY~x~y \\
    \end{array}
 
 

document/core/valid/conventions.rst

@@ -38,7 +38,7 @@ which collects relevant information about the surrounding :ref:`module <syntax-m
 * *Tables*: the list of tables declared in the current module, represented by their table type.
 * *Memories*: the list of memories declared in the current module, represented by their memory type.
 * *Globals*: the list of globals declared in the current module, represented by their global type.
-* *Element Segments*: the list of element segments declared in the current module, each represented by an |ok| entry.
+* *Element Segments*: the list of element segments declared in the current module, represented by their element type.
 * *Data Segments*: the list of data segments declared in the current module, each represented by an |ok| entry.
 * *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.
@@ -61,7 +61,7 @@ More concretely, contexts are defined as :ref:`records <notation-record>` :math:
         & \CTABLES & \tabletype^\ast, \\
         & \CMEMS & \memtype^\ast, \\
         & \CGLOBALS & \globaltype^\ast, \\
-        & \CELEMS & {\ok}^\ast, \\
+        & \CELEMS & \reftype^\ast, \\
         & \CDATAS & {\ok}^\ast, \\
         & \CLOCALS & \valtype^\ast, \\
         & \CLABELS & \resulttype^\ast, \\

document/core/valid/instructions.rst

@@ -431,7 +431,7 @@ Table Instructions
 
 .. math::
    \frac{
-     C.\CTABLES[x] = t
+     C.\CTABLES[x] = \tabletype
    }{
      C \vdashinstr \TABLESIZE~x : [] \to [\I32]
    }
@@ -450,7 +450,7 @@ Table Instructions
 
 .. math::
    \frac{
-     C.\CTABLES[x] = t
+     C.\CTABLES[x] = \limits~t
    }{
      C \vdashinstr \TABLEGROW~x : [t~\I32] \to [\I32]
    }
@@ -469,47 +469,67 @@ Table Instructions
 
 .. math::
    \frac{
-     C.\CTABLES[x] = t
+     C.\CTABLES[x] = \limits~t
    }{
      C \vdashinstr \TABLEFILL~x : [\I32~t~\I32] \to []
    }
 
 
 .. _valid-table.copy:
 
-:math:`\TABLECOPY`
-.....................
+:math:`\TABLECOPY~x~y`
+......................
+
+* The table :math:`C.\CTABLES[x]` must be defined in the context.
+
+* Let :math:`\limits_1~t_1` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
+
+* The table :math:`C.\CTABLES[y]` must be defined in the context.
 
-* The table :math:`C.\CTABLES[0]` must be defined in the context.
+* Let :math:`\limits_2~t_2` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[y]`.
+
+* The :ref:`reference type <syntax-reftype>` :math:`t_2` must :ref:`match <match-reftype>` :math:`t_1`.
 
 * Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`.
 
 .. math::
    \frac{
-     C.\CTABLES[0] = \tabletype
+     C.\CTABLES[x] = \limits_1~t_1
+     \qquad
+     C.\CTABLES[x] = \limits_2~t_2
+     \qquad
+     \vdashreftypematch t_2 \matchesvaltype t_1
    }{
-     C \vdashinstr \TABLECOPY : [\I32~\I32~\I32] \to []
+     C \vdashinstr \TABLECOPY~x~y : [\I32~\I32~\I32] \to []
    }
 
 
 .. _valid-table.init:
 
-:math:`\TABLEINIT~x`
-.....................
+:math:`\TABLEINIT~x~y`
+......................
 
-* The table :math:`C.\CTABLES[0]` must be defined in the context.
+* The table :math:`C.\CTABLES[x]` must be defined in the context.
 
-* The element segment :math:`C.\CELEMS[x]` must be defined in the context.
+* Let :math:`\limits~t_1` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
+
+* The element segment :math:`C.\CELEMS[y]` must be defined in the context.
+
+* Let :math:`t_2` be the :ref:`reference type <syntax-reftype>` :math:`C.\CELEMS[y]`.
+
+* The :ref:`reference type <syntax-reftype>` :math:`t_2` must :ref:`match <match-reftype>` :math:`t_1`.
 
 * Then the instruction is valid with type :math:`[\I32~\I32~\I32] \to []`.
 
 .. math::
    \frac{
-     C.\CTABLES[0] = \tabletype
+     C.\CTABLES[x] = \limits_1~t_1
+     \qquad
+     C.\CELEMS[y] = t_2
      \qquad
-     C.\CELEMS[x] = {\ok}
+     \vdashreftypematch t_2 \matchesvaltype t_1
    }{
-     C \vdashinstr \TABLEINIT~x : [\I32~\I32~\I32] \to []
+     C \vdashinstr \TABLEINIT~x~y : [\I32~\I32~\I32] \to []
    }
 
 
@@ -524,7 +544,7 @@ Table Instructions
 
 .. math::
    \frac{
-     C.\CELEMS[x] = {\ok}
+     C.\CELEMS[x] = t
    }{
      C \vdashinstr \ELEMDROP~x : [] \to []
    }

document/core/valid/modules.rst

@@ -145,20 +145,22 @@ Globals :math:`\global` are classified by :ref:`global types <syntax-globaltype>
 Element Segments
 ~~~~~~~~~~~~~~~~
 
-Element segments :math:`\elem` are not classified by any type but merely checked for well-formedness.
+Element segments :math:`\elem` are classified by the :ref:`reference type <syntax-reftype>` of their elements.
 
-:math:`\{ \ETYPE~et, \EINIT~e^\ast, \EMODE~\elemmode \}`
-........................................................
+:math:`\{ \ETYPE~t, \EINIT~e^\ast, \EMODE~\elemmode \}`
+.......................................................
 
 * For each :math:`e_i` in :math:`e^\ast`,
 
   * The expression :math:`e_i` must be :ref:`valid <valid-expr>`.
 
   * The expression :math:`e_i` must be :ref:`constant <valid-const>`.
 
-* The element mode :math:`\elemmode` must be valid for :ref:`reference type <syntax-reftype>` :math:`\X{et}`.
+* The element mode :math:`\elemmode` must be valid with :ref:`reference type <syntax-reftype>` :math:`t'`.
 
-* Then the element segment is valid.
+* The :ref:`reference type <syntax-reftype>` :math:`t` must :ref:`match <match-reftype>` the reference type :math:`t'`.
+
+* Then the element segment is valid with :ref:`reference type <syntax-reftype>` :math:`t`.
 
 
 .. math::
@@ -167,9 +169,11 @@ Element segments :math:`\elem` are not classified by any type but merely checked
      \qquad
      (C \vdashexprconst e \const)^\ast
      \qquad
-     C; \X{et} \vdashelemmode \elemmode \ok
+     C \vdashelemmode \elemmode : t'
+     \qquad
+     \vdashreftypematch t \matchesvaltype t'
    }{
-     C \vdashelem \{ \ETYPE~et, \EINIT~e^\ast, \EMODE~\elemmode \} \ok
+     C \vdashelem \{ \ETYPE~t, \EINIT~e^\ast, \EMODE~\elemmode \} : t
    }
 
 
@@ -178,12 +182,12 @@ Element segments :math:`\elem` are not classified by any type but merely checked
 :math:`\EPASSIVE`
 .................
 
-* The element mode is valid for any :ref:`reference type <syntax-reftype>` :math:`\X{et}`.
+* The element mode is valid with any :ref:`reference type <syntax-reftype>`.
 
 .. math::
    \frac{
    }{
-     C; \X{et} \vdashelemmode \EPASSIVE \ok
+     C \vdashelemmode \EPASSIVE : \reftype
    }
 
 
@@ -194,38 +198,34 @@ Element segments :math:`\elem` are not classified by any type but merely checked
 
 * Let :math:`\limits~t` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
 
-* The :ref:`reference type <syntax-reftype>` :math:`\X{et}` must :ref:`match <match-reftype>` the reference type :math:`t`.
-
 * The expression :math:`\expr` must be :ref:`valid <valid-expr>` with :ref:`result type <syntax-resulttype>` :math:`[\I32]`.
 
 * The expression :math:`\expr` must be :ref:`constant <valid-constant>`.
 
-* Then the element mode is valid for :ref:`reference type <syntax-reftype>` :math:`\X{et}`.
+* Then the element mode is valid with :ref:`reference type <syntax-reftype>` :math:`t`.
 
 .. math::
    \frac{
      \begin{array}{@{}c@{}}
      C.\CTABLES[x] = \limits~t
-     \qquad
-     \vdashreftypematch \X{et} \matchesvaltype t
      \\
      C \vdashexpr \expr : [\I32]
      \qquad
      C \vdashexprconst \expr \const
      \end{array}
    }{
-     C; \X{et} \vdashelemmode \EACTIVE~\{ \ETABLE~x, \EOFFSET~\expr \} \ok
+     C \vdashelemmode \EACTIVE~\{ \ETABLE~x, \EOFFSET~\expr \} : t 
    }
 
 :math:`\EDECLARATIVE`
 .....................
 
-* The element mode is valid for any :ref:`reference type <syntax-reftype>` :math:`\X{et}`.
+* The element mode is valid with any :ref:`reference type <syntax-reftype>`.
 
 .. math::
    \frac{
    }{
-     C; \X{et} \vdashelemmode \EDECLARATIVE \ok
+     C \vdashelemmode \EDECLARATIVE : \reftype
    }
 
 
@@ -290,7 +290,7 @@ Data segments :math:`\data` are not classified by any type but merely checked fo
      \qquad
      C \vdashexprconst \expr \const
    }{
-     C \vdashelemmode \DACTIVE~\{ \DMEM~x, \DOFFSET~\expr \} \ok
+     C \vdashdatamode \DACTIVE~\{ \DMEM~x, \DOFFSET~\expr \} \ok
    }
 
 
@@ -531,7 +531,7 @@ Instead, the context :math:`C` for validation of the module's content is constru
   * :math:`C.\CGLOBALS` is :math:`\etglobals(\X{it}^\ast)` concatenated with :math:`\X{gt}^\ast`,
     with the import's :ref:`external types <syntax-externtype>` :math:`\X{it}^\ast` and the internal :ref:`global types <syntax-globaltype>` :math:`\X{gt}^\ast` as determined below,
 
-  * :math:`C.\CELEMS` is :math:`{\ok}^{N_e}`, where :math:`N_e` is the length of the vector :math:`\module.\MELEMS`,
+  * :math:`C.\CELEMS` is :math:`{\X{rt}}^\ast` as determined below,
 
   * :math:`C.\CDATAS` is :math:`{\ok}^{N_d}`, where :math:`N_d` is the length of the vector :math:`\module.\MDATAS`,
 
@@ -573,7 +573,7 @@ Instead, the context :math:`C` for validation of the module's content is constru
       the definition :math:`\global_i` must be :ref:`valid <valid-global>` with a :ref:`global type <syntax-globaltype>` :math:`\X{gt}_i`.
 
   * For each :math:`\elem_i` in :math:`\module.\MELEMS`,
-    the segment :math:`\elem_i` must be :ref:`valid <valid-elem>`.
+    the segment :math:`\elem_i` must be :ref:`valid <valid-elem>` with :ref:`reference type <syntax-reftype>` :math:`\X{rt}_i`.
 
   * For each :math:`\data_i` in :math:`\module.\MDATAS`,
     the segment :math:`\data_i` must be :ref:`valid <valid-data>`.
@@ -599,6 +599,8 @@ Instead, the context :math:`C` for validation of the module's content is constru
 
 * Let :math:`\X{gt}^\ast` be the concatenation of the internal :ref:`global types <syntax-globaltype>` :math:`\X{gt}_i`, in index order.
 
+* Let :math:`\X{rt}^\ast` be the concatenation of the :ref:`referense types <syntax-reftype>` :math:`\X{rt}_i`, in index order.
+
 * Let :math:`\X{it}^\ast` be the concatenation of :ref:`external types <syntax-externtype>` :math:`\X{it}_i` of the imports, in index order.
 
 * Let :math:`\X{et}^\ast` be the concatenation of :ref:`external types <syntax-externtype>` :math:`\X{et}_i` of the exports, in index order.
@@ -618,7 +620,7 @@ Instead, the context :math:`C` for validation of the module's content is constru
      \quad
      (C' \vdashglobal \global : \X{gt})^\ast
      \\
-     (C \vdashelem \elem \ok)^{N_e}
+     (C \vdashelem \elem : \X{rt})^\ast
      \quad
      (C \vdashdata \data \ok)^{N_d}
      \quad
@@ -636,7 +638,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}, \CREFS~\freefuncidx(\elem^{N_e}) \}
+     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~\X{rt}^\ast, \CDATAS~{\ok}^{N_d}, \CREFS~\freefuncidx(\elem^\ast) \}
      \\
      C' = \{ \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \}
      \qquad
@@ -652,7 +654,7 @@ 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^{N_e},
+         \MELEMS~\elem^\ast,
          \MDATAS~\data^{N_d},
          \MSTART~\start^?,
          \MIMPORTS~\import^\ast,

interpreter/valid/valid.ml

@@ -21,8 +21,8 @@ type context =
   tables : table_type list;
   memories : memory_type list;
   globals : global_type list;
+  elems : ref_type list;
   datas : unit list;
-  elems : unit list;
   locals : value_type list;
   results : value_type list;
   labels : stack_type list;
@@ -31,7 +31,7 @@ type context =
 
 let empty_context =
   { types = []; funcs = []; tables = []; memories = [];
-    globals = []; datas = []; elems = [];
+    globals = []; elems = []; datas = [];
     locals = []; results = []; labels = [];
     refs = Free.empty
   }
@@ -45,8 +45,8 @@ let func (c : context) x = lookup "function" c.funcs x
 let table (c : context) x = lookup "table" c.tables x
 let memory (c : context) x = lookup "memory" c.memories x
 let global (c : context) x = lookup "global" c.globals x
-let data (c : context) x = lookup "data segment" c.datas x
 let elem (c : context) x = lookup "elem segment" c.elems x
+let data (c : context) x = lookup "data segment" c.datas x
 let local (c : context) x = lookup "local" c.locals x
 let label (c : context) x = lookup "label" c.labels x
 
@@ -288,13 +288,19 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
     [NumType I32Type; RefType t; NumType I32Type] --> []
 
   | TableCopy (x, y) ->
-    ignore (table c x);
-    ignore (table c y);
+    let TableType (_lim1, t1) = table c x in
+    let TableType (_lim2, t2) = table c y in
+    require (match_ref_type t2 t1) x.at
+      ("type mismatch: source element type " ^ string_of_ref_type t1 ^
+       " does not match destination element type " ^ string_of_ref_type t2);
     [NumType I32Type; NumType I32Type; NumType I32Type] --> []
 
   | TableInit (x, y) ->
-    ignore (table c x);
-    ignore (elem c y);
+    let TableType (_lim1, t1) = table c x in
+    let t2 = elem c y in
+    require (match_ref_type t2 t1) x.at
+      ("type mismatch: source element type " ^ string_of_ref_type t1 ^
+       " does not match destination element type " ^ string_of_ref_type t2);
     [NumType I32Type; NumType I32Type; NumType I32Type] --> []
 
   | ElemDrop x ->
@@ -568,8 +574,8 @@ let check_module (m : module_) =
       funcs = c0.funcs @ List.map (fun f -> type_ c0 f.it.ftype) funcs;
       tables = c0.tables @ List.map (fun tab -> tab.it.ttype) tables;
       memories = c0.memories @ List.map (fun mem -> mem.it.mtype) memories;
-      elems = List.map (fun _ -> ()) elems;
-      datas = List.map (fun _ -> ()) datas;
+      elems = List.map (fun elem -> elem.it.etype) elems;
+      datas = List.map (fun _data -> ()) datas;
     }
   in
   let c =