From e41fee9e37bf0b3df904f62608ce44afed4bc82d Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 7 Sep 2022 15:40:24 +0200 Subject: [PATCH 1/4] WIP: Add prose for reduction rule of rethrow. Why WIP: -------- I'm not sure how to justify step 5 of the prose, that is how to assert that the lth label surrounding a rethrow instruction has a CAUGHTadm{a val*} next to it. - Also slightly changed notation to match the [formal overview document](https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md). --- document/core/exec/instructions.rst | 32 ++++++++++++++++++++++++++--- 1 file changed, 29 insertions(+), 3 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index c1a231f7..d038ffd6 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2715,14 +2715,40 @@ Control Instructions :math:`\RETHROW~l` .................. +1. Assert: due to :ref:`validation `, the stack contans at least :math:`l+1` labels. + +2. Let :math:`L` be the :math:`l`-th label appearing on the stack, starting from the top and counting from zero. + +3. Assert: due to :ref:`validation `, :math:`L` is a catch label, i.e., a label of the form :math:`(\LCATCH~[t^\ast])`. + +4. Repeat :math:`l+1` times: + + a. While the instruction at the top of the stack is a value, a |handler|, or a |CAUGHTadm| instruction, do: + + i. Pop the instruction from the stack. + + b. Assert: due to :ref:`validation `, the top of the stack now is a label. + + c. Pop the label from the stack. + +5. Assert: due to **TODO**, the last two instructions popped are a |CAUGHTadm| instruction and the :math:`l+1`-th label, in that order. + .. todo:: - Add prose for the |RETHROW| execution step. + Justify the existence of a |CAUGHTadm| here. Perhaps extend some typing rule? + +6. Let :math:`\CAUGHTadm\{a~\val^\ast\}` be the instruction after the label :math:`L`. + +7. Put all the popped values back on the stack, except the last instruction, the |RETHROW|. + +8. Push the values :math:`\val^\ast` onto the stack. + +8. :ref:`Throw ` an exception with :ref:`tag address ` :math:`a`. .. math:: ~\\[-1ex] \begin{array}{lclr@{\qquad}} - \CAUGHTadm\{a~\val^n\}~\XB^l[\RETHROW~l]~\END &\stepto& - \CAUGHTadm\{a~\val^n\}~\XB^l[\val^n~(\THROWadm~a)]~\END \\ + \CAUGHTadm\{a~\val^\ast\}~\XB^l[\RETHROW~l]~\END &\stepto& + \CAUGHTadm\{a~\val^\ast\}~\XB^l[\val^\ast~(\THROWadm~a)]~\END \\ \end{array} From 4617c8ec88b9d3d56f325b78bb9b5fc2c1a42a92 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Fri, 16 Sep 2022 02:56:21 +0200 Subject: [PATCH 2/4] Apply suggestions from code review Co-authored-by: Heejin Ahn --- document/core/exec/instructions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index d038ffd6..0e5378a2 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2715,7 +2715,7 @@ Control Instructions :math:`\RETHROW~l` .................. -1. Assert: due to :ref:`validation `, the stack contans at least :math:`l+1` labels. +1. Assert: due to :ref:`validation `, the stack contains at least :math:`l+1` labels. 2. Let :math:`L` be the :math:`l`-th label appearing on the stack, starting from the top and counting from zero. @@ -2723,7 +2723,7 @@ Control Instructions 4. Repeat :math:`l+1` times: - a. While the instruction at the top of the stack is a value, a |handler|, or a |CAUGHTadm| instruction, do: + a. While the top of the stack is a value, a |handler|, or a |CAUGHTadm| instruction, do: i. Pop the instruction from the stack. From dce0915e195ca47c84f56ba5b367c8419f98bfdc Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Fri, 9 Dec 2022 23:53:25 +0100 Subject: [PATCH 3/4] Apply suggestions from code review Co-authored-by: Heejin Ahn --- document/core/exec/instructions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 0e5378a2..6e89f671 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2727,7 +2727,7 @@ Control Instructions i. Pop the instruction from the stack. - b. Assert: due to :ref:`validation `, the top of the stack now is a label. + b. Assert: due to :ref:`validation `, the top of the stack now is a label. c. Pop the label from the stack. From a3ec6f53c528d015cc9334a62b07e3c4b616e05a Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Sat, 10 Dec 2022 00:19:38 +0100 Subject: [PATCH 4/4] Simplified prose, removing loop. I no longer consider this PR a WIP. --- document/core/exec/instructions.rst | 25 ++++--------------------- 1 file changed, 4 insertions(+), 21 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 6e89f671..b61bbc2c 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2719,30 +2719,13 @@ Control Instructions 2. Let :math:`L` be the :math:`l`-th label appearing on the stack, starting from the top and counting from zero. -3. Assert: due to :ref:`validation `, :math:`L` is a catch label, i.e., a label of the form :math:`(\LCATCH~[t^\ast])`. +3. Assert: due to :ref:`validation `, :math:`L` is a catch label, i.e., a label of the form :math:`(\LCATCH~[t^\ast])`, which is a label followed by a caught exception in an active catch clause. -4. Repeat :math:`l+1` times: +4. Let :math:`\{a~\val^\ast\}` be the caught exception. - a. While the top of the stack is a value, a |handler|, or a |CAUGHTadm| instruction, do: - - i. Pop the instruction from the stack. - - b. Assert: due to :ref:`validation `, the top of the stack now is a label. - - c. Pop the label from the stack. - -5. Assert: due to **TODO**, the last two instructions popped are a |CAUGHTadm| instruction and the :math:`l+1`-th label, in that order. - -.. todo:: - Justify the existence of a |CAUGHTadm| here. Perhaps extend some typing rule? - -6. Let :math:`\CAUGHTadm\{a~\val^\ast\}` be the instruction after the label :math:`L`. - -7. Put all the popped values back on the stack, except the last instruction, the |RETHROW|. - -8. Push the values :math:`\val^\ast` onto the stack. +5. Push the values :math:`\val^\ast` onto the stack. -8. :ref:`Throw ` an exception with :ref:`tag address ` :math:`a`. +6. :ref:`Throw ` an exception with :ref:`tag address ` :math:`a`. .. math:: ~\\[-1ex]