Update formal spec to implement the 3rd EH proposal without prose. (WebAssembly#180)

* Update core formal spec to the current (3rd) EH proposal

As described in `proposals/exceptions/Exceptions.md` and in
`proposals/exceptions/Exceptions-formal-overview.md`.

* Detailed changes from the previous (2nd proposal) formal spec:

  - Removed:
    + the reference type "exnref" is removed,
    + the administrative instruction "REFEXNADDR" is removed,
    + Release dependencies "bulk instructions" and "reference types" are removed.
  - Renamed:
    + "exn" and (most occurrences of) "exception" renamed to "tag",
    + "EITYPE" renamed to "TAGITYPE",
    + "ETYPE" renamed to "TAGTYPE",
    + variable names for tags changed from "et" to "tt" or "tagt" and "iet" to "itagt",
    + "CATCHN" is renamed to "CATCHadm".
    + "THROWADDR" is renamed to "THROWadm".
  - Adjusted:
    + syntax and rules for "TRY-CATCH", "RETHROW", and "CATCHadm",
    + folded text format for "TRY-CATCH",
    + validation example of control frame with opcode catch.
  - Added:
    + validation example of control frame with opcode catch_all,
    + administrative instructions "CAUGHTadm" and "DELEGATEadm" with rules,
    + syntax and rules for "TRY-DELEGATE".
  - Most prose that is changing in the 3rd spec is removed and several temporary `..todo::` sections are added.
    + These will be updated in followup PRs.

Co-authored-by: Heejin Ahn <aheejin@gmail.com>
Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>

Author: 3 people

document/core/appendix/algorithm.rst

@@ -25,7 +25,7 @@ Types are representable as an enumeration.
 
 .. code-block:: pseudo
 
-   type val_type = I32 | I64 | F32 | F64 | V128 | Funcref | Exnref | Externref
+   type val_type = I32 | I64 | F32 | F64 | V128 | Funcref | Externref
 
    func is_num(t : val_type | Unknown) : bool =
      return t = I32 || t = I64 || t = F32 || t = F64 || t = Unknown
@@ -34,7 +34,7 @@ Types are representable as an enumeration.
      return t = V128 || 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>`,
@@ -216,8 +216,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 params = tags[x].type.params
+         push_ctrl(catch, params , 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)
@@ -241,7 +247,8 @@ Other instructions are checked in a similar manner.
          pop_vals(label_types(ctrls[m]))
          unreachable()
 
-
+.. todo::
+   Add a case for :code:`throw`.
 
 .. note::
    It is an invariant under the current WebAssembly instruction set that an operand of :code:`Unknown` type is never duplicated on the stack.

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 a 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

@@ -16,13 +16,12 @@ Category                                  Constructor
 (reserved)                                                                             :math:`\hex{7A}` .. :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{6E}` (-18 as |Bs7|)
-(reserved)                                                                             :math:`\hex{6D}` .. :math:`\hex{61}`
+(reserved)                                                                             :math:`\hex{6E}` .. :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)
 ========================================  ===========================================  ===============================================================================