From a85de9d9de43e1274cb36f1ed5351e4bb632a8bc Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 13 May 2020 12:22:25 +0200 Subject: [PATCH 1/2] [spec/interpreter/test] Relax ref check to whole module --- document/core/valid/conventions.rst | 2 +- document/core/valid/modules.rst | 26 +++++++++++++---------- interpreter/valid/valid.ml | 2 +- test/core/ref_func.wast | 33 ++++++++++++++++++++++++++--- 4 files changed, 47 insertions(+), 16 deletions(-) diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 405ad23e..b6a49b0c 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -43,7 +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. +* *References*: the list of :ref:`function indices ` that occur in the module outside functions and can hence be used to form references inside them. In other words, a context contains a sequence of suitable :ref:`types ` for each :ref:`index space `, describing each defined entry in that space. diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index b86a62f0..ef520501 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -526,7 +526,7 @@ Instead, the context :math:`C` for validation of the module's content is constru * :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`, + * :math:`C.\CDATAS` is :math:`{\ok}^n`, where :math:`n` is the length of the vector :math:`\module.\MDATAS`, * :math:`C.\CLOCALS` is empty, @@ -534,7 +534,7 @@ 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 `. + * :math:`C.\CREFS` is the set :math:`\freefuncidx(\module \with \MFUNCS = \epsilon)`, i.e., the set of :ref:`function indices ` occurring in the module, except in its :ref:`functions `. * Let :math:`C'` be the :ref:`context ` where: @@ -603,7 +603,7 @@ Instead, the context :math:`C` for validation of the module's content is constru .. math:: \frac{ \begin{array}{@{}c@{}} - (\vdashfunctype \functype \ok)^\ast + (\vdashfunctype \type \ok)^\ast \quad (C \vdashfunc \func : \X{ft})^\ast \quad @@ -615,7 +615,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \\ (C \vdashelem \elem : \X{rt})^\ast \quad - (C \vdashdata \data \ok)^{N_d} + (C \vdashdata \data \ok)^n \quad (C \vdashstart \start \ok)^? \quad @@ -631,28 +631,32 @@ 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~\X{rt}^\ast, \CDATAS~{\ok}^{N_d}, \CREFS~\freefuncidx(\elem^\ast) \} + x^\ast = \freefuncidx(\module \with \MFUNCS = \epsilon) + \\ + C = \{ \CTYPES~\type^\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, \CREFS~x^\ast \} \\ C' = \{ \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CREFS~(C.\CREFS) \} \qquad |C.\CMEMS| \leq 1 \qquad (\export.\ENAME)^\ast ~\F{disjoint} - \end{array} - }{ - \vdashmodule \{ + \\ + \module = \{ \begin{array}[t]{@{}l@{}} - \MTYPES~\functype^\ast, + \MTYPES~\type^\ast, \MFUNCS~\func^\ast, \MTABLES~\table^\ast, \MMEMS~\mem^\ast, \MGLOBALS~\global^\ast, \\ \MELEMS~\elem^\ast, - \MDATAS~\data^{N_d}, + \MDATAS~\data^n, \MSTART~\start^?, \MIMPORTS~\import^\ast, - \MEXPORTS~\export^\ast \} : \X{it}^\ast \to \X{et}^\ast \\ + \MEXPORTS~\export^\ast \} \end{array} + \end{array} + }{ + \vdashmodule \module : \X{it}^\ast \to \X{et}^\ast } .. note:: diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 80998371..92e05a19 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -584,7 +584,7 @@ let check_module (m : module_) = let c0 = List.fold_right check_import imports { empty_context with - refs = Free.list Free.elem elems; + refs = Free.module_ ({m.it with funcs = []} @@ m.at); types = List.map (fun ty -> ty.it) types; } in diff --git a/test/core/ref_func.wast b/test/core/ref_func.wast index 436b3866..5da14969 100644 --- a/test/core/ref_func.wast +++ b/test/core/ref_func.wast @@ -74,10 +74,37 @@ "unknown function 7" ) -(assert_invalid - (module (func $f) (global funcref (ref.func $f))) - "undeclared function reference" + +;; Reference declaration + +(module + (func $f1) + (func $f2) + (func $f3) + (func $f4) + (func $f5) + (func $f6) + + (table $t 1 funcref) + + (global funcref (ref.func $f1)) + (export "f" (func $f2)) + (elem (table $t) (i32.const 0) func $f3) + (elem (table $t) (i32.const 0) funcref (ref.func $f4)) + (elem func $f5) + (elem funcref (ref.func $f6)) + + (func + (ref.func $f1) + (ref.func $f2) + (ref.func $f3) + (ref.func $f4) + (ref.func $f5) + (ref.func $f6) + (return) + ) ) + (assert_invalid (module (func $f (drop (ref.func $f)))) "undeclared function reference" From 5a6ff06e08f0d4f28ee48844ffde8bd11ed5cb0e Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 13 May 2020 18:01:10 +0200 Subject: [PATCH 2/2] Exclude start function --- document/core/valid/modules.rst | 4 ++-- interpreter/valid/valid.ml | 2 +- test/core/ref_func.wast | 4 ++++ 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index ef520501..eeed38f3 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -534,7 +534,7 @@ 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 \with \MFUNCS = \epsilon)`, i.e., the set of :ref:`function indices ` occurring in the module, except in its :ref:`functions `. + * :math:`C.\CREFS` is the set :math:`\freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon)`, i.e., the set of :ref:`function indices ` occurring in the module, except in its :ref:`functions ` or :ref:`start function `. * Let :math:`C'` be the :ref:`context ` where: @@ -631,7 +631,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \qquad \X{igt}^\ast = \etglobals(\X{it}^\ast) \\ - x^\ast = \freefuncidx(\module \with \MFUNCS = \epsilon) + x^\ast = \freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon) \\ C = \{ \CTYPES~\type^\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, \CREFS~x^\ast \} \\ diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 92e05a19..a6a6a2d2 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -584,7 +584,7 @@ let check_module (m : module_) = let c0 = List.fold_right check_import imports { empty_context with - refs = Free.module_ ({m.it with funcs = []} @@ m.at); + refs = Free.module_ ({m.it with funcs = []; start = None} @@ m.at); types = List.map (fun ty -> ty.it) types; } in diff --git a/test/core/ref_func.wast b/test/core/ref_func.wast index 5da14969..c0c5a0cc 100644 --- a/test/core/ref_func.wast +++ b/test/core/ref_func.wast @@ -109,3 +109,7 @@ (module (func $f (drop (ref.func $f)))) "undeclared function reference" ) +(assert_invalid + (module (start $f) (func $f (drop (ref.func $f)))) + "undeclared function reference" +)