diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index be20a535..fcfe0ad4 100644 --- a/document/core/appendix/algorithm.rst +++ b/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 ` of operand values on the :ref:`stack `, @@ -52,7 +52,6 @@ the latter surrounding :ref:`structured control instructions `, 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 ` 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`. diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst index dde34900..0da08412 100644 --- a/document/core/appendix/index-rules.rst +++ b/document/core/appendix/index-rules.rst @@ -20,8 +20,8 @@ Construct Judgement :ref:`Memory type ` :math:`\vdashmemtype \memtype \ok` :ref:`Global type ` :math:`\vdashglobaltype \globaltype \ok` :ref:`External type ` :math:`\vdashexterntype \externtype \ok` -:ref:`Instruction ` :math:`S;C \vdashinstr \instr : \functype` -:ref:`Instruction sequence ` :math:`S;C \vdashinstrseq \instr^\ast : \functype` +:ref:`Instruction ` :math:`S;C \vdashinstr \instr : \stacktype` +:ref:`Instruction sequence ` :math:`S;C \vdashinstrseq \instr^\ast : \stacktype` :ref:`Expression ` :math:`C \vdashexpr \expr : \resulttype` :ref:`Function ` :math:`C \vdashfunc \func : \functype` :ref:`Table ` :math:`C \vdashtable \table : \tabletype` diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 360b9d84..66dbd618 100644 --- a/document/core/util/macros.def +++ b/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 diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 5dbf44f4..61744233 100644 --- a/document/core/valid/instructions.rst +++ b/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 ` are classified by :ref:`function types ` :math:`[t_1^\ast] \to [t_2^\ast]` -that describe how they manipulate the :ref:`operand stack `. -The types describe the required input stack with argument values of types :math:`t_1^\ast` that an instruction pops off +:ref:`Instructions ` are classified by *stack types* :math:`[t_1^\ast] \to [t_2^\ast]` that describe how instructions manipulate the :ref:`operand 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 `, +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 ` :math:`t`. + * The instruction is valid with type :math:`[t~t~\I32] \to [t]`, for any :ref:`operand type ` :math:`t` that :ref:`matches ` some :ref:`number type `. .. 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 ` :math:`t^\ast`. + for any sequence of :ref:`operand types ` :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 ` :math:`t^\ast` and :math:`t_3^\ast`. * There must be a sequence of :ref:`value types ` :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 ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :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 ` with type :math:`[] \to [t^\ast]`, - for some :ref:`result type ` :math:`[t^\ast]`. +* The instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with some :ref:`stack type ` :math:`[] \to [t'^\ast]`. + +* For each :ref:`operand type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`value type ` type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`. * Then the expression is valid with :ref:`result type ` :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] } diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index aff90b0c..be8097ea 100644 --- a/interpreter/valid/valid.ml +++ b/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 -->... [] diff --git a/test/core/br_table.wast b/test/core/br_table.wast index fc84e2f0..a9649645 100644 --- a/test/core/br_table.wast +++ b/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")) diff --git a/test/core/select.wast b/test/core/select.wast index 61edfd9e..b2098ffc 100644 --- a/test/core/select.wast +++ b/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)) diff --git a/test/core/unreached-invalid.wast b/test/core/unreached-invalid.wast index aeecf28c..3ddd7738 100644 --- a/test/core/unreached-invalid.wast +++ b/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)))