Merge remote-tracking branch 'exn/main' into wasm-3.0

Author: rossberg

.github/workflows/ci-spec.yml

@@ -90,7 +90,7 @@ jobs:
           name: code-metadata-rendered
           path: document/metadata/code/_build/html
 
-  build-legacy-exceptions-spec:
+  build-legacy-exceptions-core-spec:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo
@@ -102,16 +102,31 @@ jobs:
       - name: Setup Sphinx
         run: pip install six && pip install sphinx==5.1.0
       - name: Build main spec
-        run: cd document/legacy/exceptions && make main
+        run: cd document/legacy/exceptions/core && make main
       - name: Upload artifact
         uses: actions/upload-artifact@v2
         with:
-          name: legacy-exceptions-rendered
-          path: document/legacy/exceptions/_build/html
+          name: legacy-exceptions-core-rendered
+          path: document/legacy/exceptions/core/_build/html
+
+  build-legacy-exceptions-js-api-spec:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repo
+        uses: actions/checkout@v2
+      - name: Setup Bikeshed
+        run: pip install bikeshed && bikeshed update
+      - name: Run Bikeshed
+        run: bikeshed spec "document/legacy/exceptions/js-api/index.bs" "document/legacy/exceptions/js-api/index.html"
+      - name: Upload artifact
+        uses: actions/upload-artifact@v2
+        with:
+          name: legacy-exceptions-js-api-rendered
+          path: document/legacy/exceptions/js-api/index.html
 
   publish-spec:
     runs-on: ubuntu-latest
-    needs: [build-core-spec, build-js-api-spec, build-web-api-spec, build-code-metadata-spec, build-legacy-exceptions-spec]
+    needs: [build-core-spec, build-js-api-spec, build-web-api-spec, build-code-metadata-spec, build-legacy-exceptions-core-spec, build-legacy-exceptions-js-api-spec]
     steps:
       - name: Checkout repo
         uses: actions/checkout@v2
@@ -137,11 +152,16 @@ jobs:
         with:
           name: code-metadata-rendered
           path: _output/metadata/code
-      - name: Download legacy exceptions spec artifact
+      - name: Download legacy exceptions core spec artifact
+        uses: actions/download-artifact@v2
+        with:
+          name: legacy-exceptions-core-rendered
+          path: _output/legacy/exceptions/core
+      - name: Download legacy exceptions JS API spec artifact
         uses: actions/download-artifact@v2
         with:
-          name: legacy-exceptions-rendered
-          path: _output/legacy/exceptions
+          name: legacy-exceptions-js-api-rendered
+          path: _output/legacy/exceptions/js-api
       - name: Publish to GitHub Pages
         if: github.ref == 'refs/heads/main'
         uses: peaceiris/actions-gh-pages@v3

document/core/appendix/embedding.rst

@@ -39,10 +39,19 @@ Interface operation that are predicates return Boolean values:
 
 .. _embed-error:
 
-Errors
-~~~~~~
+Exceptions and Errors
+~~~~~~~~~~~~~~~~~~~~~
+
+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}
 
-Failure of an interface operation is indicated by an auxiliary syntactic class:
+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}
@@ -56,6 +65,8 @@ In addition to the error conditions specified explicitly in this section, such a
    Implementations can refine it to carry suitable classifications and diagnostic messages.
 
 
+
+
 Pre- and Post-Conditions
 ~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -307,22 +318,25 @@ 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', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \result) \\
+   \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}
 
 .. note::
@@ -576,6 +590,77 @@ 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
+~~~~~~~~~~
+
+.. _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 instance <syntax-exninst>` 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}{lcll}
+   \F{exn\_alloc}(S, \tagaddr, \val^\ast) &=& (S \compose \{\SEXNS~\exninst\}, |S.\SEXNS|) &
+     (\iff \exninst = \{\EITAG~\tagaddr, \EIFIELDS~\val^\ast\} \\
+   \end{array}
+
+
+.. _embed-exn-tag:
+
+:math:`\F{exn\_tag}(\store, \exnaddr) : \tagaddr`
+.................................................
+
+1. Let :math:`\exninst` be the :ref:`exception instance <syntax-exninst>` :math:`\store.\SEXNS[\exnaddr]`.
+
+2. Return the :ref:`tag address <syntax-tagaddr>` :math:`\exninst.\EITAG`.
+
+.. math::
+   \begin{array}{lcll}
+   \F{exn\_tag}(S, a) &=& \exninst.\EITAG &
+     (\iff \exninst = S.\SEXNS[a]) \\
+   \end{array}
+
+
+.. _embed-exn-read:
+
+:math:`\F{exn\_read}(\store, \exnaddr) : \val^\ast`
+...................................................
+
+1. Let :math:`\exninst` be the :ref:`exception instance <syntax-exninst>` :math:`\store.\SEXNS[\exnaddr]`.
+
+2. Return the :ref:`values <syntax-val>` :math:`\exninst.\EIFIELDS`.
+
+.. math::
+   \begin{array}{lcll}
+   \F{exn\_read}(S, a) &=& \exninst.\EIFIELDS &
+     (\iff \exninst = S.\SEXNS[a]) \\
+   \end{array}
+
+
 .. index:: global, global address, store, global instance, global type, value
 .. _embed-global:
 

document/core/binary/modules.rst

@@ -181,7 +181,7 @@ It decodes into a vector of :ref:`imports <syntax-import>` that represent the |M
      \hex{01}~~\X{tt}{:}\Btabletype &\Rightarrow& \IDTABLE~\X{tt} \\ &&|&
      \hex{02}~~\X{mt}{:}\Bmemtype &\Rightarrow& \IDMEM~\X{mt} \\ &&|&
      \hex{03}~~\X{gt}{:}\Bglobaltype &\Rightarrow& \IDGLOBAL~\X{gt} \\ &&|&
-     \hex{04}~~\X{tt}{:}\Btag &\Rightarrow& \IDTAG~\X{tt} \\
+     \hex{04}~~\X{tt}{:}\Btagtype &\Rightarrow& \IDTAG~\X{tt} \\
    \end{array}
 
 

document/core/exec/instructions.rst

@@ -4030,27 +4030,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]
@@ -4114,13 +4112,13 @@ Control Instructions
 
     a. Let :math:`\catch_1` be the first :ref:`catch clause <syntax-catch>` in :math:`\catch^\ast` and :math:`{\catch'}^\ast` the remaining clauses.
 
-    b. If :math:`\catch_1` is of the form :math:`\CATCH~x~l` and the :ref:`exception address <syntax-exnaddr>` :math:`a` equals :math:`F.\AMODULE.\MITAGS[x]`, then:
+    b. If :math:`\catch_1` is of the form :math:`\CATCH~x~l` and the :ref:`tag address <syntax-tagaddr>` :math:`a` equals :math:`F.\AMODULE.\MITAGS[x]`, then:
 
        i. Push the values :math:`\X{exn}.\EIFIELDS` to the stack.
 
        ii. Execute the instruction :math:`\BR~l`.
 
-    c. Else if :math:`\catch_1` is of the form :math:`\CATCHREF~x~l` and the :ref:`exception address <syntax-exnaddr>` :math:`a` equals :math:`F.\AMODULE.\MITAGS[x]`, then:
+    c. Else if :math:`\catch_1` is of the form :math:`\CATCHREF~x~l` and the :ref:`tag address <syntax-tagaddr>` :math:`a` equals :math:`F.\AMODULE.\MITAGS[x]`, then:
 
        i. Push the values :math:`\X{exn}.\EIFIELDS` to the stack.
 

document/core/exec/modules.rst

@@ -170,6 +170,32 @@ are *allocated* in a :ref:`store <syntax-store>` :math:`S`, as defined by the fo
    \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:
 

document/core/util/macros.def

@@ -1202,6 +1202,8 @@
 .. |allocdata| mathdef:: \xref{exec/modules}{alloc-data}{\F{allocdata}}
 .. |allocmodule| mathdef:: \xref{exec/modules}{alloc-module}{\F{allocmodule}}
 
+.. |allocexn| mathdef:: \xref{exec/modules}{alloc-exception}{\F{allocexn}}
+
 .. |growtable| mathdef:: \xref{exec/modules}{grow-table}{\F{growtable}}
 .. |growmem| mathdef:: \xref{exec/modules}{grow-mem}{\F{growmem}}
 
@@ -1627,3 +1629,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}}

document/index.html

@@ -82,8 +82,17 @@ <h3>Legacy Extensions</h3>
   <ul>
     <li><p><b>Legacy Exception Handling</b>: defines additional instructions for exception handling that may still be available in some engines and tools, specifically web browsers.</p>
       <ul>
-        <li><a href="legacy/exceptions/">Browser version</a></li>
-        <li><a href="legacy/exceptions/_download/WebAssembly-Legacy-Exceptions.pdf">PDF version</a></li>
+        <li><p><b>Core specification</b></p>
+          <ul>
+            <li><a href="legacy/exceptions/core/">Browser version</a></li>
+            <li><a href="legacy/exceptions/core/_download/WebAssembly-Legacy-Exceptions.pdf">PDF version</a></li>
+          </ul>
+        </li>
+        <li><p><b>JavaScirpt Embedding</b></p>
+          <ul>
+            <li><a href="legacy/exceptions/js-api/">W3C version</a></li>
+          </ul>
+        </li>
       </ul>
     </li>
   </ul>