From c038c9c8064ca78b9181bc3ff2c272974bd45493 Mon Sep 17 00:00:00 2001 From: Wonho Date: Fri, 10 Nov 2023 15:34:52 +0900 Subject: [PATCH 1/6] Fix ref.null semantics --- document/core/exec/instructions.rst | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 637b002d8a..ecbafc76c2 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -195,10 +195,23 @@ Reference Instructions :math:`\REFNULL~\X{ht}` ....................... -1. Push the value :math:`\REFNULL~\X{ht}` to the stack. +1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -.. note:: - No formal reduction rule is required for this instruction, since the |REFNULL| instruction is already a :ref:`value `. +2. If :math:`\X{ht}` is :math:`\typeidx`, then: + + a. Let :math:`\X{ht}_1` be the :ref:`heap type ` :math:`\insttype_{F.\AMODULE}(\X{ht})`. + + b. Push the value :math:`\REFNULL~\X{ht}_1` to the stack. + +3. Else: + + a. Push the value :math:`\REFNULL~\X{ht}` to the stack. + +.. math:: + \begin{array}{lcl@{\qquad}l} + F; (\REFNULL~x) &\stepto& F; (\REFNULL~\X{ht}) + & (\iff \X{ht} = \insttype_{F.\AMODULE}(\X{x})) \\ + \end{array} .. _exec-ref.func: From aecb95dab04c79a87bc76ce53cd29f0f2c186f57 Mon Sep 17 00:00:00 2001 From: Wonho Date: Mon, 13 Nov 2023 17:32:58 +0900 Subject: [PATCH 2/6] Update ref.null syntax and semantics --- document/core/exec/instructions.rst | 16 ++++++---------- document/core/exec/runtime.rst | 2 +- 2 files changed, 7 insertions(+), 11 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ecbafc76c2..43db30278c 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -192,25 +192,21 @@ Reference Instructions .. _exec-ref.null: -:math:`\REFNULL~\X{ht}` +:math:`\REFNULL~x` ....................... 1. Let :math:`F` be the :ref:`current ` :ref:`frame `. -2. If :math:`\X{ht}` is :math:`\typeidx`, then: +2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. - a. Let :math:`\X{ht}_1` be the :ref:`heap type ` :math:`\insttype_{F.\AMODULE}(\X{ht})`. +3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. - b. Push the value :math:`\REFNULL~\X{ht}_1` to the stack. - -3. Else: - - a. Push the value :math:`\REFNULL~\X{ht}` to the stack. +4. Push the value :math:`\REFNULL~\deftype` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} - F; (\REFNULL~x) &\stepto& F; (\REFNULL~\X{ht}) - & (\iff \X{ht} = \insttype_{F.\AMODULE}(\X{x})) \\ + F; (\REFNULL~x) &\stepto& F; (\REFNULL~\deftype) + & (\iff \deftype = F.\AMODULE.\MITYPES[x]) \\ \end{array} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index e0f0753734..a2e03c3cd3 100644 --- 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~t & (\iff t \neq \typeidx) \\&&|& \REFI31NUM~\u31 \\&&|& \REFSTRUCTADDR~\structaddr \\&&|& \REFARRAYADDR~\arrayaddr \\&&|& From 2770996c132883dd7830376a65f9f97aeb305955 Mon Sep 17 00:00:00 2001 From: Wonho Date: Mon, 13 Nov 2023 18:23:28 +0900 Subject: [PATCH 3/6] Fix ref.null syntax --- document/core/exec/runtime.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index a2e03c3cd3..f2d724a96a 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -47,7 +47,8 @@ Any of the aformentioned references can furthermore be wrapped up as an *externa \production{vector} & \vecc &::=& \V128.\CONST~\i128 \\ \production{reference} & \reff &::=& - \REFNULL~t & (\iff t \neq \typeidx) \\&&|& + \REFNULL~\absheaptype \\&&|& + \REFNULL~\deftype \\&&|& \REFI31NUM~\u31 \\&&|& \REFSTRUCTADDR~\structaddr \\&&|& \REFARRAYADDR~\arrayaddr \\&&|& From ae8fb92177996b973978e9b0c0ad488720471f57 Mon Sep 17 00:00:00 2001 From: ShinWonho <50018375+ShinWonho@users.noreply.github.com> Date: Tue, 14 Nov 2023 19:51:34 +0900 Subject: [PATCH 4/6] Update document/core/exec/runtime.rst Co-authored-by: Andreas Rossberg --- document/core/exec/runtime.rst | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index f2d724a96a..f7b17be31c 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -47,8 +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~\absheaptype \\&&|& - \REFNULL~\deftype \\&&|& + \REFNULL~(\absheaptype~|~\deftype) \\&&|& \REFI31NUM~\u31 \\&&|& \REFSTRUCTADDR~\structaddr \\&&|& \REFARRAYADDR~\arrayaddr \\&&|& From ac19ae2b276140d97102311656f80cfc82d771b5 Mon Sep 17 00:00:00 2001 From: Wonho Date: Tue, 14 Nov 2023 20:12:16 +0900 Subject: [PATCH 5/6] Add note for ref.null --- document/core/exec/instructions.rst | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 43db30278c..d7417f53b8 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -209,6 +209,11 @@ Reference Instructions & (\iff \deftype = F.\AMODULE.\MITYPES[x]) \\ \end{array} +.. note:: + This is the reduction rule for |REFNULL| |TYPEIDX|. + No formal reduction rule is required for |REFNULL| |ABSHEAPTYPE|, + since the instruction is already a :ref:`value `. + .. _exec-ref.func: From c91f0a744c6f87974dad949ffe8fcff09de09972 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 14 Nov 2023 12:42:41 +0100 Subject: [PATCH 6/6] Update document/core/exec/instructions.rst --- document/core/exec/instructions.rst | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index d7417f53b8..f2d986085a 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -210,9 +210,8 @@ Reference Instructions \end{array} .. note:: - This is the reduction rule for |REFNULL| |TYPEIDX|. - No formal reduction rule is required for |REFNULL| |ABSHEAPTYPE|, - since the instruction is already a :ref:`value `. + No formal reduction rule is required for the case |REFNULL| |ABSHEAPTYPE|, + since the instruction form is already a :ref:`value `. .. _exec-ref.func: