Update formal spec to (partially) implement the current (3rd) EH prop…

…osal.

In particular:

- exnref is removed from reference types
- REFEXNADDR is removed from administrative instructions
- exn and exception are renamed to tag (also when part of a word/macro)
- renamed EITYPE to TAGITYPE, ETYPE to TAGTYPE,
- changed variable names for tags from "et" to "tt" or "tagt", "iet" to "itagt"
- adjusted indexing where needed
- CATCHN is renamed to CATCHadm and its syntax and rules are adjusted
- added CAUGHTadm and DELEGATEadm, both with syntax and rules
- adjusted syntax and rules for TRY-CATCH, using \catchtype in binary and syntax, in order to describe TRY-CATCH compactly
- added syntax and rules for TRY-DELEGATE
- adjusted syntax and rules for RETHROW
- removed dependencies "bulk instructions" and "reference types" from Release
- adjusted/added validation example of control frame with opcode catch/catch_all resp.
- adjusted "Folded Instructions" for TRY-CATCH (didn't add folded TRY-DELEGATE)
- in several places added or adjusted prose, or added TODO items to add prose later

In particular there are still the following items marked as
TODO:

[] to add prose for typing rule of DELEGATEadm
[] to add prose for execution rules of TRY-CATCH, TRY-DELEGATE, and RETHROW
[] to finish prose for "Throwing an exception" (exec/instructions.rst)
[] to add EXCEPTION result value, signifying throwing an exception to the embedder
[] to adjust block contexts by adding CATCHadm, DELEGATEadm, and CAUGHTadm
[] to change labels to include the label type "catch" (in section "Contexts")
[] to add prose for validation rules of TRY-DELEGATE and RETHROW

document/core/appendix/algorithm.rst

@@ -25,13 +25,13 @@ Types are representable as an enumeration.
 
 .. code-block:: pseudo
 
-   type val_type = I32 | I64 | F32 | F64 | Funcref | Exnref | Externref
+   type val_type = I32 | I64 | F32 | F64 | Funcref | Externref
 
    func is_num(t : val_type | Unknown) : bool =
      return t = I32 || t = I64 || t = F32 || t = F64 || t = Unknown
 
    func is_ref(t : val_type | Unknown) : bool =
-     return t = Funcref || t = Exnref || t = Externref || t = Unknown
+     return t = Funcref || t = Externref || t = Unknown
 
 The algorithm uses two separate stacks: the *value stack* and the *control stack*.
 The former tracks the :ref:`types <syntax-valtype>` of operand values on the :ref:`stack <stack>`,
@@ -215,8 +215,14 @@ Other instructions are checked in a similar manner.
 
        case (catch)
          let frame = pop_ctrl()
-         error_if(frame.opcode =/= try)
-         push_ctrl(catch, [exnref], frame.end_types)
+         error_if(frame.opcode =/= try || frame.opcode =/= catch)
+         let tagparams = tags.[x].type.params
+         push_ctrl(catch, tagparams , frame.end_types)
+
+       case (catch_all)
+         let frame = pop_ctrl()
+         error_if(frame.opcode =/= try || frame.opcode =/= catch)
+         push_ctrl(catch_all, [] , frame.end_types)
 
        case (br n)
          error_if(ctrls.size() < n)

document/core/appendix/embedding.rst

@@ -76,7 +76,7 @@ Store
 
 .. math::
    \begin{array}{lclll}
-   \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon, ~\SEXNS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\
+   \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon, ~\STAGS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\
    \end{array}
 
 
@@ -539,26 +539,26 @@ Memories
    \end{array}
 
 
-.. index:: exception, exception address, store, exception instance, exception type, function type
-.. _embed-exn:
+.. index:: tag, tag address, store, tag instance, tag type, function type
+.. _embed-tag:
 
-Exceptions
-~~~~~~~~~~
+Tags
+~~~~
 
-.. _embedd-exn-alloc:
+.. _embedd-tag-alloc:
 
-:math:`\F{exn\_alloc}(\store, \exntype) : (\store, \exnaddr)`
+:math:`\F{tag\_alloc}(\store, \tagtype) : (\store, \tagaddr)`
 .............................................................
 
-1. Pre-condition: :math:`exntype` is :ref:`valid <valid-exntype>`.
+1. Pre-condition: :math:`tagtype` is :ref:`valid <valid-tagtype>`.
 
-2. Let :math:`\exnaddr` be the result of :ref:`allocating an exception <alloc-exn>` in :math:`\store` with :ref:`exception type <syntax-exntype>` :math:`\exntype`.
+2. Let :math:`\tagaddr` be the result of :ref:`allocating an tag <alloc-tag>` in :math:`\store` with :ref:`tag type <syntax-tagtype>` :math:`\tagtype`.
 
-3. Return the new store paired with :math:`\exnaddr`.
+3. Return the new store paired with :math:`\tagaddr`.
 
 .. math::
    \begin{array}{lclll}
-   \F{exn\_alloc}(S, \X{et}) &=& (S', \X{a}) && (\iff \allocexn(S, \X{et}) = S', \X{a}) \\
+   \F{tag\_alloc}(S, \X{tt}) &=& (S', \X{a}) && (\iff \alloctag(S, \X{tt}) = S', \X{a}) \\
    \end{array}
 
 

document/core/appendix/implementation.rst

@@ -24,7 +24,7 @@ However, it is expected that all implementations have "reasonably" large limits
 Syntactic Limits
 ~~~~~~~~~~~~~~~~
 
-.. index:: abstract syntax, module, type, function, table, memory, global, element, data, import, export, parameter, result, local, structured control instruction, instruction, name, Unicode, character
+.. index:: abstract syntax, module, type, function, table, memory, tag, global, element, data, import, export, parameter, result, local, structured control instruction, instruction, name, Unicode, character
 .. _impl-syntax:
 
 Structure
@@ -36,7 +36,7 @@ An implementation may impose restrictions on the following dimensions of a modul
 * the number of :ref:`functions <syntax-func>` in a :ref:`module <syntax-module>`, including imports
 * the number of :ref:`tables <syntax-table>` in a :ref:`module <syntax-module>`, including imports
 * the number of :ref:`memories <syntax-mem>` in a :ref:`module <syntax-module>`, including imports
-* the number of :ref:`exceptions <syntax-exn>` in a :ref:`module <syntax-module>`, including imports
+* the number of :ref:`tags <syntax-tag>` in a :ref:`module <syntax-module>`, including imports
 * the number of :ref:`globals <syntax-global>` in a :ref:`module <syntax-module>`, including imports
 * the number of :ref:`element segments <syntax-elem>` in a :ref:`module <syntax-module>`
 * the number of :ref:`data segments <syntax-data>` in a :ref:`module <syntax-module>`
@@ -124,7 +124,7 @@ Restrictions on the following dimensions may be imposed during :ref:`execution <
 * the number of allocated :ref:`function instances <syntax-funcinst>`
 * the number of allocated :ref:`table instances <syntax-tableinst>`
 * the number of allocated :ref:`memory instances <syntax-meminst>`
-* the number of allocated :ref:`exception instances <syntax-exninst>`
+* the number of allocated :ref:`tag instances <syntax-taginst>`
 * the number of allocated :ref:`global instances <syntax-globalinst>`
 * the size of a :ref:`table instance <syntax-tableinst>`
 * the size of a :ref:`memory instance <syntax-meminst>`

document/core/appendix/index-rules.rst

@@ -18,7 +18,7 @@ Construct                                        Judgement
 :ref:`Block type <valid-blocktype>`              :math:`\vdashblocktype \blocktype \ok`
 :ref:`Table type <valid-tabletype>`              :math:`\vdashtabletype \tabletype \ok`
 :ref:`Memory type <valid-memtype>`               :math:`\vdashmemtype \memtype \ok`
-:ref:`Exception type <valid-exntype>`            :math:`\vdashexntype \exntype \ok`
+:ref:`Tag type <valid-tagtype>`                  :math:`\vdashtagtype \tagtype \ok`
 :ref:`Global type <valid-globaltype>`            :math:`\vdashglobaltype \globaltype \ok`
 :ref:`External type <valid-externtype>`          :math:`\vdashexterntype \externtype \ok`
 :ref:`Instruction <valid-instr>`                 :math:`S;C \vdashinstr \instr : \stacktype`
@@ -27,7 +27,7 @@ Construct                                        Judgement
 :ref:`Function <valid-func>`                     :math:`C \vdashfunc \func : \functype`
 :ref:`Table <valid-table>`                       :math:`C \vdashtable \table : \tabletype`
 :ref:`Memory <valid-mem>`                        :math:`C \vdashmem \mem : \memtype`
-:ref:`Exception <valid-exn>`                     :math:`C \vdashexn \exn : \exntype`
+:ref:`Tag <valid-tag>`                           :math:`C \vdashtag \tag : \tagtype`
 :ref:`Global <valid-global>`                     :math:`C \vdashglobal \global : \globaltype`
 :ref:`Element segment <valid-elem>`              :math:`C \vdashelem \elem : \reftype`
 :ref:`Element mode <valid-elemmode>`             :math:`C \vdashelemmode \elemmode : \reftype`
@@ -56,7 +56,7 @@ Construct                                        Judgement
 :ref:`Function instance <valid-funcinst>`        :math:`S \vdashfuncinst \funcinst : \functype`
 :ref:`Table instance <valid-tableinst>`          :math:`S \vdashtableinst \tableinst : \tabletype`
 :ref:`Memory instance <valid-meminst>`           :math:`S \vdashmeminst \meminst : \memtype`
-:ref:`Exception instance <valid-exninst>`        :math:`S \vdashexninst \exninst : \exntype`
+:ref:`Tag instance <valid-taginst>`              :math:`S \vdashtaginst \taginst : \tagtype`
 :ref:`Global instance <valid-globalinst>`        :math:`S \vdashglobalinst \globalinst : \globaltype`
 :ref:`Element instance <valid-eleminst>`         :math:`S \vdasheleminst \eleminst \ok`
 :ref:`Data instance <valid-datainst>`            :math:`S \vdashdatainst \datainst \ok`
@@ -100,7 +100,7 @@ Construct                                        Judgement
 :ref:`Function instance <extend-funcinst>`       :math:`\vdashfuncinstextends \funcinst_1 \extendsto \funcinst_2`
 :ref:`Table instance <extend-tableinst>`         :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2`
 :ref:`Memory instance <extend-meminst>`          :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2`
-:ref:`Exception instance <extend-exninst>`       :math:`\vdashexninstextends \exninst_1 \extendsto \exninst_2`
+:ref:`Tag instance <extend-taginst>`             :math:`\vdashtaginstextends \taginst_1 \extendsto \taginst_2`
 :ref:`Global instance <extend-globalinst>`       :math:`\vdashglobalinstextends \globalinst_1 \extendsto \globalinst_2`
 :ref:`Element instance <extend-eleminst>`         :math:`\vdasheleminstextends \eleminst_1 \extendsto \eleminst_2`
 :ref:`Data instance <extend-datainst>`           :math:`\vdashdatainstextends \datainst_1 \extendsto \datainst_2`

document/core/appendix/index-types.rst

@@ -15,13 +15,12 @@ Category                                  Constructor
 (reserved)                                                                             :math:`\hex{7B}` .. :math:`\hex{71}`
 :ref:`Reference type <syntax-reftype>`    |FUNCREF|                                    :math:`\hex{70}` (-16 as |Bs7|)
 :ref:`Reference type <syntax-reftype>`    |EXTERNREF|                                  :math:`\hex{6F}` (-17 as |Bs7|)
-:ref:`Reference type <syntax-reftype>`    |EXNREF|                                     :math:`\hex{68}` (-18 as |Bs7|)
 (reserved)                                                                             :math:`\hex{6D}` .. :math:`\hex{61}`
 :ref:`Function type <syntax-functype>`    :math:`[\valtype^\ast] \to [\valtype^\ast]`  :math:`\hex{60}` (-32 as |Bs7|)
 (reserved)                                                                             :math:`\hex{5F}` .. :math:`\hex{41}`
 :ref:`Result type <syntax-resulttype>`    :math:`[\epsilon]`                             :math:`\hex{40}` (-64 as |Bs7|)
 :ref:`Table type <syntax-tabletype>`      :math:`\limits~\reftype`                     (none)
 :ref:`Memory type <syntax-memtype>`       :math:`\limits`                              (none)
-:ref:`Exception type <syntax-exntype>`    :math:`\functype`                            (none)
+:ref:`Tag type <syntax-tagtype>`          :math:`\functype`                            (none)
 :ref:`Global type <syntax-globaltype>`    :math:`\mut~\valtype`                        (none)
 ========================================  ===========================================  ===============================================================================