Address additional review of #222, also fixing label types everywhere.

document/core/appendix/algorithm.rst

@@ -16,7 +16,7 @@ Consequently, it can be integrated directly into a decoder.
 The algorithm is expressed in typed pseudo code whose semantics is intended to be self-explanatory.
 
 
-.. index:: value type, stack, label, frame, instruction
+.. index:: value type, label type, stack, label, frame, instruction
 
 Data Structures
 ~~~~~~~~~~~~~~~
@@ -51,6 +51,7 @@ the latter surrounding :ref:`structured control instructions <syntax-instr-contr
      end_types : list(val_type)
      height : nat
      unreachable : bool
+     catch_label : bool
    }
 
 For each value, the value stack records its :ref:`value type <syntax-valtype>`, or :code:`Unknown` when the type is not known.
@@ -122,9 +123,16 @@ The control stack is likewise manipulated through auxiliary functions:
      ctrls.pop()
      return frame
 
-   func label_types(frame : ctrl_frame) : list(val_types) =
+   func label_val_types(frame : ctrl_frame) : list(val_type) =
      return (if frame.opcode == loop then frame.start_types else frame.end_types)
 
+   func is_catch(frame : ctrl_frame) : bool =
+     return frame.catch_label
+
+   func set_catch(catch : bool) =
+     error_if(ctrls.is_empty())
+     ctrls[0].catch_label := catch
+
    func unreachable() =
      vals.resize(ctrls[0].height)
      ctrls[0].unreachable := true
@@ -136,7 +144,9 @@ Popping a frame first checks that the control stack is not empty.
 It then verifies that the operand stack contains the right types of values expected at the end of the exited block and pops them off the operand stack.
 Afterwards, it checks that the stack has shrunk back to its initial height.
 
-The type of the :ref:`label <syntax-label>` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from.
+The result type of the :ref:`label <syntax-label>` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from.
+
+Whether a label has :ref:`label type <syntax-labeltype>` with present |LCATCH| is stored with the boolean :math:`catch_label` of the frame, which can be checked with :math:`is_catch`, or modified in the top control frame with :math:`set_catch`.
 
 Finally, the current frame can be marked as unreachable.
 In that case, all existing operand types are purged from the value stack, in order to allow for the :ref:`stack-polymorphism <polymorphism>` logic in :code:`pop_val` to take effect.
@@ -219,32 +229,34 @@ Other instructions are checked in a similar manner.
          error_if(frame.opcode =/= try || frame.opcode =/= catch)
          let params = tags[x].type.params
          push_ctrl(catch, params , frame.end_types)
+         if (frame.opcode =/= try) then set_catch(true)
 
        case (catch_all)
          let frame = pop_ctrl()
          error_if(frame.opcode =/= try || frame.opcode =/= catch)
          push_ctrl(catch_all, [], frame.end_types)
+         if (frame.opcode =/= try) then set_catch(true)
 
        case (br n)
          error_if(ctrls.size() < n)
-         pop_vals(label_types(ctrls[n]))
+         pop_vals(label_val_types(ctrls[n]))
          unreachable()
 
        case (br_if n)
          error_if(ctrls.size() < n)
          pop_val(I32)
-         pop_vals(label_types(ctrls[n]))
-         push_vals(label_types(ctrls[n]))
+         pop_vals(label_val_types(ctrls[n]))
+         push_vals(label_val_types(ctrls[n]))
 
        case (br_table n* m)
          pop_val(I32)
          error_if(ctrls.size() < m)
-         let arity = label_types(ctrls[m]).size()
+         let arity = label_val_types(ctrls[m]).size()
          foreach (n in n*)
            error_if(ctrls.size() < n)
-           error_if(label_types(ctrls[n]).size() =/= arity)
-           push_vals(pop_vals(label_types(ctrls[n])))
-         pop_vals(label_types(ctrls[m]))
+           error_if(label_val_types(ctrls[n]).size() =/= arity)
+           push_vals(pop_vals(label_val_types(ctrls[n])))
+         pop_vals(label_val_types(ctrls[m]))
          unreachable()
 
 .. todo::

document/core/appendix/properties.rst

@@ -655,7 +655,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
    \frac{
      S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast]
      \qquad
-     C.\CLABELS[l] = [t_0^\ast]
+     C.\CLABELS[l] = \LCATCH^?~[t_0^\ast]
    }{
      S; C,\CLABELS\,[t^\ast] \vdashadmininstr \DELEGATEadm\{l\}~\instr^\ast~\END : [] \to [t^\ast]
    }
@@ -670,14 +670,14 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 
 * The :ref:`values <syntax-val>` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector.
+* The label type :math:`C.\CLABELS[0]` must be defined in the context.
+
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[0]` modified to :math:`(\LCATCH~[t^\ast])` in the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t^\ast]`.
 
-* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector.
-
-* Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`.
+* Then the compound instruction is valid under context :math:`C` with type :math:`[] \to [t^\ast]`.
 
 
 .. math::
@@ -686,9 +686,9 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
      \qquad
      (val : t_0)^\ast
      \qquad
-     S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast]
+     S; C,\CLABELS[0]:=(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast]
    }{
-     S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast]
+     S; C \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast]
    }
 
 
@@ -716,7 +716,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 
 * The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid <valid-instr-seq>` with some type :math:`[t_1^n] \to [t_2^*]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_1^n]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`[t_1^n]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t_2^*]`.

document/core/valid/instructions.rst

@@ -1234,7 +1234,7 @@ Memory Instructions
    }
 
 
-.. index:: control instructions, structured control, label, block, branch, block type, label index, function index, type index, tag index, vector, polymorphism, context
+.. index:: control instructions, structured control, label, block, branch, block type, label index, label type, function index, type index, tag index, vector, polymorphism, context
    pair: validation; instruction
    single: abstract syntax; instruction
 .. _valid-label:
@@ -1281,7 +1281,7 @@ Control Instructions
 
 * The :ref:`block type <syntax-blocktype>` must be :ref:`valid <valid-blocktype>` as some :ref:`function type <syntax-functype>` :math:`[t_1^\ast] \to [t_2^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
@@ -1308,7 +1308,7 @@ Control Instructions
 
 * The :ref:`block type <syntax-blocktype>` must be :ref:`valid <valid-blocktype>` as some :ref:`function type <syntax-functype>` :math:`[t_1^\ast] \to [t_2^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_1^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`[t_1^\ast]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
@@ -1335,7 +1335,7 @@ Control Instructions
 
 * The :ref:`block type <syntax-blocktype>` must be :ref:`valid <valid-blocktype>` as some :ref:`function type <syntax-functype>` :math:`[t_1^\ast] \to [t_2^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
@@ -1368,23 +1368,25 @@ Control Instructions
 
 * The :ref:`block type <syntax-blocktype>` must be :ref:`valid <valid-blocktype>` as some :ref:`function type <syntax-functype>` :math:`[t_1^\ast] \to [t_2^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
 
-* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label <exec-label>` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector.
 
-* For every :math:`(\CATCH~x~\instr_2^\ast)`:
+* For every :math:`x_i` and :math:`\instr_{2i}^\ast` in :math:`(\CATCH~x~\instr_2^\ast)^\ast`:
 
   * The tag :math:`C.\CTAGS[x]` must be defined in the context :math:`C`.
 
-  * Let :math:`[t^\ast] \to []` be its :ref:`tag type <syntax-tagtype>`.
+  * Let :math:`[t_{3i}^\ast] \to [t_{4i}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x]`.
+
+  * The :ref:`result type <syntax-resulttype>` :math:`[t_{4i}^\ast]` must be empty.
 
   * Under context :math:`C''`,
-    the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t^\ast] \to [t_2^\ast]`.
+    the instruction sequence :math:`\instr_{2i}^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_{3i}^\ast] \to [t_2^\ast]`.
 
-* If there is a :math:`(\CATCHALL~\instr_3^\ast)`, then:
+* If :math:`(\CATCHALL~\instr_3^\ast)^?` is not empty, then:
 
   * Under context :math:`C''`,
     the instruction sequence :math:`\instr_3^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t_2^\ast]`.
@@ -1458,11 +1460,11 @@ Control Instructions
 :math:`\RETHROW~l`
 ..................
 
-* The label :math:`C.\CLABELS[l]` must be defined in the context.
+* The label type :math:`C.\CLABELS[l]` must be defined in the context.
 
-* Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type <labeltype>` :math:`C.\CLABELS[l]`.
+* Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[l]`.
 
-* The |LCATCH| must be present in the :ref:`label type <labeltype>` :math:`C.\CLABELS[l]`.
+* The |LCATCH| must be present in the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[l]`.
 
 * Then the instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of  :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
 
@@ -1485,21 +1487,21 @@ Control Instructions
 :math:`\BR~l`
 .............
 
-* The label :math:`C.\CLABELS[l]` must be defined in the context.
+* The label type :math:`C.\CLABELS[l]` must be defined in the context.
 
-* Let :math:`[t^\ast]` be the :ref:`result type <syntax-resulttype>` :math:`C.\CLABELS[l]`.
+* Let :math:`\LCATCH^?~[t^\ast]` be the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[l]`.
 
 * Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
 
 .. math::
    \frac{
-     C.\CLABELS[l] = [t^\ast]
+     C.\CLABELS[l] = \LCATCH^?~[t^\ast]
    }{
      C \vdashinstr \BR~l : [t_1^\ast~t^\ast] \to [t_2^\ast]
    }
 
 .. note::
-   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
+   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label type first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
 
    The |BR| instruction is :ref:`stack-polymorphic <polymorphism>`.
 
@@ -1509,21 +1511,21 @@ Control Instructions
 :math:`\BRIF~l`
 ...............
 
-* The label :math:`C.\CLABELS[l]` must be defined in the context.
+* The label type :math:`C.\CLABELS[l]` must be defined in the context.
 
-* Let :math:`[t^\ast]` be the :ref:`result type <syntax-resulttype>` :math:`C.\CLABELS[l]`.
+* Let :math:`\LCATCH^?~[t^\ast]` be the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[l]`.
 
 * Then the instruction is valid with type :math:`[t^\ast~\I32] \to [t^\ast]`.
 
 .. math::
    \frac{
-     C.\CLABELS[l] = [t^\ast]
+     C.\CLABELS[l] = \LCATCH^?~[t^\ast]
    }{
      C \vdashinstr \BRIF~l : [t^\ast~\I32] \to [t^\ast]
    }
 
 .. note::
-   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
+   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label type first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
 
 
 .. _valid-br_table:
@@ -1532,10 +1534,10 @@ Control Instructions
 ...........................
 
 
-* The label :math:`C.\CLABELS[l_N]` must be defined in the context.
+* The label type :math:`C.\CLABELS[l_N]` must be defined in the context.
 
 * For all :math:`l_i` in :math:`l^\ast`,
-  the label :math:`C.\CLABELS[l_i]` must be defined in the context.
+  the label type :math:`C.\CLABELS[l_i]` must be defined in the context.
 
 * There must be a :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`, such that:
 

document/core/valid/modules.rst

@@ -29,7 +29,7 @@ Functions :math:`\func` are classified by :ref:`function types <syntax-functype>
 
   * |CLOCALS| set to the sequence of :ref:`value types <syntax-valtype>` :math:`t_1^\ast~t^\ast`, concatenating parameters and locals,
 
-  * |CLABELS| set to the singular sequence containing only :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]`.
+  * |CLABELS| set to the singular sequence containing only :ref:`label type <syntax-labeltype>` :math:`[t_2^\ast]`.
 
   * |CRETURN| set to the :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]`.