Merge pull request WebAssembly#478 from ShinWonho/ref.null

Fix ref.null semantics
dhil · Nov 14, 2023 · 026ffea · 026ffea
2 parents 72493ed + c91f0a7
commit 026ffea
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 4 deletions.
diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst
@@ -192,13 +192,26 @@ Reference Instructions
 
 .. _exec-ref.null:
 
-:math:`\REFNULL~\X{ht}`
+:math:`\REFNULL~x`
 .......................
 
-1. Push the value :math:`\REFNULL~\X{ht}` to the stack.
+1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
+
+2. Assert: due to :ref:`validation <valid-ref.null>`, the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[x]` exists.
+
+3. Let :math:`\deftype` be the :ref:`defined type <syntax-deftype>` :math:`F.\AMODULE.\MITYPES[x]`.
+
+4. Push the value :math:`\REFNULL~\deftype` to the stack.
+
+.. math::
+   \begin{array}{lcl@{\qquad}l}
+   F; (\REFNULL~x) &\stepto& F; (\REFNULL~\deftype)
+     & (\iff \deftype = F.\AMODULE.\MITYPES[x]) \\
+   \end{array}
 
 .. note::
-   No formal reduction rule is required for this instruction, since the |REFNULL| instruction is already a :ref:`value <syntax-val>`.
+   No formal reduction rule is required for the case |REFNULL| |ABSHEAPTYPE|,
+   since the instruction form is already a :ref:`value <syntax-val>`.
 
 
 .. _exec-ref.func:

diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst
@@ -47,7 +47,7 @@ Any of the aformentioned references can furthermore be wrapped up as an *externa
    \production{vector} & \vecc &::=&
      \V128.\CONST~\i128 \\
    \production{reference} & \reff &::=&
-     \REFNULL~t \\&&|&
+     \REFNULL~(\absheaptype~|~\deftype) \\&&|&
      \REFI31NUM~\u31 \\&&|&
      \REFSTRUCTADDR~\structaddr \\&&|&
      \REFARRAYADDR~\arrayaddr \\&&|&