From 556009120fcc802e412a07a163aa3e2bb8075d35 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 31 Aug 2022 14:17:56 +0200 Subject: [PATCH 1/6] Simplified throw context example, with concrete types but not concrete values. Addresses @aheejin's request in a previous review comment: https://github.com/WebAssembly/exception-handling/pull/180#discussion_r955477590 Originally I wrote this using - `val_{i32} = (i32.const 1)`, - `val_{f32} = (f32.const 2.0)`, and - `val_{i64} = (i64.const 3)`, but the example seemed then really long. To keep the example relatively short I switched to the current version. --- document/core/exec/runtime.rst | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index d3df56ae..803aa541 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -732,23 +732,24 @@ Throw contexts allow matching the program context around a throw instruction up .. note:: For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. - Assume that :math:`\expand_F(bt) = [t1^n] \to [t2^m]`, for some :math:`n > m` such that :math:`t1^n[(n-m):n] = t2^m`, - and that the tag address `a` of :math:`x` corresponds to the tag type :math:`[t2^m] \to []`. + Assume that :math:`\expand_F(bt) = [i32 f32 i64] \to [f32 i64]`, + and that the tag address `a` of :math:`x` corresponds to the tag type :math:`[f32 i64] \to []`. + Let :math:`\val_{i32}`, :math:`\val_{f32}`, and :math:`\val_{i64}` be values of type |i32|, |f32|, and |i64| respectively. .. math:: \begin{array}{ll} - & \hspace{-5ex} S;~F;~\val^n~(\TRY~\X{bt}~(\THROW~x)~\CATCH~x~\RETURN~\END) \\ - \stepto & S;~F;~\LABEL_m\{\} (\CATCHadm\{a~\RETURN\}~\val^n~(\THROW~x)~\END)~\END \\ + & \hspace{-5ex} F;~\val_{i32}~\val_{f32}~\val_{i64}~(\TRY~\X{bt}~(\THROW~x)~\CATCH~x~\END) \\ + \stepto & F;~\LABEL_2\{\} (\CATCHadm\{a~\epsilon}~\val_{i32}~\val_{f32}~\val_{i64}~(\THROW~x)~\END)~\END \\ \end{array} - We denote :math:`\val^n = \val^{n-m} \val^m`. :ref:`Handling the thrown exception ` with tag address :math:`a` in the throw context - :math:`T=[val^{n-m}\_]`, with the exception handler :math:`H=\CATCHadm\{a~\RETURN\}` gives: + :math:`T=[val_{i32}\_]`, with the exception handler :math:`H=\CATCHadm\{a~\epsilon\}` gives: .. math:: \begin{array}{lll} - \stepto & S;~F;~\LABEL_m\{\}~(\CAUGHTadm\{a~\val^m\}~\val^m~\RETURN~\END)~\END & \hspace{9ex}\ \\ - \stepto & \val^m & \\ + \stepto & F;~\LABEL_2\{\}~(\CAUGHTadm\{a~\val_{f32}~\val_{i64}\}~\val_{f32}~\val_{i64}~\END)~\END & \hspace{9ex}\ \\ + \stepto & F;~\LABEL_2\{\}~\val_{f32}~\val_{i64}~\END & \hspace{9ex}\ \\ + \stepto & \val_{f32}~\val_{i64} & \\ \end{array} From 0301d88f427bddb8303f24d2ae9ec16f3691aba7 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Thu, 1 Sep 2022 16:49:56 +0200 Subject: [PATCH 2/6] Typesetting fixes. --- document/core/exec/runtime.rst | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 803aa541..c92880d8 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -732,14 +732,14 @@ Throw contexts allow matching the program context around a throw instruction up .. note:: For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. - Assume that :math:`\expand_F(bt) = [i32 f32 i64] \to [f32 i64]`, - and that the tag address `a` of :math:`x` corresponds to the tag type :math:`[f32 i64] \to []`. - Let :math:`\val_{i32}`, :math:`\val_{f32}`, and :math:`\val_{i64}` be values of type |i32|, |f32|, and |i64| respectively. + Assume that :math:`\expand_F(bt) = [\I32~\F32~\I64] \to [\F32~\I64]`, + and that the tag address `a` of :math:`x` corresponds to the tag type :math:`[\F32~\I64] \to []`. + Let :math:`val_{i32}`, :math:`val_{f32}`, and :math:`val_{i64}` be values of type |I32|, |F32|, and |I64| respectively. .. math:: \begin{array}{ll} - & \hspace{-5ex} F;~\val_{i32}~\val_{f32}~\val_{i64}~(\TRY~\X{bt}~(\THROW~x)~\CATCH~x~\END) \\ - \stepto & F;~\LABEL_2\{\} (\CATCHadm\{a~\epsilon}~\val_{i32}~\val_{f32}~\val_{i64}~(\THROW~x)~\END)~\END \\ + & \hspace{-5ex} F;~val_{i32}~val_{f32}~val_{i64}~(\TRY~\X{bt}~(\THROW~x)~\CATCH~x~\END) \\ + \stepto & F;~\LABEL_2\{\} (\CATCHadm\{a~\epsilon\}~val_{i32}~val_{f32}~val_{i64}~(\THROW~x)~\END)~\END \\ \end{array} :ref:`Handling the thrown exception ` with tag address :math:`a` in the throw context @@ -747,17 +747,17 @@ Throw contexts allow matching the program context around a throw instruction up .. math:: \begin{array}{lll} - \stepto & F;~\LABEL_2\{\}~(\CAUGHTadm\{a~\val_{f32}~\val_{i64}\}~\val_{f32}~\val_{i64}~\END)~\END & \hspace{9ex}\ \\ - \stepto & F;~\LABEL_2\{\}~\val_{f32}~\val_{i64}~\END & \hspace{9ex}\ \\ - \stepto & \val_{f32}~\val_{i64} & \\ + \stepto & F;~\LABEL_2\{\}~(\CAUGHTadm\{a~val_{f32}~val_{i64}\}~val_{f32}~val_{i64}~\END)~\END & \hspace{9ex}\ \\ + \stepto & F;~\LABEL_2\{\}~val_{f32}~val_{i64}~\END & \hspace{9ex}\ \\ + \stepto & val_{f32}~val_{i64} & \\ \end{array} - When a throw of the form :math:`val^m (\THROWadm~a)` occurs, we search for the maximal surrounding throw context :math:`T`, - which means we pop any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:`val^m (\THROWadm~a)`, + When a throw of the form :math:`\val^m (\THROWadm~a)` occurs, we search for the maximal surrounding throw context :math:`T`, + which means we pop any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:`\val^m (\THROWadm~a)`, until we find an exception handler (corresponding to a try block) that :ref:`handles the exception `. - We then append the values :math:`val^m:[t^m]` to the tag address :math:`a` into a new |CAUGHTadm| instruction which we push on the stack. + We then append the values :math:`\val^m:[t^m]` to the tag address :math:`a` into a new |CAUGHTadm| instruction which we push on the stack. In other words, when a throw occurs, normal execution halts and exceptional execution begins, until the throw is the continuation (i.e., in the place of a :math:`\_`) of a throw context in a catching try block. @@ -805,7 +805,7 @@ Finally, the following definition of *evaluation context* and associated structu \begin{array}{llll} \production{(evaluation contexts)} & E &::=& [\_] ~|~ - \val^\ast~E~\instr^\ast ~|~ + val^\ast~E~\instr^\ast ~|~ \LABEL_n\{\instr^\ast\}~E~\END \\ \end{array} From 5989fde55bec4b518a741a1f5fdbee92e90f8465 Mon Sep 17 00:00:00 2001 From: Ioanna Dimitriou Date: Fri, 16 Sep 2022 00:18:04 +0200 Subject: [PATCH 3/6] Addressed review comments. --- document/core/exec/runtime.rst | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index c92880d8..2d537b55 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -734,22 +734,22 @@ Throw contexts allow matching the program context around a throw instruction up Assume that :math:`\expand_F(bt) = [\I32~\F32~\I64] \to [\F32~\I64]`, and that the tag address `a` of :math:`x` corresponds to the tag type :math:`[\F32~\I64] \to []`. - Let :math:`val_{i32}`, :math:`val_{f32}`, and :math:`val_{i64}` be values of type |I32|, |F32|, and |I64| respectively. + Let :math:`\val_{i32}`, :math:`\val_{f32}`, and :math:`\val_{i64}` be values of type |I32|, |F32|, and |I64| respectively. .. math:: \begin{array}{ll} - & \hspace{-5ex} F;~val_{i32}~val_{f32}~val_{i64}~(\TRY~\X{bt}~(\THROW~x)~\CATCH~x~\END) \\ - \stepto & F;~\LABEL_2\{\} (\CATCHadm\{a~\epsilon\}~val_{i32}~val_{f32}~val_{i64}~(\THROW~x)~\END)~\END \\ + & \hspace{-5ex} F;~\val_{i32}~\val_{f32}~\val_{i64}~(\TRY~\X{bt}~(\THROW~x)~\CATCH~x~\END) \\ + \stepto & F;~\LABEL_2\{\} (\CATCHadm\{a~\epsilon\}~\val_{i32}~\val_{f32}~\val_{i64}~(\THROW~x)~\END)~\END \\ \end{array} :ref:`Handling the thrown exception ` with tag address :math:`a` in the throw context - :math:`T=[val_{i32}\_]`, with the exception handler :math:`H=\CATCHadm\{a~\epsilon\}` gives: + :math:`T=[\val_{i32}\_]`, with the exception handler :math:`H=\CATCHadm\{a~\epsilon\}` gives: .. math:: \begin{array}{lll} - \stepto & F;~\LABEL_2\{\}~(\CAUGHTadm\{a~val_{f32}~val_{i64}\}~val_{f32}~val_{i64}~\END)~\END & \hspace{9ex}\ \\ - \stepto & F;~\LABEL_2\{\}~val_{f32}~val_{i64}~\END & \hspace{9ex}\ \\ - \stepto & val_{f32}~val_{i64} & \\ + \stepto & F;~\LABEL_2\{\}~(\CAUGHTadm\{a~\val_{f32}~\val_{i64}\}~\val_{f32}~\val_{i64}~\END)~\END & \hspace{9ex}\ \\ + \stepto & F;~\LABEL_2\{\}~\val_{f32}~\val_{i64}~\END & \hspace{9ex}\ \\ + \stepto & \val_{f32}~\val_{i64} & \\ \end{array} @@ -759,8 +759,8 @@ Throw contexts allow matching the program context around a throw instruction up until we find an exception handler (corresponding to a try block) that :ref:`handles the exception `. We then append the values :math:`\val^m:[t^m]` to the tag address :math:`a` into a new |CAUGHTadm| instruction which we push on the stack. - In other words, when a throw occurs, normal execution halts and exceptional execution begins, until the throw - is the continuation (i.e., in the place of a :math:`\_`) of a throw context in a catching try block. + In other words, a thrown exception is caught when it's the continuation of a throw context in a catching try block, + i.e., it's inside a catching try block, which is the innermost with respect to the throw. In this particular case, the exception is caught by the exception handler :math:`H` and its values are returned. From 48dd359e2dbd6ff002bca93bcefdcca2d9d010a1 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Fri, 16 Sep 2022 14:59:20 +0200 Subject: [PATCH 4/6] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- document/core/exec/runtime.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 2d537b55..fb77300d 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -730,10 +730,10 @@ Throw contexts allow matching the program context around a throw instruction up |CAUGHTadm| blocks do not represent active handlers. Instead, they delimit the continuation of a handler that has already been selected. Their sole purpose is to record the exception that has been caught, such that |RETHROW| can access it inside such a block. .. note:: - For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. + For example, catching a simple :ref:`throw ` in a :ref:`try block ` would be as follows. Assume that :math:`\expand_F(bt) = [\I32~\F32~\I64] \to [\F32~\I64]`, - and that the tag address `a` of :math:`x` corresponds to the tag type :math:`[\F32~\I64] \to []`. + and that the tag address `a` of :math:`x` has tag type :math:`[\F32~\I64] \to []`. Let :math:`\val_{i32}`, :math:`\val_{f32}`, and :math:`\val_{i64}` be values of type |I32|, |F32|, and |I64| respectively. .. math:: @@ -760,7 +760,7 @@ Throw contexts allow matching the program context around a throw instruction up We then append the values :math:`\val^m:[t^m]` to the tag address :math:`a` into a new |CAUGHTadm| instruction which we push on the stack. In other words, a thrown exception is caught when it's the continuation of a throw context in a catching try block, - i.e., it's inside a catching try block, which is the innermost with respect to the throw. + i.e., it is inside a catching try block, which is the innermost with respect to the throw. In this particular case, the exception is caught by the exception handler :math:`H` and its values are returned. From 6df227fc639f4bbaa0645404214050e9abe20ebc Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 16 Sep 2022 15:08:16 +0200 Subject: [PATCH 5/6] Addressed review comments. --- document/core/exec/runtime.rst | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index fb77300d..e490b553 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -752,14 +752,12 @@ Throw contexts allow matching the program context around a throw instruction up \stepto & \val_{f32}~\val_{i64} & \\ \end{array} - - When a throw of the form :math:`\val^m (\THROWadm~a)` occurs, we search for the maximal surrounding throw context :math:`T`, which means we pop any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:`\val^m (\THROWadm~a)`, until we find an exception handler (corresponding to a try block) that :ref:`handles the exception `. We then append the values :math:`\val^m:[t^m]` to the tag address :math:`a` into a new |CAUGHTadm| instruction which we push on the stack. - In other words, a thrown exception is caught when it's the continuation of a throw context in a catching try block, + In other words, an exception throw is caught when it is the continuation of a throw context in a catching try block, i.e., it is inside a catching try block, which is the innermost with respect to the throw. In this particular case, the exception is caught by the exception handler :math:`H` and its values are returned. From 9715e4f6b1bf59d3d8f5831557c9967156c243c2 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Tue, 11 Oct 2022 16:41:13 +0200 Subject: [PATCH 6/6] Added review suggestion, fixed merge artifact --- document/core/exec/runtime.rst | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index d1415a0c..e8485d34 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -752,17 +752,14 @@ If no exception :ref:`handler that catches the exception ` is fo \end{array} - When a throw of the form :math:`val^m (\THROWadm~a)` occurs, search for the maximal surrounding throw context :math:`T` is performed, - which means any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:`val^m (\THROWadm~a)` are popped, + When a throw of the form :math:`\val^m (\THROWadm~a)` occurs, search for the maximal surrounding throw context :math:`T` is performed, + which means any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:`\val^m (\THROWadm~a)` are popped, until a :ref:`handler ` for the exception is found. Then a new |CAUGHTadm| instruction, containing the tag address :math:`a` and the values :math:`\val^m`, is pushed onto the stack. - If no exception :ref:`handler that catches the exception ` is found, the computation :ref:`results ` in an uncaught exception result value, which contains the exception's entire throw context. - In this particular case, the exception is caught by the exception handler :math:`H` and its values are returned. - .. index:: ! configuration, ! thread, store, frame, instruction, module instruction .. _syntax-thread: .. _syntax-config: @@ -800,7 +797,7 @@ Finally, the following definition of *evaluation context* and associated structu \begin{array}{llll} \production{(evaluation contexts)} & E &::=& [\_] ~|~ - val^\ast~E~\instr^\ast ~|~ + \val^\ast~E~\instr^\ast ~|~ \LABEL_n\{\instr^\ast\}~E~\END \\ \end{array}