From 153ca9a90ef27d427f1ce3d2b5aa1e6e2694f48c Mon Sep 17 00:00:00 2001 From: Derek Schuff Date: Tue, 2 Apr 2024 11:26:50 -0700 Subject: [PATCH] Add exceptional return to func_invoke in embedding doc (#268) Embedding: * Adds an auxiliary syntactic class to represent exception throwing/propagation * Allows `func_invoke` to propagate exceptions * Adds `tag_type` and `exn_alloc` to the embedding interface core/exec: * Refactors exception allocation into `alloc-exception` in modules.rst to expose it to the embedder --- document/core/appendix/embedding.rst | 79 +++++++++++++++++++++++++--- document/core/exec/instructions.rst | 16 +++--- document/core/exec/modules.rst | 28 +++++++++- document/core/util/macros.def | 3 ++ 4 files changed, 110 insertions(+), 16 deletions(-) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index 380794fe..173f60a2 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -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: + +.. 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} @@ -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. + + Pre- and Post-Conditions ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -293,14 +304,16 @@ 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 ` the function :math:`\funcaddr` in :math:`\store` with :ref:`values ` :math:`\val^\ast` as arguments: a. If it succeeds with :ref:`values ` :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 ` :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}`. @@ -308,6 +321,7 @@ Functions ~ \\ \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} @@ -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 ` is :ref:`valid `. + +.. 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 +~~~~~~~~~~ + +.. _embed-exn-alloc: + +:math:`\F{exn\_alloc}(\store, \tagaddr, \val^\ast) : (\store, \exnaddr)` +........................................................................ + +1. Pre-condition: :math:`\tagaddr` is an allocated :ref:`tag address `. + +2. Let :math:`\exnaddr` be the result of :ref:`allocating an exception ` in :math:`\store` with :ref:`tag address ` :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 ` :math:`\store.\SEXNS[\exnaddr]`. + +2. Return the :ref:`tag address ` :math:`\X{ei}.\EITAG~\tagaddr` paired with :ref:`values ` :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: diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 175dc07c..5d1b766b 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -2719,11 +2719,11 @@ Control Instructions 2. Assert: due to :ref:`validation `, :math:`F.\AMODULE.\MITAGS[x]` exists. -3. Let :math:`a` be the :ref:`tag address ` :math:`F.\AMODULE.\MITAGS[x]`. +3. Let :math:`ta` be the :ref:`tag address ` :math:`F.\AMODULE.\MITAGS[x]`. -4. Assert: due to :ref:`validation `, :math:`S.\STAGS[a]` exists. +4. Assert: due to :ref:`validation `, :math:`S.\STAGS[ta]` exists. -5. Let :math:`\X{ti}` be the :ref:`tag instance ` :math:`S.\STAGS[a]`. +5. Let :math:`\X{ti}` be the :ref:`tag instance ` :math:`S.\STAGS[ta]`. 6. Let :math:`[t^n] \toF [{t'}^\ast]` be the :ref:`tag type ` :math:`\X{ti}.\TAGITYPE`. @@ -2731,15 +2731,13 @@ Control Instructions 8. Pop the :math:`n` values :math:`\val^n` from the stack. -9. Let :math:`\X{exn}` be the :ref:`exception instance ` :math:`\{ \EITAG~a, \EIFIELDS~\val^n \}`. +9. Let :math:`\X{ea}` be the :ref:`exception address ` resulting from :ref:`allocating ` 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] diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index a43f55e9..2a52bc96 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -190,7 +190,7 @@ The following auxiliary typing rules specify this typing relation relative to a Allocation ~~~~~~~~~~ -New instances of :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`tags `, and :ref:`globals ` are *allocated* in a :ref:`store ` :math:`S`, as defined by the following auxiliary functions. +New instances of :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`tags `, :ref:`exceptions `, and :ref:`globals ` are *allocated* in a :ref:`store ` :math:`S`, as defined by the following auxiliary functions. .. index:: function, function instance, function address, module instance, function type @@ -338,6 +338,32 @@ New instances of :ref:`functions `, :ref:`tables ` +.................................. + +1. Let :math:`ta` be the :ref:`tag address ` 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 ` in :math:`S`. + +3. Let :math:`\exninst` be the :ref:`exception instance ` :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: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index f2e71072..ed0da332 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -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}} @@ -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}}