Add prose for typing rule of try-catch-catch_all. #222

ioannad · 2022-09-07T12:21:13Z

Fixes related .. todo:: section.

Also changed notation to match the formal overview document.

rossberg

Sorry, being a bit late.

rossberg · 2022-09-16T07:52:37Z

document/core/valid/instructions.rst

+* Under context :math:`C'`,
+  the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
+
+* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label <exec-label>` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector.


Suggested change

* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label <exec-label>` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector.

* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector.

rossberg · 2022-09-16T07:59:19Z

document/core/valid/instructions.rst

+
+* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label <exec-label>` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector.
+
+* For every :math:`(\CATCH~x~\instr_2^\ast)`:


Suggested change

* For every :math:`(\CATCH~x~\instr_2^\ast)`:

* For every :math:`x_i` and :math:`\instr_{2i}^\ast` in :math:`(\CATCH~x~\instr_2^\ast)^\ast`:

rossberg · 2022-09-16T08:00:27Z

document/core/valid/instructions.rst

+
+  * The tag :math:`C.\CTAGS[x]` must be defined in the context :math:`C`.
+
+  * Let :math:`[t^\ast] \to []` be its :ref:`tag type <syntax-tagtype>`.


This should actually check that the return type is [].

Suggested change

* Let :math:`[t^\ast] \to []` be its :ref:`tag type <syntax-tagtype>`.

* Let :math:`[t_{3i}^\ast] \to [t_{4i}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`C.\tags[x]`.

* The :ref:`result type <syntax-resulttype>` :math:`[t_{4i}^\ast]` must be empty.

rossberg · 2022-09-16T08:04:51Z

document/core/valid/instructions.rst

+  * Let :math:`[t^\ast] \to []` be its :ref:`tag type <syntax-tagtype>`.
+
+  * Under context :math:`C''`,
+    the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t^\ast] \to [t_2^\ast]`.


Suggested change

the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t^\ast] \to [t_2^\ast]`.

the instruction sequence :math:`\instr_{2i}^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_{3i}^\ast] \to [t_2^\ast]`.

rossberg · 2022-09-16T08:06:22Z

document/core/valid/instructions.rst

+  * Under context :math:`C''`,
+    the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t^\ast] \to [t_2^\ast]`.
+
+* If there is a :math:`(\CATCHALL~\instr_3^\ast)`, then:


Suggested change

* If there is a :math:`(\CATCHALL~\instr_3^\ast)`, then:

* If :math:`(\CATCHALL~\instr_3^\ast)^?` is not empty, then:

aheejin · 2022-09-16T08:18:17Z

@rossberg Thanks for the review! Just in case you'd like to do final check, there also have been several recently landed PRs.

rossberg · 2022-09-16T08:30:16Z

@aheejin, yes, I saw. I'll comment on the ones I find issues with.

rossberg · 2022-09-16T08:31:08Z

Btw, with the introduction of label type, I think all places that say something like "add result type [t*] to C.labels" need to change to say "label type" instead.

… everywhere. This addresses additional review comments to PR WebAssembly#222, that were made after it was merged. The last review comment in the discussion suggests to adjust all validation labels to use label types instead of just result types. Should address all occurrences of validation labels. Additionally adds a boolean catch_label to control frames in the validation algorithm, and some related functionality, fixing the cases for opcodes `catch` and `catch_all`.

ioannad · 2022-10-21T19:29:08Z

Btw, with the introduction of label type, I think all places that say something like "add result type [t*] to C.labels" need to change to say "label type" instead.

@rossberg created PR #241 with the additional changes requested here, also changing to "label type" I think in all appropriate places, including ctrl_frames.

#241) This addresses additional review comments to PR #222, that were made after it was merged. The last review comment in the discussion suggests to adjust all validation labels to use label types instead of just result types. Should address all occurrences of validation labels. Additionally adds a boolean catch_label to control frames in the validation algorithm, and some related functionality, fixing the cases for opcodes `catch` and `catch_all`. * Apply suggestions from code review Co-authored-by: Andreas Rossberg <[email protected]> Co-authored-by: Heejin Ahn <[email protected]> * Reverting changes to typing of CAUGHTadm. Changes to this rule are now done in PR #244

ioannad added 2 commits September 7, 2022 14:32

valid-try-catch: Typesetting and notation like in formal-overview.

db1ff5f

Fix todo:: Prose for valid-try-catch.

06cb90a

ioannad force-pushed the spec-prose-valid-try-catch branch from e172a0c to 06cb90a Compare September 7, 2022 12:33

aheejin approved these changes Sep 8, 2022

View reviewed changes

ioannad merged commit b7cf92c into WebAssembly:main Sep 9, 2022

rossberg reviewed Sep 16, 2022

View reviewed changes

ioannad mentioned this pull request Oct 21, 2022

Address additional review of #222, also fixing label types everywhere. #241

Merged

ioannad deleted the spec-prose-valid-try-catch branch October 24, 2022 17:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add prose for typing rule of try-catch-catch_all. #222

Add prose for typing rule of try-catch-catch_all. #222

Uh oh!

ioannad commented Sep 7, 2022

Uh oh!

rossberg left a comment

Uh oh!

rossberg Sep 16, 2022

Uh oh!

rossberg Sep 16, 2022

Uh oh!

rossberg Sep 16, 2022

Uh oh!

rossberg Sep 16, 2022

Uh oh!

rossberg Sep 16, 2022

Uh oh!

aheejin commented Sep 16, 2022

Uh oh!

rossberg commented Sep 16, 2022

Uh oh!

rossberg commented Sep 16, 2022

Uh oh!

ioannad commented Oct 21, 2022

Uh oh!

Uh oh!

	* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label <exec-label>` :math:`\LCATCH~[t_2^\ast]` prepended to the \|CLABELS\| vector.
	* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`\LCATCH~[t_2^\ast]` prepended to the \|CLABELS\| vector.


		* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label <exec-label>` :math:`\LCATCH~[t_2^\ast]` prepended to the \|CLABELS\| vector.

		* For every :math:`(\CATCH~x~\instr_2^\ast)`:

	* For every :math:`(\CATCH~x~\instr_2^\ast)`:
	* For every :math:`x_i` and :math:`\instr_{2i}^\ast` in :math:`(\CATCH~x~\instr_2^\ast)^\ast`:


		* The tag :math:`C.\CTAGS[x]` must be defined in the context :math:`C`.

		* Let :math:`[t^\ast] \to []` be its :ref:`tag type <syntax-tagtype>`.

-  * Let :math:`[t^\ast] \to []` be its :ref:`tag type <syntax-tagtype>`.
+  * Let :math:`[t_{3i}^\ast] \to [t_{4i}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`C.\tags[x]`.
+  * The :ref:`result type <syntax-resulttype>` :math:`[t_{4i}^\ast]` must be empty.

	the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t^\ast] \to [t_2^\ast]`.
	the instruction sequence :math:`\instr_{2i}^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_{3i}^\ast] \to [t_2^\ast]`.

	* If there is a :math:`(\CATCHALL~\instr_3^\ast)`, then:
	* If :math:`(\CATCHALL~\instr_3^\ast)^?` is not empty, then:

Add prose for typing rule of try-catch-catch_all. #222

Add prose for typing rule of try-catch-catch_all. #222

Uh oh!

Conversation

ioannad commented Sep 7, 2022

Uh oh!

rossberg left a comment

Choose a reason for hiding this comment

Uh oh!

rossberg Sep 16, 2022

Choose a reason for hiding this comment

Uh oh!

rossberg Sep 16, 2022

Choose a reason for hiding this comment

Uh oh!

rossberg Sep 16, 2022

Choose a reason for hiding this comment

Uh oh!

rossberg Sep 16, 2022

Choose a reason for hiding this comment

Uh oh!

rossberg Sep 16, 2022

Choose a reason for hiding this comment

Uh oh!

aheejin commented Sep 16, 2022

Uh oh!

rossberg commented Sep 16, 2022

Uh oh!

rossberg commented Sep 16, 2022

Uh oh!

ioannad commented Oct 21, 2022

Uh oh!

Uh oh!