From 03d832f0d100b5035c05be5b89b2b6cd2328b488 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 13 Feb 2020 15:47:43 +0100 Subject: [PATCH] [spec] Fix missing multi table bulk cases --- document/core/appendix/index-rules.rst | 4 +- document/core/binary/instructions.rst | 4 +- document/core/valid/conventions.rst | 4 +- document/core/valid/instructions.rst | 52 ++++++++++++++++++-------- document/core/valid/modules.rst | 48 ++++++++++++------------ interpreter/valid/valid.ml | 24 +++++++----- test/core/table-sub.wast | 31 +++++++++++++++ 7 files changed, 113 insertions(+), 54 deletions(-) create mode 100644 test/core/table-sub.wast diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index 4d3db62f..525fe139 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -26,8 +26,8 @@ Construct Judgement :ref:`Table ` :math:`C \vdashtable \table : \tabletype` :ref:`Memory ` :math:`C \vdashmem \mem : \memtype` :ref:`Global ` :math:`C \vdashglobal \global : \globaltype` -:ref:`Element segment ` :math:`C \vdashelem \elem \ok` -:ref:`Element mode ` :math:`C \vdashelemmode \elemmode \ok` +:ref:`Element segment ` :math:`C \vdashelem \elem : \reftype` +:ref:`Element mode ` :math:`C \vdashelemmode \elemmode : \reftype` :ref:`Data segment ` :math:`C \vdashdata \data \ok` :ref:`Data mode ` :math:`C \vdashdatamode \datamode \ok` :ref:`Start function ` :math:`C \vdashstart \start \ok` diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 84b6296b..ed3e506d 100644 --- a/document/core/binary/instructions.rst +++ b/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} diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 9c0a4046..727d9ecb 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -38,7 +38,7 @@ which collects relevant information about the surrounding :ref:`module ` :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, \\ diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 843a736a..e55a0803 100644 --- a/document/core/valid/instructions.rst +++ b/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,7 +469,7 @@ Table Instructions .. math:: \frac{ - C.\CTABLES[x] = t + C.\CTABLES[x] = \limits~t }{ C \vdashinstr \TABLEFILL~x : [\I32~t~\I32] \to [] } @@ -477,39 +477,59 @@ Table Instructions .. _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 ` :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 ` :math:`C.\CTABLES[y]`. + +* The :ref:`reference type ` :math:`t_2` must :ref:`match ` :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 ` :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 ` :math:`C.\CELEMS[y]`. + +* The :ref:`reference type ` :math:`t_2` must :ref:`match ` :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 [] } diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 48e4a9ca..fc2f9be1 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -145,10 +145,10 @@ Globals :math:`\global` are classified by :ref:`global types 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 ` 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`, @@ -156,9 +156,11 @@ Element segments :math:`\elem` are not classified by any type but merely checked * The expression :math:`e_i` must be :ref:`constant `. -* The element mode :math:`\elemmode` must be valid for :ref:`reference type ` :math:`\X{et}`. +* The element mode :math:`\elemmode` must be valid with :ref:`reference type ` :math:`t'`. -* Then the element segment is valid. +* The :ref:`reference type ` :math:`t` must :ref:`match ` the reference type :math:`t'`. + +* Then the element segment is valid with :ref:`reference type ` :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 ` :math:`\X{et}`. +* The element mode is valid with any :ref:`reference type `. .. 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 ` :math:`C.\CTABLES[x]`. -* The :ref:`reference type ` :math:`\X{et}` must :ref:`match ` the reference type :math:`t`. - * The expression :math:`\expr` must be :ref:`valid ` with :ref:`result type ` :math:`[\I32]`. * The expression :math:`\expr` must be :ref:`constant `. -* Then the element mode is valid for :ref:`reference type ` :math:`\X{et}`. +* Then the element mode is valid with :ref:`reference type ` :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 ` :math:`\X{et}`. +* The element mode is valid with any :ref:`reference type `. .. 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 ` :math:`\X{it}^\ast` and the internal :ref:`global types ` :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 ` with a :ref:`global type ` :math:`\X{gt}_i`. * For each :math:`\elem_i` in :math:`\module.\MELEMS`, - the segment :math:`\elem_i` must be :ref:`valid `. + the segment :math:`\elem_i` must be :ref:`valid ` with :ref:`reference type ` :math:`\X{rt}_i`. * For each :math:`\data_i` in :math:`\module.\MDATAS`, the segment :math:`\data_i` must be :ref:`valid `. @@ -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 ` :math:`\X{gt}_i`, in index order. +* Let :math:`\X{rt}^\ast` be the concatenation of the :ref:`referense types ` :math:`\X{rt}_i`, in index order. + * Let :math:`\X{it}^\ast` be the concatenation of :ref:`external types ` :math:`\X{it}_i` of the imports, in index order. * Let :math:`\X{et}^\ast` be the concatenation of :ref:`external types ` :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, diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index d7d7f295..9752bd92 100644 --- a/interpreter/valid/valid.ml +++ b/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 = diff --git a/test/core/table-sub.wast b/test/core/table-sub.wast new file mode 100644 index 00000000..66f18310 --- /dev/null +++ b/test/core/table-sub.wast @@ -0,0 +1,31 @@ +(module + (table $t1 10 anyref) + (table $t2 10 funcref) + (elem $el funcref) + (func $f + (table.init $t1 $el (i32.const 0) (i32.const 1) (i32.const 2)) + (table.copy $t1 $t2 (i32.const 0) (i32.const 1) (i32.const 2)) + ) +) + +(assert_invalid + (module + (table $t1 10 funcref) + (table $t2 10 anyref) + (func $f + (table.copy $t1 $t2 (i32.const 0) (i32.const 1) (i32.const 2)) + ) + ) + "type mismatch" +) + +(assert_invalid + (module + (table $t 10 funcref) + (elem $el anyref) + (func $f + (table.init $t $el (i32.const 0) (i32.const 1) (i32.const 2)) + ) + ) + "type mismatch" +)