From cbe17019508df3d8508e1b6df07c093e92b60a66 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Thu, 16 Feb 2023 13:56:57 +0100 Subject: [PATCH 1/7] Adds validation for exception results. Uses the "current" version of exception results, as it will be changed by #226. --- document/core/appendix/properties.rst | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 2c2c3eea..37aa8f9c 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -58,8 +58,29 @@ Results S \vdashresult \TRAP : [t^\ast] } -.. todo:: - Add validation for exception results. + +:ref:`Results ` :math:`\val^\ast~(\THROWadm~\tagaddr)` +..................................................................... + +* The :ref:`tag address ` :math:`\tagaddr` must be in :math:`\moduleinst.\MITAGS`. + +* The :ref:`external value ` :math:`\EVTAG~\tagaddr` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETTAG~\tagtype`. + +* Let :math:`[t_1^\ast]\to[]` be the :ref:`tag type ` |tagtype|. + +* The values :math:`\val^\ast` must be :ref:`valid ` with types :math:`[t_1^\ast]`. + +* Then the result is valid with :ref:`result type ` :math:`[t_2^\ast]`, for any sequence :math:`t_2^\ast` of :ref:`value types `. + + +.. math:: + \frac{ + \vdashexterntype \ETTAG~[t_1^\ast]\to[]~\ok + \qquad + (S \vdashval \val : t_1)^\ast + }{ + S \vdashresult \val^\ast~(\THROWadm~\tagaddr) : [t_2^\ast] + } .. _module-context: From 4171c4a9b1e0c60ac32fb6c5dfbaad36783a0eb2 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Thu, 23 Feb 2023 18:05:18 +0100 Subject: [PATCH 2/7] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- document/core/appendix/properties.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 37aa8f9c..cfed78a4 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -66,7 +66,7 @@ Results * The :ref:`external value ` :math:`\EVTAG~\tagaddr` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETTAG~\tagtype`. -* Let :math:`[t_1^\ast]\to[]` be the :ref:`tag type ` |tagtype|. +* Let :math:`[t_1^\ast]\to[t_2^\ast]` be the :ref:`tag type ` |tagtype|. * The values :math:`\val^\ast` must be :ref:`valid ` with types :math:`[t_1^\ast]`. @@ -75,11 +75,11 @@ Results .. math:: \frac{ - \vdashexterntype \ETTAG~[t_1^\ast]\to[]~\ok + S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t^\ast] \to [] \qquad - (S \vdashval \val : t_1)^\ast + (S \vdashval \val : t)^\ast }{ - S \vdashresult \val^\ast~(\THROWadm~\tagaddr) : [t_2^\ast] + S \vdashresult \val^\ast~(\THROWadm~\tagaddr) : [{t'}^\ast] } From 66352049fa89fe14eae248792c547f3a9ea86a5f Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 1 Mar 2023 17:56:15 +0100 Subject: [PATCH 3/7] Addressed review comments. --- document/core/appendix/properties.rst | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index cfed78a4..b167d48e 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -62,15 +62,15 @@ Results :ref:`Results ` :math:`\val^\ast~(\THROWadm~\tagaddr)` ..................................................................... -* The :ref:`tag address ` :math:`\tagaddr` must be in :math:`\moduleinst.\MITAGS`. - * The :ref:`external value ` :math:`\EVTAG~\tagaddr` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETTAG~\tagtype`. -* Let :math:`[t_1^\ast]\to[t_2^\ast]` be the :ref:`tag type ` |tagtype|. +* Let :math:`[t^\ast]\to[{t'}^\ast]` be the :ref:`tag type ` |tagtype|. + +* For each :ref:`value ` :math:`\val_i` in :math:`\val^\ast`: -* The values :math:`\val^\ast` must be :ref:`valid ` with types :math:`[t_1^\ast]`. + * The value :math:`\val_i` must be :ref:`valid ` with :ref:`value type ` :math:`t_i`. -* Then the result is valid with :ref:`result type ` :math:`[t_2^\ast]`, for any sequence :math:`t_2^\ast` of :ref:`value types `. +* Then the result is valid with :ref:`result type ` :math:`[{t'}^\ast]`, for any sequence :math:`{t'}^\ast` of :ref:`value types `. .. math:: From 599a343db28542ef90c963ba40ca6893b622995d Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 10 Mar 2023 13:10:21 +0100 Subject: [PATCH 4/7] addressed review comments --- document/core/appendix/properties.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index b167d48e..7741d5e5 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -64,7 +64,9 @@ Results * The :ref:`external value ` :math:`\EVTAG~\tagaddr` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETTAG~\tagtype`. -* Let :math:`[t^\ast]\to[{t'}^\ast]` be the :ref:`tag type ` |tagtype|. +* Let :math:`[t^\ast]\to[t_0^\ast]` be the :ref:`tag type ` |tagtype|. + +* Assert: due to :ref:`validation ` the type sequence :math:`t_0^\ast` must be empty. * For each :ref:`value ` :math:`\val_i` in :math:`\val^\ast`: From af1bcb20b9537e64437c73e38f13d86715b52568 Mon Sep 17 00:00:00 2001 From: Ioanna M Dimitriou H <9728696+ioannad@users.noreply.github.com> Date: Fri, 17 Mar 2023 17:10:33 +0100 Subject: [PATCH 5/7] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- document/core/appendix/properties.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 7741d5e5..84259049 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -68,7 +68,7 @@ Results * Assert: due to :ref:`validation ` the type sequence :math:`t_0^\ast` must be empty. -* For each :ref:`value ` :math:`\val_i` in :math:`\val^\ast`: +* For each :ref:`value ` :math:`\val_i` in :math:`\val^\ast` and corresponding :ref:`value type ` :math:`t_i` in :math:`t_i`: * The value :math:`\val_i` must be :ref:`valid ` with :ref:`value type ` :math:`t_i`. From 602a10a8d40881aef1cde8cc02a107bad1f49dda Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 17 Mar 2023 17:17:12 +0100 Subject: [PATCH 6/7] Addressing review comment https://github.com/WebAssembly/exception-handling/pull/254/files/599a343db28542ef90c963ba40ca6893b622995d#r1137212721 --- document/core/appendix/properties.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 84259049..a053d1da 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -66,7 +66,7 @@ Results * Let :math:`[t^\ast]\to[t_0^\ast]` be the :ref:`tag type ` |tagtype|. -* Assert: due to :ref:`validation ` the type sequence :math:`t_0^\ast` must be empty. +* Due to :ref:`validation ` the type sequence :math:`t_0^\ast` must be empty. * For each :ref:`value ` :math:`\val_i` in :math:`\val^\ast` and corresponding :ref:`value type ` :math:`t_i` in :math:`t_i`: From bac761f6e2a1a398989ed4ec40fb694098b28234 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 14 Apr 2023 18:11:00 +0200 Subject: [PATCH 7/7] Merged the first three steps to one reflecting what is done in THROWadm's typing --- document/core/appendix/properties.rst | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index a053d1da..31eb3be4 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -62,11 +62,7 @@ Results :ref:`Results ` :math:`\val^\ast~(\THROWadm~\tagaddr)` ..................................................................... -* The :ref:`external value ` :math:`\EVTAG~\tagaddr` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETTAG~\tagtype`. - -* Let :math:`[t^\ast]\to[t_0^\ast]` be the :ref:`tag type ` |tagtype|. - -* Due to :ref:`validation ` the type sequence :math:`t_0^\ast` must be empty. +* The :ref:`external tag value ` :math:`\EVTAG~\tagaddr` must be :ref:`valid ` with :ref:`external tag type ` :math:`\ETTAG~[t^\ast]\to[]`. * For each :ref:`value ` :math:`\val_i` in :math:`\val^\ast` and corresponding :ref:`value type ` :math:`t_i` in :math:`t_i`: