[spec/interpreter/test] Relax ref check to whole module

document/core/valid/conventions.rst

@@ -43,7 +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.
+* *References*: the list of :ref:`function indices <syntax-funcidx>` 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 <syntax-type>` for each :ref:`index space <syntax-index>`,
 describing each defined entry in that space.

document/core/valid/modules.rst

@@ -526,15 +526,15 @@ 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,
 
   * :math:`C.\CLABELS` is empty,
 
   * :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>`.
+  * :math:`C.\CREFS` is the set :math:`\freefuncidx(\module \with \MFUNCS = \epsilon \with \MSTART = \epsilon)`, i.e., the set of :ref:`function indices <syntax-funcidx>` occurring in the module, except in its :ref:`functions <syntax-func>` or :ref:`start function <syntax-start>`.
 
 * Let :math:`C'` be the :ref:`context <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 \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 \}
      \\
      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::

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 = []; start = None} @@ m.at);
         types = List.map (fun ty -> ty.it) types;
       }
   in

test/core/ref_func.wast

@@ -74,11 +74,42 @@
   "unknown function 7"
 )
 
+
+;; 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) (global funcref (ref.func $f)))
+  (module (func $f (drop (ref.func $f))))
   "undeclared function reference"
 )
 (assert_invalid
-  (module (func $f (drop (ref.func $f))))
+  (module (start $f) (func $f (drop (ref.func $f))))
   "undeclared function reference"
 )