Instructions

Instructions are classified by instruction types that describe how they manipulate the operand stack and initialize locals: A type \({t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast}\) describes the required input stack with argument values of types \({t_1^\ast}\) that an instruction pops off and the provided output stack with result values of types \({t_2^\ast}\) that it pushes back. Moreover, it enumerates the indices \({x^\ast}\) of locals that have been set by the instruction. In most cases, this is empty.

Note

For example, the instruction \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} {.} \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\) has type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\), consuming two \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) values and producing one. The instruction \((\href{../syntax/instructions.html#syntax-instr-variable}{\mathsf{local{.}set}}~x)\) has type \(t \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x} \epsilon\), provided \(t\) is the type declared for the local \(x\).

Typing extends to instruction sequences \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\). Such a sequence has an instruction type \({t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast}\) if the accumulative effect of executing the instructions is consuming values of types \({t_1^\ast}\) off the operand stack, pushing new values of types \({t_2^\ast}\), and setting all locals \({x^\ast}\).

For some instructions, the typing rules do not fully constrain the type, and therefore allow for multiple types. Such instructions are called polymorphic. Two degrees of polymorphism can be distinguished:

  • value-polymorphic: the value type \(t\) of one or several individual operands is unconstrained. That is the case for all parametric instructions like \(\mathsf{drop}\) and \(\mathsf{select}\).

  • stack-polymorphic: the entire (or most of the) instruction type \({t_1^\ast} \rightarrow {t_2^\ast}\) of the instruction is unconstrained. That is the case for all control instructions that perform an unconditional control transfer, such as \(\mathsf{unreachable}\), \(\mathsf{br}\), or \(\mathsf{return}\).

In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they are valid in the current context and meet the constraints imposed for the surrounding parts of the program.

Note

For example, the \(\mathsf{select}\) instruction is valid with type \(t~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow t\), for any possible number type \(t\). Consequently, both instruction sequences

\[(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~1)~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~2)~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~3)~(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}})\]

and

\[(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{+1})~(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{+2})~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~3)~(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}})\]

are valid, with \(t\) in the typing of \(\mathsf{select}\) being instantiated to \(\mathsf{i{\scriptstyle 32}}\) or \(\mathsf{f{\scriptstyle 64}}\), respectively.

The \(\mathsf{unreachable}\) instruction is stack-polymorphic, and hence valid with type \({t_1^\ast} \rightarrow {t_2^\ast}\) for any possible sequences of value types \({t_1^\ast}\) and \({t_2^\ast}\). Consequently,

\[(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}})~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} {.} \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}})\]

is valid by assuming type \(\epsilon \rightarrow \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) for the \(\mathsf{unreachable}\) instruction. In contrast,

\[(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}})~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} {.} \href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}})\]

is invalid, because there is no possible type to pick for the \(\mathsf{unreachable}\) instruction that would make the sequence well-typed.

The Appendix describes a type checking algorithm that efficiently implements validation of instruction sequences as prescribed by the rules given here.

Parametric Instructions

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}}\)

The instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}}\) is valid with the instruction type \(\epsilon~\rightarrow~\epsilon\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}} : \epsilon \rightarrow \epsilon } \qquad \end{array}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}\)

The instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast} \rightarrow {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}} : {t_1^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

Note

The \(\mathsf{unreachable}\) instruction is stack-polymorphic.

\(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}}\)

The instruction \(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}}\) is valid with the instruction type \(t~\rightarrow~\epsilon\) if:

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}} : t \rightarrow \epsilon } \qquad \end{array}\]

Note

Both \(\mathsf{drop}\) and \(\mathsf{select}\) without annotation are value-polymorphic instructions.

\(\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}~(t^\ast)^?\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}~{{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?})\) is valid with the instruction type \(t~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~t\) if:

  • The value type \(t\) is valid.

  • Either:

    • The value type sequence \({{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?}\) is of the form \(t\).

  • Or:

    • The value type sequence \({{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?}\) is absent.

    • The value type \(t\) matches the value type \({t'}\).

    • The value type \({t'}\) is of the form \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) or \({t'}\) is of the form \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}}~t : t~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow t } \qquad \frac{ C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}} \qquad C \href{../valid/matching.html#match-valtype}{\vdash} t \href{../valid/matching.html#match-valtype}{\leq} {t'} \qquad {t'} = {\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}} \lor {t'} = {\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}} : t~t~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow t } \qquad \end{array}\]

Note

In future versions of WebAssembly, \(\mathsf{select}\) may allow more than one value per choice.

Control Instructions

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\href{../syntax/types.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:

  • The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).

  • Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_2^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).

  • Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\mathit{bt}} : {t_1^\ast} \rightarrow {t_2^\ast} \qquad \{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_2^\ast}) \} \oplus C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t_1^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

Note

The notation \(\{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t^\ast}) \} \oplus C\) inserts the new label type at index \(0\), shifting all others. The same applies to all other block instructions.

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~\href{../syntax/types.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast})\) is valid with the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:

  • The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).

  • Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_1^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).

  • Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\mathit{bt}} : {t_1^\ast} \rightarrow {t_2^\ast} \qquad \{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_1^\ast}) \} \oplus C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast} : {t_1^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~\href{../syntax/types.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1^\ast}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast})\) is valid with the instruction type \({t_1^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~{t_2^\ast}\) if:

  • The block type \({\mathit{bt}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\).

  • Let \({C'}\) be the same context as \(C\), but with the result type sequence \({t_2^\ast}\) prepended to the field \(\href{../valid/conventions.html#context}{\mathsf{labels}}\).

  • Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_1^\ast}}\,{t_2^\ast}\).

  • Under the context \({C'}\), the instruction sequence \({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast}\) is valid with the instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_2^\ast}}\,{t_2^\ast}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\mathit{bt}} : {t_1^\ast} \rightarrow {t_2^\ast} \qquad \{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_2^\ast}) \} \oplus C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x_1^\ast}} {t_2^\ast} \qquad \{ \href{../valid/conventions.html#context}{\mathsf{labels}}~({t_2^\ast}) \} \oplus C \href{../valid/instructions.html#valid-instrs}{\vdash} {{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast} : {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x_2^\ast}} {t_2^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~{\mathit{bt}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_1^\ast}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~{{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}_2^\ast} : {t_1^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {t_2^\ast} } \qquad \end{array}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l)\) is valid with the instruction type \({t_1^\ast}~{t^\ast}~\rightarrow~{t_2^\ast}\) if:

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is of the form \({t^\ast}\).

  • The instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast} \qquad C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast} \rightarrow {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l : {t_1^\ast}~{t^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

Note

The label index space in the context \(C\) contains the most recent label first, so that \(C{.}\mathsf{labels}{}[l]\) performs a relative lookup as expected. This applies to other branch instructions as well.

The \(\mathsf{br}\) instruction is stack-polymorphic.

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l)\) is valid with the instruction type \({t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~{t^\ast}\) if:

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is of the form \({t^\ast}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l : {t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {t^\ast} } \qquad \end{array}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~l^\ast~l_N\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~{l^\ast}~{l'})\) is valid with the instruction type \({t_1^\ast}~{t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~{t_2^\ast}\) if:

  • For all \(l\) in \({l^\ast}\):

    • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

    • The result type \({t^\ast}\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\).

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[{l'}]\) exists.

  • The result type \({t^\ast}\) matches the label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[{l'}]\).

  • The instruction type \({t_1^\ast}~{t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\rightarrow~{t_2^\ast}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ (C \href{../valid/matching.html#match-resulttype}{\vdash} {t^\ast} \href{../valid/matching.html#match-resulttype}{\leq} C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l])^\ast \qquad C \href{../valid/matching.html#match-resulttype}{\vdash} {t^\ast} \href{../valid/matching.html#match-resulttype}{\leq} C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[{l'}] \qquad C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast}~{t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~{l^\ast}~{l'} : {t_1^\ast}~{t^\ast}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {t_2^\ast} } \qquad \end{array}\]

Note

The \(\mathsf{br\_table}\) instruction is stack-polymorphic.

Furthermore, the result type \({t^\ast}\) is also chosen non-deterministically in this rule. Although it may seem necessary to compute \({t^\ast}\) as the greatest lower bound of all label types in practice, a simple sequential algorithm does not require this.

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_null}}~l\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_null}}~l)\) is valid with the instruction type \({t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}})~\rightarrow~{t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}})\) if:

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is of the form \({t^\ast}\).

  • The heap type \({\mathit{ht}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast} \qquad C \href{../valid/types.html#valid-heaptype}{\vdash} {\mathit{ht}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_null}}~l : {t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}}) \rightarrow {t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}}) } \qquad \end{array}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_non\_null}}~l\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_non\_null}}~l)\) is valid with the instruction type \({t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}})~\rightarrow~{t^\ast}\) if:

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is of the form \({t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}~{\mathit{ht}})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}~{\mathit{ht}}) }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_non\_null}}~l : {t^\ast}~(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}}) \rightarrow {t^\ast} } \qquad \end{array}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast}}~l~\mathit{rt}_1~\mathit{rt}_2\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast}}~l~{\mathit{rt}}_1~{\mathit{rt}}_2)\) is valid with the instruction type \({t^\ast}~{\mathit{rt}}_1~\rightarrow~{t^\ast}~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}\) if:

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is of the form \({t^\ast}~{\mathit{rt}}\).

  • The reference type \({\mathit{rt}}_1\) is valid.

  • The reference type \({\mathit{rt}}_2\) is valid.

  • The reference type \({\mathit{rt}}_2\) matches the reference type \({\mathit{rt}}_1\).

  • The reference type \({\mathit{rt}}_2\) matches the reference type \({\mathit{rt}}\).

  • The reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}\) is \({\mathit{rt}}_1 \href{../valid/conventions.html#aux-reftypediff}{\setminus} {\mathit{rt}}_2\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l] = {t^\ast}~{\mathit{rt}} \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}}_1 : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\mathit{rt}}_2 : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}}_2 \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}}_1 \qquad C \href{../valid/matching.html#match-reftype}{\vdash} {\mathit{rt}}_2 \href{../valid/matching.html#match-reftype}{\leq} {\mathit{rt}} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast}}~l~{\mathit{rt}}_1~{\mathit{rt}}_2 : {t^\ast}~{\mathit{rt}}_1 \rightarrow {t^\ast}~({\mathit{rt}}_1 \href{../valid/conventions.html#aux-reftypediff}{\setminus} {\mathit{rt}}_2) } \qquad \end{array}\]

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast\_fail}}~l~\mathit{rt}_1~\mathit{rt}_2\)

The instruction \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_on\_cast\_fail}}~l~{\mathit{rt}}_1~{\mathit{rt}}_2)\) is valid with the instruction type \({t^\ast}~{\mathit{rt}}_1~\rightarrow~{t^\ast}~{\mathit{rt}}_2\) if:

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) exists.

  • The label \(C{.}\href{../valid/conventions.html#context}{\mathsf{labels}}{}[l]\) is of the form \({t^\ast}~{\mathit{rt}}\).

  • The reference type \({\mathit{rt}}_1\) is