[spec/interpreter/test] Land bulk instructions & reference types prop…

…osals (#1287)

document/core/appendix/algorithm.rst

@@ -21,15 +21,25 @@ The algorithm is expressed in typed pseudo code whose semantics is intended to b
 Data Structures
 ~~~~~~~~~~~~~~~
 
-The algorithm uses two separate stacks: the *operand stack* and the *control stack*.
+Types are representable as an enumeration.
+
+.. code-block:: pseudo
+
+   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 = 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>`,
 the latter surrounding :ref:`structured control instructions <syntax-instr-control>` and their associated :ref:`blocks <syntax-instr-control>`.
 
 .. code-block:: pseudo
 
-   type val_type = I32 | I64 | F32 | F64
-
-   type opd_stack = stack(val_type | Unknown)
+   type val_stack = stack(val_type | Unknown)
 
    type ctrl_stack = stack(ctrl_frame)
    type ctrl_frame = {
@@ -40,79 +50,82 @@ the latter surrounding :ref:`structured control instructions <syntax-instr-contr
      unreachable : bool
    }
 
-For each value, the operand stack records its :ref:`value type <syntax-valtype>`, or :code:`Unknown` when the type is not known.
+For each value, the value stack records its :ref:`value type <syntax-valtype>`, or :code:`Unknown` when the type is not known.
 
 For each entered block, the control stack records a *control frame* with the originating opcode, the types on the top of the operand stack at the start and end of the block (used to check its result as well as branches), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), and a flag recording whether the remainder of the block is unreachable (used to handle :ref:`stack-polymorphic <polymorphism>` typing after branches).
 
 For the purpose of presenting the algorithm, the operand and control stacks are simply maintained as global variables:
 
 .. code-block:: pseudo
 
-   var opds : opd_stack
+   var vals : val_stack
    var ctrls : ctrl_stack
 
 However, these variables are not manipulated directly by the main checking function, but through a set of auxiliary functions:
 
 .. code-block:: pseudo
 
-   func push_opd(type : val_type | Unknown) =
-     opds.push(type)
+   func push_val(type : val_type | Unknown) =
+     vals.push(type)
 
-   func pop_opd() : val_type | Unknown =
-     if (opds.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown
-     error_if(opds.size() = ctrls[0].height)
-     return opds.pop()
+   func pop_val() : val_type | Unknown =
+     if (vals.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown
+     error_if(vals.size() = ctrls[0].height)
+     return vals.pop()
 
-   func pop_opd(expect : val_type | Unknown) : val_type | Unknown =
-     let actual = pop_opd()
+   func pop_val(expect : val_type | Unknown) : val_type | Unknown =
+     let actual = pop_val()
      if (actual = Unknown) return expect
      if (expect = Unknown) return actual
      error_if(actual =/= expect)
      return actual
 
-   func push_opds(types : list(val_type)) = foreach (t in types) push_opd(t)
-   func pop_opds(types : list(val_type)) = foreach (t in reverse(types)) pop_opd(t)
+   func push_vals(types : list(val_type)) = foreach (t in types) push_val(t)
+   func pop_vals(types : list(val_type)) : list(val_type) =
+     var popped := []
+     foreach (t in reverse(types)) popped.append(pop_val(t))
+     return popped
 
-Pushing an operand simply pushes the respective type to the operand stack.
+Pushing an operand value simply pushes the respective type to the value stack.
 
-Popping an operand checks that the operand stack does not underflow the current block and then removes one type.
-But first, a special case is handled where the block contains no known operands, but has been marked as unreachable.
+Popping an operand value checks that the value stack does not underflow the current block and then removes one type.
+But first, a special case is handled where the block contains no known values, but has been marked as unreachable.
 That can occur after an unconditional branch, when the stack is typed :ref:`polymorphically <polymorphism>`.
 In that case, an unknown type is returned.
 
-A second function for popping an operand takes an expected type, which the actual operand type is checked against.
+A second function for popping an operand value takes an expected type, which the actual operand type is checked against.
 The types may differ in case one of them is Unknown.
-The more specific type is returned.
+The function returns the actual type popped from the stack.
 
 Finally, there are accumulative functions for pushing or popping multiple operand types.
 
 .. note::
    The notation :code:`stack[i]` is meant to index the stack from the top,
-   so that :code:`ctrls[0]` accesses the element pushed last.
+   so that, e.g., :code:`ctrls[0]` accesses the element pushed last.
 
 
 The control stack is likewise manipulated through auxiliary functions:
 
 .. code-block:: pseudo
 
    func push_ctrl(opcode : opcode, in : list(val_type), out : list(val_type)) =
-     let frame = ctrl_frame(opcode, in, out, opds.size(), false)
+     let frame = ctrl_frame(opcode, in, out, vals.size(), false)
      ctrls.push(frame)
-     push_opds(in)
+     push_vals(in)
 
    func pop_ctrl() : ctrl_frame =
      error_if(ctrls.is_empty())
      let frame = ctrls[0]
-     pop_opds(frame.end_types)
-     error_if(opds.size() =/= frame.height)
+     pop_vals(frame.end_types)
+     error_if(vals.size() =/= frame.height)
      ctrls.pop()
      return frame
 
    func label_types(frame : ctrl_frame) : list(val_types) =
      return (if frame.opcode == loop then frame.start_types else frame.end_types)
 
    func unreachable() =
-     opds.resize(ctrls[0].height)
+     vals.resize(ctrls[0].height)
      ctrls[0].unreachable := true
 
 Pushing a control frame takes the types of the label and result values.
@@ -125,7 +138,7 @@ 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.
 
 Finally, the current frame can be marked as unreachable.
-In that case, all existing operand types are purged from the operand stack, in order to allow for the :ref:`stack-polymorphism <polymorphism>` logic in :code:`pop_opd` to take effect.
+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.
 
 .. note::
    Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand stack.
@@ -150,38 +163,46 @@ Other instructions are checked in a similar manner.
    func validate(opcode) =
      switch (opcode)
        case (i32.add)
-         pop_opd(I32)
-         pop_opd(I32)
-         push_opd(I32)
+         pop_val(I32)
+         pop_val(I32)
+         push_val(I32)
 
        case (drop)
-         pop_opd()
+         pop_val()
 
        case (select)
-         pop_opd(I32)
-         let t1 = pop_opd()
-         let t2 = pop_opd(t1)
-         push_opd(t2)
+         pop_val(I32)
+         let t1 = pop_val()
+         let t2 = pop_val()
+         error_if(not (is_num(t1) && is_num(t2)))
+         error_if(t1 =/= t2 && t1 =/= Unknown && t2 =/= Unknown)
+         push_val(if (t1 = Unknown) t2 else t1)
+
+       case (select t)
+         pop_val(I32)
+         pop_val(t)
+         pop_val(t)
+         push_val(t)
 
        case (unreachable)
          unreachable()
 
        case (block t1*->t2*)
-         pop_opds([t1*])
+         pop_vals([t1*])
          push_ctrl(block, [t1*], [t2*])
 
        case (loop t1*->t2*)
-         pop_opds([t1*])
+         pop_vals([t1*])
          push_ctrl(loop, [t1*], [t2*])
 
        case (if t1*->t2*)
-         pop_opd(I32)
-         pop_opds([t1*])
+         pop_val(I32)
+         pop_vals([t1*])
          push_ctrl(if, [t1*], [t2*])
 
        case (end)
          let frame = pop_ctrl()
-         push_opds(frame.end_types)
+         push_vals(frame.end_types)
 
        case (else)
          let frame = pop_ctrl()
@@ -190,23 +211,27 @@ Other instructions are checked in a similar manner.
 
        case (br n)
          error_if(ctrls.size() < n)
-         pop_opds(label_types(ctrls[n]))
+         pop_vals(label_types(ctrls[n]))
          unreachable()
 
        case (br_if n)
          error_if(ctrls.size() < n)
-         pop_opd(I32)
-         pop_opds(label_types(ctrls[n]))
-         push_opds(label_types(ctrls[n]))
+         pop_val(I32)
+         pop_vals(label_types(ctrls[n]))
+         push_vals(label_types(ctrls[n]))
 
        case (br_table n* m)
+         pop_val(I32)
          error_if(ctrls.size() < m)
+         let arity = label_types(ctrls[m]).size()
          foreach (n in n*)
-           error_if(ctrls.size() < n || label_types(ctrls[n]) =/= label_types(ctrls[m]))
-         pop_opd(I32)
-         pop_opds(label_types(ctrls[m]))
+           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]))
          unreachable()
 
+
 .. note::
    It is an invariant under the current WebAssembly instruction set that an operand of :code:`Unknown` type is never duplicated on the stack.
    This would change if the language were extended with stack instructions like :code:`dup`.