From a774d22946b5c13d7f83049be2a19df1b5613c1e Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 25 Nov 2022 22:17:11 +0100 Subject: [PATCH 1/3] Addressed review comment on merged #229 Fixes the typing rule of CAUGHTadm as suggested in: https://github.com/WebAssembly/exception-handling/pull/229#discussion_r1029160012 --- document/core/appendix/properties.rst | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 07717b28..b8a88972 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -676,15 +676,18 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera * The :ref:`values ` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. +* The label :math:`C.\CLABELS[0]` must be defined in the context. -* Under context :math:`C'`, - the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^\ast]`. +* Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type ` :math:`C.\CLABELS[0]`. + +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the first label popped from the |CLABELS| vector. -* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C''` be the same :ref:`context ` as :math:`C'`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. -* Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`. +* Under context :math:`C''`, + the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^\ast]`. +* Then the compound instruction is valid with type :math:`[] \to [t^\ast]`. .. math:: \frac{ @@ -692,9 +695,9 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \qquad (val : t_0)^\ast \qquad - S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] + S; C',\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] }{ - S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] + S; C',\CLABELS\,(\LCATCH^?~[t^\ast]) \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] } From 3a885d0bf28fca63f3e5939719514eea21d2566a Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Sat, 26 Nov 2022 12:51:12 +0100 Subject: [PATCH 2/3] Applying suggestion from PR #241 https://github.com/WebAssembly/exception-handling/pull/241/files/201ff276be6c458e7a819662eb2862bd475f2fcd..f97c9d108a999c3c3fd30f25554a113822bed1b8#r1030097793 --- document/core/appendix/properties.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index b8a88972..176e755b 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -679,10 +679,10 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera * The label :math:`C.\CLABELS[0]` must be defined in the context. * Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type ` :math:`C.\CLABELS[0]`. - + * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the first label popped from the |CLABELS| vector. -* Let :math:`C''` be the same :ref:`context ` as :math:`C'`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. +* Let :math:`C''` be the same :ref:`context ` as :math:`C'`, but with the label type :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. * Under context :math:`C''`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^\ast]`. From 4455a7205ec1464d224ce258aeec4ca98b905b4b Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 15 Feb 2023 18:08:14 +0100 Subject: [PATCH 3/3] Applied suggestions from code review, fixed notation. - Also added the missing _n to CAUGHTadm. The subscript is introduced by the changes in PR #226 --- document/core/appendix/properties.rst | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 12f0fe04..2c2c3eea 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -675,8 +675,8 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera .. index:: caught, throw context -:math:`\CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END` -......................................................... +:math:`\CAUGHTadm_n\{\tagaddr~\val^\ast\}~\instr^\ast~\END` +........................................................... * The :ref:`external tag value ` :math:`\EVTAG~\tagaddr` must be :ref:`valid ` with some :ref:`external tag type ` :math:`\ETTAG~[t_0^\ast] \to []`. @@ -684,16 +684,16 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera * The label :math:`C.\CLABELS[0]` must be defined in the context. -* Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type ` :math:`C.\CLABELS[0]`. +* Let :math:`(\LCATCH^?~[t^n])` be the :ref:`label type ` :math:`C.\CLABELS[0]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the first label popped from the |CLABELS| vector. +* The |LCATCH| must not be present in the label type :math:`C.\CLABELS[0]`. -* Let :math:`C''` be the same :ref:`context ` as :math:`C'`, but with the label type :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector. +* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the label type :math:`(\LCATCH~[t^n])` replacing the first element of the |CLABELS| vector. * Under context :math:`C''`, - the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^\ast]`. + the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t^n]`. -* Then the compound instruction is valid with type :math:`[] \to [t^\ast]`. +* Then the compound instruction is valid with type :math:`[] \to [t^n]`. .. math:: \frac{ @@ -701,9 +701,9 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \qquad (val : t_0)^\ast \qquad - S; C',\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast] + S; C',\CLABELS\,(\LCATCH~[t^n]) \vdashinstrseq \instr^\ast : [] \to [t^n] }{ - S; C',\CLABELS\,(\LCATCH^?~[t^\ast]) \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast] + S; C',\CLABELS\,[t^n] \vdashadmininstr \CAUGHTadm_n\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^n] }