From 587dafb42fe07e81ab779d987ff3bb0682da6d47 Mon Sep 17 00:00:00 2001 From: Derek Schuff Date: Thu, 16 Mar 2023 16:25:47 -0700 Subject: [PATCH 01/10] Add exceptional return to func_invoke in embedding doc This is a basic start of what we'll need to add to the embedder spec. I'm not sure if we also need a way to allow exceptions to bubble from the embedder into wasm ; I don't see any reference to what happens when the instance wants to call an import, so maybe not. Also the references aren't quite right, but I may need help to fix that --- document/core/appendix/embedding.rst | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index b4ad120d..c8b8a85e 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -293,14 +293,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 ~|~ \error ~|~ \exception)` +...................................................................................................... 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 result is a :ref:`throw context ` for an uncaught exception with :ref:`tag ` :math:`{\tag}` and payload :ref:`values ` :math:`{\val'}^\ast`, let :math:`\X{result}` be :math:`{tag'}`, :math:`{\val'}`. + + c. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`. 2. Return the new store paired with :math:`\X{result}`. @@ -309,6 +311,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', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\ + \F{func\_invoke}(S, a, v^\ast) &=& (S', {v}, {v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \THROW) \\ \end{array} .. note:: From 15a47cff3cf5b52390e4ae8d0a76d3effa934a5b Mon Sep 17 00:00:00 2001 From: Derek Schuff Date: Mon, 27 Mar 2023 10:27:01 -0700 Subject: [PATCH 02/10] review comments --- document/core/Makefile | 4 ++-- document/core/appendix/embedding.rst | 17 +++++++++++++++-- document/core/util/macros.def | 2 ++ 3 files changed, 19 insertions(+), 4 deletions(-) diff --git a/document/core/Makefile b/document/core/Makefile index 3ff1a87c..3cd7c947 100644 --- a/document/core/Makefile +++ b/document/core/Makefile @@ -136,13 +136,13 @@ singlehtml: bikeshed: $(SPHINXBUILD) -b singlehtml -c util/bikeshed \ $(ALLSPHINXOPTS) $(BUILDDIR)/bikeshed_singlehtml - python util/bikeshed_fixup.py $(BUILDDIR)/bikeshed_singlehtml/index.html \ + python3 util/bikeshed_fixup.py $(BUILDDIR)/bikeshed_singlehtml/index.html \ >$(BUILDDIR)/bikeshed_singlehtml/index_fixed.html mkdir -p $(BUILDDIR)/bikeshed_mathjax/ bikeshed spec index.bs $(BUILDDIR)/bikeshed_mathjax/index.html mkdir -p $(BUILDDIR)/html/bikeshed/ (cd util/katex/ && yarn && yarn build && npm install --only=prod) - python util/mathjax2katex.py $(BUILDDIR)/bikeshed_mathjax/index.html \ + python3 util/mathjax2katex.py $(BUILDDIR)/bikeshed_mathjax/index.html \ >$(BUILDDIR)/html/bikeshed/index.html mkdir -p $(BUILDDIR)/html/bikeshed/katex/dist/ cp -r util/katex/dist/* $(BUILDDIR)/html/bikeshed/katex/dist/ diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index c8b8a85e..11a47547 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -43,6 +43,19 @@ In addition to the error conditions specified explicitly in this section, implem Implementations can refine it to carry suitable classifications and diagnostic messages. +.. _embed-exception: + +Exceptions +~~~~~~~~~~ + +Invoke operations may throw or propagate exceptions, indicated by an auxiliary syntactic class: + +.. math:: + \begin{array}{llllll} + \production{exception} & \exception &::=& \ETHROW & exnaddr & val^\ast \\ + \end{array} + + Pre- and Post-Conditions ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -300,7 +313,7 @@ Functions a. If it succeeds with :ref:`values ` :math:`{\val'}^\ast` as results, then let :math:`\X{result}` be :math:`{\val'}^\ast`. - b. Else if the result is a :ref:`throw context ` for an uncaught exception with :ref:`tag ` :math:`{\tag}` and payload :ref:`values ` :math:`{\val'}^\ast`, let :math:`\X{result}` be :math:`{tag'}`, :math:`{\val'}`. + b. Else if the outcome is an exception with :ref:`tag ` :math:`\tagaddr` and payload :ref:`values ` :math:`{\val'}^\ast`, let :math:`\X{result}` be :math:`\ETHROW~\tagaddr~{\val'}^\ast`. c. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`. @@ -310,8 +323,8 @@ 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'~{v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \XT[(\THROWadm~a')]) \\ \F{func\_invoke}(S, a, v^\ast) &=& (S', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\ - \F{func\_invoke}(S, a, v^\ast) &=& (S', {v}, {v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \THROW) \\ \end{array} .. note:: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index eae5e93f..df1d6368 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -1323,3 +1323,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-exception}{\X{exception}} +.. |ETHROW| mathdef:: \xref{appendix/embedding}{embed-exception}{\K{THROW}} From 904a8fbc0abb5f14e5112f154afb5a2938f6e37f Mon Sep 17 00:00:00 2001 From: Derek Schuff Date: Thu, 30 Mar 2023 16:21:12 -0700 Subject: [PATCH 03/10] swap order of error/exception in func_invoke --- document/core/appendix/embedding.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index 11a47547..c27c0232 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -306,7 +306,7 @@ Functions .. index:: invocation, value, result .. _embed-func-invoke: -:math:`\F{func\_invoke}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \error ~|~ \exception)` +: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: From ec302e1aeb76364816fd51f6e437ef27d73fba5c Mon Sep 17 00:00:00 2001 From: Derek Schuff Date: Tue, 11 Apr 2023 15:33:13 -0700 Subject: [PATCH 04/10] review suggestions --- document/core/appendix/embedding.rst | 24 +++++++++++------------- document/core/util/macros.def | 4 ++-- 2 files changed, 13 insertions(+), 15 deletions(-) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index c27c0232..d827edca 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -26,8 +26,17 @@ For numeric parameters, notation like :math:`n:\u32` is used to specify a symbol .. _embed-error: -Errors -~~~~~~ +Exceptions and Errors +~~~~~~~~~~~~~~~~~~~~~ + +Invoke operations may throw or propagate exceptions, indicated by an auxiliary syntactic class: + +.. math:: + \begin{array}{llll} + \production{exception} & \exception &::=& \ETHROW ~ \tagaddr ~ val^\ast \\ + \end{array} + +The tag instance :math:`tagaddr` identifies the :ref:`type ` of exception thrown. The values :math:`val^\ast` are the exception's payload; their types match the tag type's parameters. Failure of an interface operation is indicated by an auxiliary syntactic class: @@ -43,17 +52,6 @@ In addition to the error conditions specified explicitly in this section, implem Implementations can refine it to carry suitable classifications and diagnostic messages. -.. _embed-exception: - -Exceptions -~~~~~~~~~~ - -Invoke operations may throw or propagate exceptions, indicated by an auxiliary syntactic class: - -.. math:: - \begin{array}{llllll} - \production{exception} & \exception &::=& \ETHROW & exnaddr & val^\ast \\ - \end{array} Pre- and Post-Conditions diff --git a/document/core/util/macros.def b/document/core/util/macros.def index df1d6368..13e904d7 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -1323,5 +1323,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-exception}{\X{exception}} -.. |ETHROW| mathdef:: \xref{appendix/embedding}{embed-exception}{\K{THROW}} +.. |exception| mathdef:: \xref{appendix/embedding}{embed-error}{\X{exception}} +.. |ETHROW| mathdef:: \xref{appendix/embedding}{embed-error}{\K{THROW}} From fdf1b7c2a9553fec8734b3c15199a16b0cb47ca8 Mon Sep 17 00:00:00 2001 From: Derek Schuff Date: Wed, 3 May 2023 17:35:56 -0700 Subject: [PATCH 05/10] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- document/core/appendix/embedding.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index d827edca..d11da93b 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -29,16 +29,16 @@ For numeric parameters, notation like :math:`n:\u32` is used to specify a symbol Exceptions and Errors ~~~~~~~~~~~~~~~~~~~~~ -Invoke operations may throw or propagate exceptions, 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 ~ \tagaddr ~ val^\ast \\ \end{array} -The tag instance :math:`tagaddr` identifies the :ref:`type ` of exception thrown. The values :math:`val^\ast` are the exception's payload; their types match the tag type's parameters. +The tag instance :math:`tagaddr` identifies the exception thrown. The values :math:`val^\ast` are the exception's payload; their types match the tag type's parameters. -Failure of an interface operation is indicated by an auxiliary syntactic class: +Failure of an interface operation is also indicated by an auxiliary syntactic class: .. math:: \begin{array}{llll} From f57cdb8cc4c5e374cc5ae59e9de2eee38c843d80 Mon Sep 17 00:00:00 2001 From: Derek Schuff Date: Thu, 21 Mar 2024 17:30:31 -0700 Subject: [PATCH 06/10] add exception allocation --- document/core/appendix/embedding.rst | 38 ++++++++++++++++++++++++++++ document/core/exec/instructions.rst | 16 +++++------- document/core/exec/modules.rst | 28 +++++++++++++++++++- document/core/util/macros.def | 1 + 4 files changed, 73 insertions(+), 10 deletions(-) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index 5413799f..13dd1ed3 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -576,6 +576,44 @@ 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-exception-alloc: + +:math:`\F{exception\_alloc}(\store, \tagaddr, \val) : (\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{exception\_alloc}(S, \X{gt}, v) &=& (S', \X{a}) && (\iff \allocglobal(S, \X{gt}, v) = S', \X{a}) \\ + \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 5d19010c..5ee4a605 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..4f1335f1 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, \GIVALUE~\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 ca40cd52..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}} From ccbee0f7e15d277067fc81fdbad5100eb91c253e Mon Sep 17 00:00:00 2001 From: Derek Schuff Date: Fri, 22 Mar 2024 10:42:43 -0700 Subject: [PATCH 07/10] udpate for exnref --- document/core/appendix/embedding.rst | 4 ++-- document/core/exec/modules.rst | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index 13dd1ed3..7f75fb76 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -311,7 +311,7 @@ Functions a. If it succeeds with :ref:`values ` :math:`{\val'}^\ast` as results, then let :math:`\X{result}` be :math:`{\val'}^\ast`. - b. Else if the outcome is an exception with :ref:`tag ` :math:`\tagaddr` and payload :ref:`values ` :math:`{\val'}^\ast`, let :math:`\X{result}` be :math:`\ETHROW~\tagaddr~{\val'}^\ast`. + 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:`\exnaddr` c. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`. @@ -321,7 +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'~{v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \XT[(\THROWadm~a')]) \\ + \F{func\_invoke}(S, a, v^\ast) &=& (S', \ETHROW~a'~{v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \XT[(\REFEXNADDR~\exnaddr)~\THROWREF] \\ \F{func\_invoke}(S, a, v^\ast) &=& (S', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\ \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 4f1335f1..b2ebe665 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -348,7 +348,7 @@ New instances of :ref:`functions `, :ref:`tables ` in :math:`S`. -3. Let :math:`\exninst` be the :ref:`exception instance ` :math:`\{ \EITAG~ta, \EIFIELDS~\val^\ast \}`. +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`. From 4d08a587f5cb8654c2347027cb1a6a3940c554d5 Mon Sep 17 00:00:00 2001 From: Derek Schuff Date: Fri, 29 Mar 2024 10:29:10 -0700 Subject: [PATCH 08/10] apply all suggestions other than exn_read --- document/core/appendix/embedding.rst | 14 +++++++------- document/core/exec/modules.rst | 4 ++-- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index 7f75fb76..65723a47 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -33,10 +33,10 @@ Invoking an exported function may throw or propagate exceptions, expressed by an .. math:: \begin{array}{llll} - \production{exception} & \exception &::=& \ETHROW ~ \tagaddr ~ val^\ast \\ + \production{exception} & \exception &::=& \ETHROW ~ \exnaddr \\ \end{array} -The tag instance :math:`tagaddr` identifies the exception thrown. The values :math:`val^\ast` are the exception's payload; their types match the tag type's parameters. +The exception instance :math:`exnaddr` identifies the exception thrown. Failure of an interface operation is also indicated by an auxiliary syntactic class: @@ -311,7 +311,7 @@ Functions a. If it succeeds with :ref:`values ` :math:`{\val'}^\ast` as results, then let :math:`\X{result}` be :math:`{\val'}^\ast`. - 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:`\exnaddr` + 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`. @@ -321,7 +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'~{v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \XT[(\REFEXNADDR~\exnaddr)~\THROWREF] \\ + \F{func\_invoke}(S, a, v^\ast) &=& (S', \ETHROW~a') && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \XT[(\REFEXNADDR~\exnaddr)~\THROWREF] \\ \F{func\_invoke}(S, a, v^\ast) &=& (S', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\ \end{array} @@ -597,9 +597,9 @@ Tags Exceptions ~~~~~~~~~~ -.. _embed-exception-alloc: +.. _embed-exn-alloc: -:math:`\F{exception\_alloc}(\store, \tagaddr, \val) : (\store, \exnaddr)` +:math:`\F{exn\_alloc}(\store, \tagaddr, \val^\ast) : (\store, \exnaddr)` ............................................................................ 1. Pre-condition: :math:`\tagaddr` is an allocated :ref:`tag address `. @@ -610,7 +610,7 @@ Exceptions .. math:: \begin{array}{lclll} - \F{exception\_alloc}(S, \X{gt}, v) &=& (S', \X{a}) && (\iff \allocglobal(S, \X{gt}, v) = S', \X{a}) \\ + \F{exn\_alloc}(S, \tagaddr, \val^\ast) &=& (S', a) && (\iff \allocexn(S, \tagaddr, \val^\ast) = S', a) \\ \end{array} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index b2ebe665..2a52bc96 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -356,10 +356,10 @@ New instances of :ref:`functions `, :ref:`tables Date: Fri, 29 Mar 2024 10:50:20 -0700 Subject: [PATCH 09/10] add exn_read --- document/core/appendix/embedding.rst | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index 65723a47..4c6791ae 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -614,6 +614,21 @@ Exceptions \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: From afa0c7a8e0201a155322a320f6f4f7d114bd80c7 Mon Sep 17 00:00:00 2001 From: Derek Schuff Date: Tue, 2 Apr 2024 11:17:09 -0700 Subject: [PATCH 10/10] apply suggestions --- document/core/appendix/embedding.rst | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index 4c6791ae..173f60a2 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -36,7 +36,7 @@ Invoking an exported function may throw or propagate exceptions, expressed by an \production{exception} & \exception &::=& \ETHROW ~ \exnaddr \\ \end{array} -The exception instance :math:`exnaddr` identifies the exception thrown. +The exception address :math:`exnaddr` identifies the exception thrown. Failure of an interface operation is also indicated by an auxiliary syntactic class: @@ -321,7 +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~\exnaddr)~\THROWREF] \\ + \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} @@ -579,7 +579,7 @@ Tags .. _embed-tag-type: :math:`\F{tag\_type}(\store, \tagaddr) : \tagtype` -........................................................ +.................................................. 1. Return :math:`S.\STAGS[a].\TAGITYPE`. @@ -600,7 +600,7 @@ 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 `. @@ -617,7 +617,7 @@ Exceptions .. _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]`.