Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add exceptional return to func_invoke in embedding doc #268

Merged
merged 11 commits into from
Apr 2, 2024
79 changes: 73 additions & 6 deletions document/core/appendix/embedding.rst
Original file line number Diff line number Diff line change
Expand Up @@ -26,10 +26,19 @@ For numeric parameters, notation like :math:`n:\u32` is used to specify a symbol

.. _embed-error:

Errors
~~~~~~
Exceptions and Errors
~~~~~~~~~~~~~~~~~~~~~

Failure of an interface operation is indicated by an auxiliary syntactic class:
Invoking an exported function may throw or propagate exceptions, expressed by an auxiliary syntactic class:
dschuff marked this conversation as resolved.
Show resolved Hide resolved

.. math::
\begin{array}{llll}
\production{exception} & \exception &::=& \ETHROW ~ \exnaddr \\
\end{array}

The exception address :math:`exnaddr` identifies the exception thrown.

Failure of an interface operation is also indicated by an auxiliary syntactic class:

.. math::
\begin{array}{llll}
Expand All @@ -43,6 +52,8 @@ In addition to the error conditions specified explicitly in this section, implem
Implementations can refine it to carry suitable classifications and diagnostic messages.



dschuff marked this conversation as resolved.
Show resolved Hide resolved

Pre- and Post-Conditions
~~~~~~~~~~~~~~~~~~~~~~~~

Expand Down Expand Up @@ -293,21 +304,24 @@ Functions
.. index:: invocation, value, result
.. _embed-func-invoke:

:math:`\F{func\_invoke}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \error)`
........................................................................................
:math:`\F{func\_invoke}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \exception ~|~ \error)`
......................................................................................................

1. Try :ref:`invoking <exec-invocation>` the function :math:`\funcaddr` in :math:`\store` with :ref:`values <syntax-val>` :math:`\val^\ast` as arguments:

a. If it succeeds with :ref:`values <syntax-val>` :math:`{\val'}^\ast` as results, then let :math:`\X{result}` be :math:`{\val'}^\ast`.

b. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`.
b. Else if the outcome is an exception with a thrown :ref:`exception <exec-throw_ref>` :math:`\REFEXNADDR~\exnaddr` as the result, then let :math:`\X{result}` be :math:`\ETHROW~\exnaddr`

c. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`.

2. Return the new store paired with :math:`\X{result}`.

.. math::
~ \\
\begin{array}{lclll}
\F{func\_invoke}(S, a, v^\ast) &=& (S', {v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; {v'}^\ast) \\
\F{func\_invoke}(S, a, v^\ast) &=& (S', \ETHROW~a') && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \XT[(\REFEXNADDR~a')~\THROWREF] \\
\F{func\_invoke}(S, a, v^\ast) &=& (S', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\
\end{array}

Expand Down Expand Up @@ -562,6 +576,59 @@ Tags
\end{array}


.. _embed-tag-type:

:math:`\F{tag\_type}(\store, \tagaddr) : \tagtype`
..................................................

1. Return :math:`S.\STAGS[a].\TAGITYPE`.

2. Post-condition: the returned :ref:`tag type <syntax-tagtype>` is :ref:`valid <valid-tagtype>`.

.. math::
\begin{array}{lclll}
\F{tag\_type}(S, a) &=& S.\STAGS[a].\TAGITYPE \\
\end{array}


.. index:: exception, exception address, store, exception instance, exception type
.. _embed-exception:

Exceptions
dschuff marked this conversation as resolved.
Show resolved Hide resolved
~~~~~~~~~~

.. _embed-exn-alloc:

:math:`\F{exn\_alloc}(\store, \tagaddr, \val^\ast) : (\store, \exnaddr)`
........................................................................

1. Pre-condition: :math:`\tagaddr` is an allocated :ref:`tag address <syntax-tagaddr>`.

2. Let :math:`\exnaddr` be the result of :ref:`allocating an exception <alloc-exception>` in :math:`\store` with :ref:`tag address <syntax-tagaddr>` :math:`\tagaddr` and initialization values :math:`\val^\ast`.

3. Return the new store paired with :math:`\exnaddr`.

.. math::
\begin{array}{lclll}
\F{exn\_alloc}(S, \tagaddr, \val^\ast) &=& (S', a) && (\iff \allocexn(S, \tagaddr, \val^\ast) = S', a) \\
\end{array}


.. _embed-exn-read:

:math:`\F{exn\_read}(\store, \exnaddr) : (\tagaddr, \val^\ast)`
...............................................................

1. Let :math:`\X{ei}` be the :ref:`exception instance <syntax-exninst>` :math:`\store.\SEXNS[\exnaddr]`.

2. Return the :ref:`tag address <syntax-tagaddr>` :math:`\X{ei}.\EITAG~\tagaddr` paired with :ref:`values <syntax-val>` :math:`\X{ei}.\EIFIELDS~\val^\ast`.

.. math::
\begin{array}{lcll}
\F{exn\_read}(S, a) &=& (a', v^\ast) \\
\end{array}


.. index:: global, global address, store, global instance, global type, value
.. _embed-global:

Expand Down
16 changes: 7 additions & 9 deletions document/core/exec/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -2719,27 +2719,25 @@ Control Instructions

2. Assert: due to :ref:`validation <valid-throw>`, :math:`F.\AMODULE.\MITAGS[x]` exists.

3. Let :math:`a` be the :ref:`tag address <syntax-tagaddr>` :math:`F.\AMODULE.\MITAGS[x]`.
3. Let :math:`ta` be the :ref:`tag address <syntax-tagaddr>` :math:`F.\AMODULE.\MITAGS[x]`.

4. Assert: due to :ref:`validation <valid-throw>`, :math:`S.\STAGS[a]` exists.
4. Assert: due to :ref:`validation <valid-throw>`, :math:`S.\STAGS[ta]` exists.

5. Let :math:`\X{ti}` be the :ref:`tag instance <syntax-taginst>` :math:`S.\STAGS[a]`.
5. Let :math:`\X{ti}` be the :ref:`tag instance <syntax-taginst>` :math:`S.\STAGS[ta]`.

6. Let :math:`[t^n] \toF [{t'}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`\X{ti}.\TAGITYPE`.

7. Assert: due to :ref:`validation <valid-throw>`, there are at least :math:`n` values on the top of the stack.

8. Pop the :math:`n` values :math:`\val^n` from the stack.

9. Let :math:`\X{exn}` be the :ref:`exception instance <syntax-exninst>` :math:`\{ \EITAG~a, \EIFIELDS~\val^n \}`.
9. Let :math:`\X{ea}` be the :ref:`exception address <syntax-exnaddr>` resulting from :ref:`allocating <alloc-exception>` an exception instance with tag address :math:`ta` and initializer values :math:`\val^n`.

10. Let :math:`\X{ea}` be the length of :math:`S.\SEXNS`.
10. Let :math:`\X{exn}` be :math:`S.\SEXNS[ea]`

11. Append :math:`\X{exn}` to :math:`S.\SEXNS`.
11. Push the value :math:`\REFEXNADDR~\X{ea}` to the stack.

12. Push the value :math:`\REFEXNADDR~\X{ea}` to the stack.

13. Execute the instruction |THROWREF|.
12. Execute the instruction |THROWREF|.

.. math::
~\\[-1ex]
Expand Down
28 changes: 27 additions & 1 deletion document/core/exec/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ The following auxiliary typing rules specify this typing relation relative to a
Allocation
~~~~~~~~~~

New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tableinst>`, :ref:`memories <syntax-meminst>`, :ref:`tags <syntax-taginst>`, and :ref:`globals <syntax-globalinst>` are *allocated* in a :ref:`store <syntax-store>` :math:`S`, as defined by the following auxiliary functions.
New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tableinst>`, :ref:`memories <syntax-meminst>`, :ref:`tags <syntax-taginst>`, :ref:`exceptions <syntax-exninst>`, and :ref:`globals <syntax-globalinst>` are *allocated* in a :ref:`store <syntax-store>` :math:`S`, as defined by the following auxiliary functions.


.. index:: function, function instance, function address, module instance, function type
Expand Down Expand Up @@ -338,6 +338,32 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
\end{array}


.. index:: exception, exception instance, exception address, tag address
.. _alloc-exception:

:ref:`Exceptions <syntax-exninst>`
..................................

1. Let :math:`ta` be the :ref:`tag address <syntax-tagaddr>` associated with the exception to allocate and :math:`\EIFIELDS~\val^\ast` be the values to initialize the exception with.

2. Let :math:`a` be the first free :ref:`exception address <syntax-exnaddr>` in :math:`S`.

3. Let :math:`\exninst` be the :ref:`exception instance <syntax-exninst>` :math:`\{ \EITAG~ta, \EIFIELDS~\val^\ast \}`.

4. Append :math:`\exninst` to the |SEXNS| of :math:`S`.

5. Return :math:`a`.

.. math::
\begin{array}{rlll}
\allocexn(S, \tagaddr, \val^\ast) &=& S', \exnaddr \\[1ex]
\mbox{where:} \hfill \\
\exnaddr &=& |S.\SEXNS| \\
\exninst &=& \{ \EITAG~\tagaddr, \EIFIELDS~\val^\ast \} \\
S' &=& S \compose \{\SEXNS~\exninst\} \\
\end{array}


.. index:: global, global instance, global address, global type, value type, mutability, value
.. _alloc-global:

Expand Down
3 changes: 3 additions & 0 deletions document/core/util/macros.def
Original file line number Diff line number Diff line change
Expand Up @@ -981,6 +981,7 @@
.. |alloctable| mathdef:: \xref{exec/modules}{alloc-table}{\F{alloctable}}
.. |allocmem| mathdef:: \xref{exec/modules}{alloc-mem}{\F{allocmem}}
.. |alloctag| mathdef:: \xref{exec/modules}{alloc-tag}{\F{alloctag}}
.. |allocexn| mathdef:: \xref{exec/modules}{alloc-exception}{\F{allocexn}}
.. |allocglobal| mathdef:: \xref{exec/modules}{alloc-global}{\F{allocglobal}}
.. |allocelem| mathdef:: \xref{exec/modules}{alloc-elem}{\F{allocelem}}
.. |allocdata| mathdef:: \xref{exec/modules}{alloc-data}{\F{allocdata}}
Expand Down Expand Up @@ -1335,3 +1336,5 @@

.. |error| mathdef:: \xref{appendix/embedding}{embed-error}{\X{error}}
.. |ERROR| mathdef:: \xref{appendix/embedding}{embed-error}{\K{error}}
.. |exception| mathdef:: \xref{appendix/embedding}{embed-error}{\X{exception}}
.. |ETHROW| mathdef:: \xref{appendix/embedding}{embed-error}{\K{THROW}}
Loading