Adds validation for exception results.#254
Conversation
Uses the "current" version of exception results, as it will be changed by WebAssembly#226.
| :ref:`Results <syntax-result>` :math:`\val^\ast~(\THROWadm~\tagaddr)` | ||
| ..................................................................... | ||
|
|
||
| * The :ref:`tag address <syntax-tagaddr>` :math:`\tagaddr` must be in :math:`\moduleinst.\MITAGS`. |
There was a problem hiding this comment.
That isn't right, it may come from any module. It must only exist in the store, which is already verified by the next step.
|
|
||
| * Let :math:`[t_1^\ast]\to[]` be the :ref:`tag type <syntax-tagtype>` |tagtype|. | ||
|
|
||
| * The values :math:`\val^\ast` must be :ref:`valid <valid-val>` with types :math:`[t_1^\ast]`. |
There was a problem hiding this comment.
The sequence of values does not form a result itself here, so we shouldn't type it against a result type. Rather use the same "loop" as in the regular result case (mirroring what the formal rule does).
Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>
| * The :ref:`external value <syntax-externval>` :math:`\EVTAG~\tagaddr` must be :ref:`valid <valid-externval-tag>` with some :ref:`external type <syntax-externtype>` :math:`\ETTAG~\tagtype`. | ||
|
|
||
| * Let :math:`[t_1^\ast]\to[]` be the :ref:`tag type <syntax-tagtype>` |tagtype|. | ||
| * Let :math:`[t^\ast]\to[{t'}^\ast]` be the :ref:`tag type <syntax-tagtype>` |tagtype|. |
There was a problem hiding this comment.
There seems to be a step missing after this one that checks that t'* is empty.
| * The value :math:`\val_i` must be :ref:`valid <valid-val>` with :ref:`value type <syntax-valtype>` :math:`t_i`. | ||
|
|
||
| * Then the result is valid with :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]`, for any sequence :math:`t_2^\ast` of :ref:`value types <syntax-valtype>`. | ||
| * Then the result is valid with :ref:`result type <syntax-resulttype>` :math:`[{t'}^\ast]`, for any sequence :math:`{t'}^\ast` of :ref:`value types <syntax-valtype>`. |
There was a problem hiding this comment.
We have a name clash, this is a different t'*.
There was a problem hiding this comment.
Renamed the first occurrence to t_0^\ast.
|
|
||
| * Let :math:`[t^\ast]\to[t_0^\ast]` be the :ref:`tag type <syntax-tagtype>` |tagtype|. | ||
|
|
||
| * Assert: due to :ref:`validation <valid-externval-tag>` the type sequence :math:`t_0^\ast` must be empty. |
There was a problem hiding this comment.
This isn't actually an assertion -- this rule is the very one that validates this property for results. ;)
There was a problem hiding this comment.
Doesn't the first line (L.65) do this validation?
- The :ref:
external value <syntax-externval>:math:\EVTAG~\tagaddrmust be :ref:valid <valid-externval-tag>with some :ref:external type <syntax-externtype>:math:\ETTAG~\tagtype.
There was a problem hiding this comment.
I guess that's the justification, so removing the "Assert:"
Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>
| * Let :math:`[t^\ast]\to[t_0^\ast]` be the :ref:`tag type <syntax-tagtype>` |tagtype|. | ||
|
|
||
| * Assert: due to :ref:`validation <valid-externval-tag>` the type sequence :math:`t_0^\ast` must be empty. | ||
| * Due to :ref:`validation <valid-externval-tag>` the type sequence :math:`t_0^\ast` must be empty. |
There was a problem hiding this comment.
| * Due to :ref:`validation <valid-externval-tag>` the type sequence :math:`t_0^\ast` must be empty. | |
| * The type sequence :math:`t_0^\ast` must be empty. |
It's not due to some other validation, this rule is the validation. ;)
There was a problem hiding this comment.
To expand on this, there are several layers:
- Externval-tag validity, which you referenced here, does not actually check that the referenced tag instance is valid (and this rule does not know if the store is valid).
- Tag instance validity (as part of store validity) checks that the tag type is valid.
- Tag type validity checks that the result is empty (but see below).
You can actually combine the first three bullets in this rule into one by saying something like "The extern value TAG tagaddr must be valid with some external type TAG [t^\ast]->[]." This style is already used in some of the other rules, I believe, e.g. THROWadm.
Finally, I noticed that we are currently a bit inconsistent: tag type validity requires that the result is empty, but we are simply assuming, not asserting that in various places of the prose (e.g., the validation rule for THROW). My preference for fixing this would be to not treat tag types with empty results as invalid themselves, but only enforce emptiness in the exception-related use site rules.
There was a problem hiding this comment.
Externval-tag validity, which you referenced here, does not actually check that the referenced tag instance is valid (and this rule does not know if the store is valid).
Thank you, I think I missed that point. I saw that externval-tag validation does check if the tag is valid, and I forgot that it's not aware of the store's validity.
I will implement your second suggestion to combine the first three bullets. This way it's shorter and consistent with THROWadm validation.
Finally, I noticed that we are currently a bit inconsistent: tag type validity requires that the result is empty, but we are simply assuming, not asserting that in various places of the prose (e.g., the validation rule for THROW). My preference for fixing this would be to not treat tag types with empty results as invalid themselves, but only enforce emptiness in the exception-related use site rules.
I will create a new PR to make these changes, to not mix up the conversations.
There was a problem hiding this comment.
I will implement your second suggestion to combine the first three bullets. This way it's shorter and consistent with THROWadm validation.
Done.
2 participants
Uses the "current" version of exception results, as it will be changed by #226.