From d1bf45ac815c45ca114a5e35dc5943d1c6ed3c46 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Fri, 22 Nov 2024 10:00:07 +0100
Subject: [PATCH] Fix exception allocation

---
 document/core/exec/instructions.rst | 16 +++++++++-------
 document/core/exec/modules.rst      | 26 --------------------------
 document/core/util/macros.def       |  2 --
 3 files changed, 9 insertions(+), 35 deletions(-)

diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst
index d6a16b84a3..25eb52ab95 100644
--- a/document/core/exec/instructions.rst
+++ b/document/core/exec/instructions.rst
@@ -4226,11 +4226,11 @@ Control Instructions
 
 2. Assert: due to :ref:`validation <valid-throw>`, :math:`F.\AMODULE.\MITAGS[x]` exists.
 
-3. Let :math:`ta` be the :ref:`tag address <syntax-tagaddr>` :math:`F.\AMODULE.\MITAGS[x]`.
+3. Let :math:`\X{ta}` be the :ref:`tag address <syntax-tagaddr>` :math:`F.\AMODULE.\MITAGS[x]`.
 
-4. Assert: due to :ref:`validation <valid-throw>`, :math:`S.\STAGS[ta]` exists.
+4. Assert: due to :ref:`validation <valid-throw>`, :math:`S.\STAGS[\X{ta}]` exists.
 
-5. Let :math:`\X{ti}` be the :ref:`tag instance <syntax-taginst>` :math:`S.\STAGS[ta]`.
+5. Let :math:`\X{ti}` be the :ref:`tag instance <syntax-taginst>` :math:`S.\STAGS[\X{ta}]`.
 
 6. Let :math:`[t^n] \toF [{t'}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`\X{ti}.\TAGITYPE`.
 
@@ -4238,13 +4238,15 @@ Control Instructions
 
 8. Pop the :math:`n` values :math:`\val^n` from the stack.
 
-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`.
+9. Let :math:`\X{exn}` be the :ref:`exception instance <syntax-exninst>` :math:`\{\EITAG~\X{ta}, \EIFIELDS~\val^n\}`.
 
-10. Let :math:`\X{exn}` be :math:`S.\SEXNS[ea]`
+10. Let :math:`\X{ea}` be the length of :math:`S.\SEXNS`.
 
-11. Push the value :math:`\REFEXNADDR~\X{ea}` to the stack.
+11. Append :math:`\X{exn}` to :math:`S.\SEXNS`.
 
-12. Execute the instruction |THROWREF|.
+12. Push the value :math:`\REFEXNADDR~\X{ea}` to the stack.
+
+13. Execute the instruction |THROWREF|.
 
 .. math::
    ~\\[-1ex]
diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst
index c9618231e6..be2b62b952 100644
--- a/document/core/exec/modules.rst
+++ b/document/core/exec/modules.rst
@@ -170,32 +170,6 @@ 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:
 
diff --git a/document/core/util/macros.def b/document/core/util/macros.def
index 2a45188b15..92f4e5490d 100644
--- a/document/core/util/macros.def
+++ b/document/core/util/macros.def
@@ -1229,8 +1229,6 @@
 .. |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}}