[spec/interpreter/test] Reintroduce bottom type

document/core/appendix/algorithm.rst

@@ -27,11 +27,11 @@ Types are representable as an enumeration.
 
    type val_type = I32 | I64 | F32 | F64 | Funcref | Externref
 
-   func is_num(t : val_type) : bool =
-     return t = I32 || t = I64 || t = F32 || t = F64
+   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) : bool =
-     return t = Funcref || t = Externref
+   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>`,
@@ -52,7 +52,6 @@ the latter surrounding :ref:`structured control instructions <syntax-instr-contr
 
 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:
@@ -222,13 +221,17 @@ Other instructions are checked in a similar manner.
          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_val(I32)
-         pop_vals(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`.

document/core/appendix/index-rules.rst

@@ -20,8 +20,8 @@ Construct                                        Judgement
 :ref:`Memory type <valid-memtype>`               :math:`\vdashmemtype \memtype \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 : \functype`
-:ref:`Instruction sequence <valid-instr-seq>`    :math:`S;C \vdashinstrseq \instr^\ast : \functype`
+:ref:`Instruction <valid-instr>`                 :math:`S;C \vdashinstr \instr : \stacktype`
+:ref:`Instruction sequence <valid-instr-seq>`    :math:`S;C \vdashinstrseq \instr^\ast : \stacktype`
 :ref:`Expression <valid-expr>`                   :math:`C \vdashexpr \expr : \resulttype`
 :ref:`Function <valid-func>`                     :math:`C \vdashfunc \func : \functype`
 :ref:`Table <valid-table>`                       :math:`C \vdashtable \table : \tabletype`

document/core/util/macros.def

@@ -209,6 +209,9 @@
 
 .. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}}
 
+.. |stacktype| mathdef:: \xref{syntax/types}{syntax-stacktype}{\X{stacktype}}
+.. |opdtype| mathdef:: \xref{syntax/types}{syntax-opdtype}{\X{opdtype}}
+
 
 .. Types, meta functions
 

document/core/valid/instructions.rst

@@ -1,13 +1,39 @@
 .. index:: instruction, function type, context, value, operand stack, ! polymorphism
 .. _valid-instr:
+.. _syntax-stacktype:
+.. _syntax-opdtype:
 
 Instructions
 ------------
 
-:ref:`Instructions <syntax-instr>` are classified by :ref:`function types <syntax-functype>` :math:`[t_1^\ast] \to [t_2^\ast]`
-that describe how they manipulate the :ref:`operand stack <stack>`.
-The types describe the required input stack with argument values of types :math:`t_1^\ast` that an instruction pops off
+:ref:`Instructions <syntax-instr>` are classified by *stack types* :math:`[t_1^\ast] \to [t_2^\ast]` that describe how instructions manipulate the :ref:`operand stack <stack>`.
+
+.. math::
+   \begin{array}{llll}
+   \production{stack type} & \stacktype &::=&
+     [\opdtype^\ast] \to [\opdtype^\ast] \\
+   \production{operand type} & \opdtype &::=&
+     \valtype ~|~ \bot \\
+   \end{array}
+
+The types describe the required input stack with *operand types* :math:`t_1^\ast` that an instruction pops off
 and the provided output stack with result values of types :math:`t_2^\ast` that it pushes back.
+Stack types are akin to :ref:`function types <syntax-functype>`,
+except that they allow individual operands to be classified as :math:`\bot`, indicating that the type is unconstrained.
+As an auxiliary notion, an operand type :math:`t_1` *matches* another operand type :math:`t_2`, if :math:`t_1` is either :math:`\bot` or equal to :math:`t_2`.
+
+.. _match-opdtype:
+
+.. math::
+   \frac{
+   }{
+     \vdash t \leq t
+   }
+   \qquad
+   \frac{
+   }{
+     \vdash \bot \leq t
+   }
 
 .. note::
    For example, the instruction :math:`\I32.\ADD` has type :math:`[\I32~\I32] \to [\I32]`,
@@ -254,7 +280,7 @@ Parametric Instructions
 
 * Else:
 
-  * The instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any :ref:`number type <syntax-numtype>` :math:`t`.
+  * The instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any :ref:`operand type <syntax-opdtype>` :math:`t` that :ref:`matches <match-opdtype>` some :ref:`number type <syntax-numtype>`.
 
 .. math::
    \frac{
@@ -263,7 +289,7 @@ Parametric Instructions
    }
    \qquad
    \frac{
-     t = \numtype
+     \vdash t \leq \numtype
    }{
      C \vdashinstr \SELECT : [t~t~\I32] \to [t]
    }
@@ -1033,7 +1059,7 @@ Empty Instruction Sequence: :math:`\epsilon`
 ............................................
 
 * The empty instruction sequence is valid with type :math:`[t^\ast] \to [t^\ast]`,
-  for any sequence of :ref:`value types <syntax-valtype>` :math:`t^\ast`.
+  for any sequence of :ref:`operand types <syntax-opdtype>` :math:`t^\ast`.
 
 .. math::
    \frac{
@@ -1052,13 +1078,17 @@ Non-empty Instruction Sequence: :math:`\instr^\ast~\instr_N`
   for some sequences of :ref:`value types <syntax-valtype>` :math:`t^\ast` and :math:`t_3^\ast`.
 
 * There must be a sequence of :ref:`value types <syntax-valtype>` :math:`t_0^\ast`,
-  such that :math:`t_2^\ast = t_0^\ast~t^\ast`.
+  such that :math:`t_2^\ast = t_0^\ast~{t'}^\ast` where the type sequence :math:`{t'}^\ast` is as long as :math:`t^\ast`.
+
+* For each :ref:`operand type <syntax-opdtype>` :math:`t'_i` in :math:`{t'}^\ast` and corresponding type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches <match-opdtype>` :math:`t_i`.
 
 * Then the combined instruction sequence is valid with type :math:`[t_1^\ast] \to [t_0^\ast~t_3^\ast]`.
 
 .. math::
    \frac{
-     C \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_0^\ast~t^\ast]
+     C \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_0^\ast~{t'}^\ast]
+     \qquad
+     (\vdash t' \leq t)^\ast
      \qquad
      C \vdashinstr \instr_N : [t^\ast] \to [t_3^\ast]
    }{
@@ -1081,14 +1111,17 @@ Expressions :math:`\expr` are classified by :ref:`result types <syntax-resulttyp
 :math:`\instr^\ast~\END`
 ........................
 
-* The instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t^\ast]`,
-  for some :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`.
+* The instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with some :ref:`stack type <syntax-stacktype>` :math:`[] \to [t'^\ast]`.
+
+* For each :ref:`operand type <syntax-opdtype>` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`value type <syntax-valtype>` type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches <match-opdtype>` :math:`t_i`.
 
 * Then the expression is valid with :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`.
 
 .. math::
    \frac{
-     C \vdashinstrseq \instr^\ast : [] \to [t^\ast]
+     C \vdashinstrseq \instr^\ast : [] \to [{t'}^\ast]
+     \qquad
+     (\vdash t' \leq t)^\ast
    }{
      C \vdashexpr \instr^\ast~\END : [t^\ast]
    }

interpreter/valid/valid.ml

@@ -77,6 +77,7 @@ let known = List.map (fun t -> Some t)
 let stack ts = (NoEllipses, known ts)
 let (-~>) ts1 ts2 = {ins = NoEllipses, ts1; outs = NoEllipses, ts2}
 let (-->) ts1 ts2 = {ins = NoEllipses, known ts1; outs = NoEllipses, known ts2}
+let (-~>...) ts1 ts2 = {ins = Ellipses, ts1; outs = Ellipses, ts2}
 let (-->...) ts1 ts2 = {ins = Ellipses, known ts1; outs = Ellipses, known ts2}
 
 let string_of_infer_type t =
@@ -247,9 +248,11 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
     (label c x @ [NumType I32Type]) --> label c x
 
   | BrTable (xs, x) ->
-    let ts = label c x in
-    List.iter (fun x' -> check_stack (known ts) (known (label c x')) x'.at) xs;
-    (ts @ [NumType I32Type]) -->... []
+    let n = List.length (label c x) in
+    let ts = Lib.List.table n (fun i -> peek (n - i) s) in
+    check_stack ts (known (label c x)) x.at;
+    List.iter (fun x' -> check_stack ts (known (label c x')) x'.at) xs;
+    (ts @ [Some (NumType I32Type)]) -~>... []
 
   | Return ->
     c.results -->... []

test/core/br_table.wast

@@ -1250,6 +1250,18 @@
       )
     )
   )
+
+  (func (export "meet-bottom")
+    (block (result f64)
+      (block (result f32)
+        (unreachable)
+        (br_table 0 1 1 (i32.const 1))
+      )
+      (drop)
+      (f64.const 0)
+    )
+    (drop)
+  )
 )
 
 (assert_return (invoke "type-i32"))

test/core/select.wast

@@ -195,6 +195,19 @@
       (i32.wrap_i64 (select (i64.const 1) (i64.const 0) (local.get 0)))
     )
   )
+
+  (func (export "unreachable-num")
+    (unreachable)
+    (select)
+    (i32.eqz)
+    (drop)
+  )
+  (func (export "unreachable-ref")
+    (unreachable)
+    (select)
+    (ref.is_null)
+    (drop)
+  )
 )
 
 (assert_return (invoke "select-i32" (i32.const 1) (i32.const 2) (i32.const 1)) (i32.const 1))

test/core/unreached-invalid.wast

@@ -536,21 +536,6 @@
   "type mismatch"
 )
 
-(assert_invalid
-  (module (func $type-br_table-label-num-vs-label-num-after-unreachable
-    (block (result f64)
-      (block (result f32)
-        (unreachable)
-        (br_table 0 1 1 (i32.const 1))
-      )
-      (drop)
-      (f64.const 0)
-    )
-    (drop)
-  ))
-  "type mismatch"
-)
-
 (assert_invalid
   (module (func $type-block-value-nested-unreachable-num-vs-void
     (block (i32.const 3) (block (unreachable)))