指令¶

指令根据描述指令如何操作操作数栈的栈类型 $[t_{1}^{*}] \to [t_{2}^{*}]$ 进行分类。

\begin{array}{r} \begin{array}{llll} stacktype & ::= & [{opdtype}^{*}] \to [{opdtype}^{*}] \\ opdtype & ::= & valtype | ⊥ \end{array} \end{array}

这些类型描述了指令弹出的具有操作数类型 $t_{1}^{*}$ 的所需输入栈，以及它压入的具有类型 $t_{2}^{*}$ 的结果值的输出栈。栈类型类似于函数类型，但它们允许将单个操作数分类为 $⊥$ （底部），表示类型不受约束。作为一个辅助概念，如果 $t_{1}$ 为 $⊥$ 或等于 $t_{2}$ ，则操作数类型 $t_{1}$ 与另一个操作数类型 $t_{2}$ 匹配。这以逐点的方式扩展到栈类型。

\frac{}{⊢ t \leq t} \frac{}{⊢ ⊥ \leq t}

\frac{(⊢ t \leq t^{'})^{*}}{⊢ [t^{*}] \leq [{t^{'}}^{*}]}

注意

例如，指令 $i 32 . add$ 的类型为 $[i 32 i 32] \to [i 32]$ ，它消耗两个 $i 32$ 值并产生一个值。

类型推导扩展到指令序列 ${instr}^{*}$ 。如果执行指令的累积效果是从操作数栈中消耗类型为 $t_{1}^{*}$ 的值并压入类型为 $t_{2}^{*}$ 的新值，则此序列具有栈类型 $[t_{1}^{*}] \to [t_{2}^{*}]$ 。

对于某些指令，类型规则没有完全约束类型，因此允许多种类型。这样的指令称为多态指令。可以区分两种多态性

值多态：一个或多个单个操作数的值类型 $t$ 不受约束。对于所有参数化指令（如 $drop$ 和 $select$ ）都是这种情况。
栈多态：指令的整个（或大部分）栈类型 $[t_{1}^{*}] \to [t_{2}^{*}]$ 不受约束。对于所有执行无条件控制转移的控制指令（例如 $unreachable$ 、 $br$ 、 $br_table$ 和 $return$ ）都是这种情况。

在这两种情况下，只要满足程序周围部分施加的约束，就可以任意选择不受约束的类型或类型序列。

注意

例如， $select$ 指令对于任何可能的数值类型 $t$ ，都可以使用类型 $[t t i 32] \to [t]$ 。因此，以下两个指令序列

(i 32 . const 1) (i 32 . const 2) (i 32 . const 3) select

和

(f 64 . const 1.0) (f 64 . const 2.0) (i 32 . const 3) select

都是有效的，其中 $select$ 的类型中的 $t$ 分别被实例化为 $i 32$ 或 $f 64$ 。

$unreachable$ 指令对于任何可能的操作数类型 $t_{1}^{*}$ 和 $t_{2}^{*}$ 序列，都具有类型 $[t_{1}^{*}] \to [t_{2}^{*}]$ 。因此，

unreachable i 32 . add

通过为 $unreachable$ 指令假设类型 $[] \to [i 32 i 32]$ 是有效的。相反，

unreachable (i 64 . const 0) i 32 . add

是无效的，因为没有可以为 $unreachable$ 指令选择的类型可以使序列类型正确。

附录描述了一种类型检查算法，该算法有效地实现了此处给定规则规定的指令序列验证。

数值指令¶

$t . const c$ ¶

该指令对于类型 $[] \to [t]$ 是有效的。

\frac{}{C ⊢ t . const c : [] \to [t]}

$t . unop$ ¶

该指令对于类型 $[t] \to [t]$ 是有效的。

\frac{}{C ⊢ t . unop : [t] \to [t]}

$t . binop$ ¶

该指令对于类型 $[t t] \to [t]$ 是有效的。

\frac{}{C ⊢ t . binop : [t t] \to [t]}

$t . testop$ ¶

该指令对于类型 $[t] \to [i 32]$ 是有效的。

\frac{}{C ⊢ t . testop : [t] \to [i 32]}

$t . relop$ ¶

该指令对于类型 $[t t] \to [i 32]$ 是有效的。

\frac{}{C ⊢ t . relop : [t t] \to [i 32]}

$t_{2} . cvtop_t_{1}_{sx}^{?}$ ¶

该指令对于类型 $[t_{1}] \to [t_{2}]$ 是有效的。

\frac{}{C ⊢ t_{2} . cvtop_t_{1}_{sx}^{?} : [t_{1}] \to [t_{2}]}

引用指令¶

$ref . null t$ ¶

该指令对于类型 $[] \to [t]$ 是有效的。

\frac{}{C ⊢ ref . null t : [] \to [t]}

注意

在 WebAssembly 的未来版本中，可能存在不允许空引用的引用类型。

$ref . is_null$ ¶

该指令对于类型 $[t] \to [i 32]$ 是有效的，其中 $t$ 为任何引用类型。

\frac{t = reftype}{C ⊢ ref . is_null : [t] \to [i 32]}

$ref . func x$ ¶

上下文必须定义函数 $C . funcs [x]$ 。
函数索引 $x$ 必须包含在 $C . refs$ 中。
该指令的类型有效，为 $[] \to [funcref]$ 。

\frac{C . funcs [x] = functype x \in C . refs}{C ⊢ ref . func x : [] \to [funcref]}

向量指令¶

向量指令可以带前缀来描述操作数的形状。打包数值类型， $i 8$ 和 $i 16$ ，不是值类型。一个辅助函数将这些打包类型形状映射到值类型。

\begin{array}{r} \begin{array}{llll} unpacked (i 8 x 16) & = & i 32 \\ unpacked (i 16 x 8) & = & i 32 \\ unpacked (t x N) & = & t \end{array} \end{array}

以下辅助函数表示向量形状的车道数，即其维度

\begin{array}{llll} \dim (t x N) & = & N \end{array}

$v 128 . const c$ ¶

该指令的类型有效，为 $[] \to [v 128]$ 。

\frac{}{C ⊢ v 128 . const c : [] \to [v 128]}

$v 128 . vvunop$ ¶

该指令的类型有效，为 $[v 128] \to [v 128]$ 。

\frac{}{C ⊢ v 128 . vvunop : [v 128] \to [v 128]}

$v 128 . vvbinop$ ¶

该指令的类型有效，为 $[v 128 v 128] \to [v 128]$ 。

\frac{}{C ⊢ v 128 . vvbinop : [v 128 v 128] \to [v 128]}

$v 128 . vvternop$ ¶

该指令的类型有效，为 $[v 128 v 128 v 128] \to [v 128]$ 。

\frac{}{C ⊢ v 128 . vvternop : [v 128 v 128 v 128] \to [v 128]}

$v 128 . vvtestop$ ¶

该指令的类型有效，为 $[v 128] \to [i 32]$ 。

\frac{}{C ⊢ v 128 . vvtestop : [v 128] \to [i 32]}

$i 8 x 16. swizzle$ ¶

该指令的类型有效，为 $[v 128 v 128] \to [v 128]$ 。

\frac{}{C ⊢ i 8 x 16. swizzle : [v 128 v 128] \to [v 128]}

$i 8 x 16. shuffle {laneidx}^{16}$ ¶

对于所有 ${laneidx}_{i}$ ，在 ${laneidx}^{16}$ 中， ${laneidx}_{i}$ 必须小于 $32$ 。
该指令的类型有效，为 $[v 128 v 128] \to [v 128]$ 。

\frac{(laneidx < 32)^{16}}{C ⊢ i 8 x 16. shuffle {laneidx}^{16} : [v 128 v 128] \to [v 128]}

$shape . splat$ ¶

令 $t$ 为 $unpacked (shape)$ 。
该指令的类型有效，为 $[t] \to [v 128]$ 。

\frac{}{C ⊢ shape . splat : [unpacked (shape)] \to [v 128]}

$shape . extract_lane_{sx}^{?} laneidx$ ¶

车道索引 $laneidx$ 必须小于 $\dim (shape)$ 。
该指令的类型有效，为 $[v 128] \to [unpacked (shape)]$ 。

\frac{laneidx < \dim (shape)}{C ⊢ shape . extract_lane_{sx}^{?} laneidx : [v 128] \to [unpacked (shape)]}

$shape . replace_lane laneidx$ ¶

车道索引 $laneidx$ 必须小于 $\dim (shape)$ 。
令 $t$ 为 $unpacked (shape)$ 。
该指令的类型有效，为 $[v 128 t] \to [v 128]$ 。

\frac{laneidx < \dim (shape)}{C ⊢ shape . replace_lane laneidx : [v 128 unpacked (shape)] \to [v 128]}

$shape . vunop$ ¶

该指令的类型有效，为 $[v 128] \to [v 128]$ 。

\frac{}{C ⊢ shape . vunop : [v 128] \to [v 128]}

$shape . vbinop$ ¶

该指令的类型有效，为 $[v 128 v 128] \to [v 128]$ 。

\frac{}{C ⊢ shape . vbinop : [v 128 v 128] \to [v 128]}

$shape . vrelop$ ¶

该指令的类型有效，为 $[v 128 v 128] \to [v 128]$ 。

\frac{}{C ⊢ shape . vrelop : [v 128 v 128] \to [v 128]}

$ishape . vishiftop$ ¶

该指令的类型有效，为 $[v 128 i 32] \to [v 128]$ 。

\frac{}{C ⊢ ishape . vishiftop : [v 128 i 32] \to [v 128]}

$shape . vtestop$ ¶

该指令的类型有效，为 $[v 128] \to [i 32]$ 。

\frac{}{C ⊢ shape . vtestop : [v 128] \to [i 32]}

$shape . vcvtop_{half}^{?}_shape_{sx}^{?} {_zero}^{?}$ ¶

该指令的类型有效，为 $[v 128] \to [v 128]$ 。

\frac{}{C ⊢ shape . vcvtop_{half}^{?}_shape_{sx}^{?} {_zero}^{?} : [v 128] \to [v 128]}

${ishape}_{1} . narrow_{ishape}_{2}_sx$ ¶

该指令的类型有效，为 $[v 128 v 128] \to [v 128]$ 。

\frac{}{C ⊢ {ishape}_{1} . narrow_{ishape}_{2}_sx : [v 128 v 128] \to [v 128]}

$ishape . bitmask$ ¶

该指令的类型有效，为 $[v 128] \to [i 32]$ 。

\frac{}{C ⊢ ishape . bitmask : [v 128] \to [i 32]}

${ishape}_{1} . dot_{ishape}_{2}_s$ ¶

该指令的类型有效，为 $[v 128 v 128] \to [v 128]$ 。

\frac{}{C ⊢ {ishape}_{1} . dot_{ishape}_{2}_s : [v 128 v 128] \to [v 128]}

${ishape}_{1} . extmul_half_{ishape}_{2}_sx$ ¶

该指令的类型有效，为 $[v 128 v 128] \to [v 128]$ 。

\frac{}{C ⊢ {ishape}_{1} . extmul_half_{ishape}_{2}_sx : [v 128 v 128] \to [v 128]}

${ishape}_{1} . extadd_pairwise_{ishape}_{2}_sx$ ¶

该指令的类型有效，为 $[v 128] \to [v 128]$ 。

\frac{}{C ⊢ {ishape}_{1} . extadd_pairwise_{ishape}_{2}_sx : [v 128] \to [v 128]}

参数化指令¶

$drop$ ¶

该指令对于任何操作数类型 $t$ ，其类型有效值为 $[t] \to []$ 。

\frac{}{C ⊢ drop : [t] \to []}

注意

未带注释的 $drop$ 和 $select$ 都是值多态指令。

$select (t^{*})^{?}$ ¶

如果存在 $t^{*}$ ，则
- $t^{*}$ 的长度必须为 $1$ 。
- 则该指令类型有效值为 $[t^{*} t^{*} i 32] \to [t^{*}]$ 。
否则
- 该指令对于任何操作数类型 $t$ （其匹配某些数字类型或向量类型），其类型有效值为 $[t t i 32] \to [t]$ 。

\frac{}{C ⊢ select t : [t t i 32] \to [t]} \frac{⊢ t \leq numtype}{C ⊢ select : [t t i 32] \to [t]} \frac{⊢ t \leq vectype}{C ⊢ select : [t t i 32] \to [t]}

注意

在 WebAssembly 的未来版本中， $select$ 可能会允许每个选项有多个值。

变量指令¶

$local . get x$ ¶

局部变量 $C . locals [x]$ 必须在上下文中定义。
令 $t$ 为值类型 $C . locals [x]$ 。
则该指令类型有效值为 $[] \to [t]$ 。

\frac{C . locals [x] = t}{C ⊢ local . get x : [] \to [t]}

$local . set x$ ¶

局部变量 $C . locals [x]$ 必须在上下文中定义。
令 $t$ 为值类型 $C . locals [x]$ 。
则该指令类型有效值为 $[t] \to []$ 。

\frac{C . locals [x] = t}{C ⊢ local . set x : [t] \to []}

$local . tee x$ ¶

局部变量 $C . locals [x]$ 必须在上下文中定义。
令 $t$ 为值类型 $C . locals [x]$ 。
则该指令类型有效值为 $[t] \to [t]$ 。

\frac{C . locals [x] = t}{C ⊢ local . tee x : [t] \to [t]}

$global . get x$ ¶

全局变量 $C . globals [x]$ 必须在上下文中定义。
令 $mut t$ 为全局类型 $C . globals [x]$ 。
则该指令类型有效值为 $[] \to [t]$ 。

\frac{C . globals [x] = mut t}{C ⊢ global . get x : [] \to [t]}

$global . set x$ ¶

全局变量 $C . globals [x]$ 必须在上下文中定义。
令 $mut t$ 为全局类型 $C . globals [x]$ 。
可变性 $mut$ 必须为 $var$ 。
则该指令类型有效值为 $[t] \to []$ 。

\frac{C . globals [x] = var t}{C ⊢ global . set x : [t] \to []}

表指令¶

$table . get x$ ¶

表 $C . tables [x]$ 必须在上下文中定义。
令 $limits t$ 为表类型 $C . tables [x]$ 。
则该指令类型有效值为 $[i 32] \to [t]$ 。

\frac{C . tables [x] = limits t}{C ⊢ table . get x : [i 32] \to [t]}

$table . set x$ ¶

表 $C . tables [x]$ 必须在上下文中定义。
令 $limits t$ 为表类型 $C . tables [x]$ 。
则该指令的类型为 $[i 32 t] \to []$ 时有效。

\frac{C . tables [x] = limits t}{C ⊢ table . set x : [i 32 t] \to []}

$table . size x$ ¶

表 $C . tables [x]$ 必须在上下文中定义。
则该指令的类型为 $[] \to [i 32]$ 时有效。

\frac{C . tables [x] = tabletype}{C ⊢ table . size x : [] \to [i 32]}

$table . grow x$ ¶

表 $C . tables [x]$ 必须在上下文中定义。
令 $limits t$ 为表类型 $C . tables [x]$ 。
则该指令的类型为 $[t i 32] \to [i 32]$ 时有效。

\frac{C . tables [x] = limits t}{C ⊢ table . grow x : [t i 32] \to [i 32]}

$table . fill x$ ¶

表 $C . tables [x]$ 必须在上下文中定义。
令 $limits t$ 为表类型 $C . tables [x]$ 。
则该指令的类型为 $[i 32 t i 32] \to []$ 时有效。

\frac{C . tables [x] = limits t}{C ⊢ table . fill x : [i 32 t i 32] \to []}

$table . copy x y$ ¶

表 $C . tables [x]$ 必须在上下文中定义。
令 ${limits}_{1} t_{1}$ 为表类型 $C . tables [x]$ 。
表 $C . tables [y]$ 必须在上下文中定义。
令 ${limits}_{2} t_{2}$ 为表类型 $C . tables [y]$ 。
引用类型 $t_{1}$ 必须与 $t_{2}$ 相同。
则该指令的类型为 $[i 32 i 32 i 32] \to []$ 时有效。

\frac{C . tables [x] = {limits}_{1} t C . tables [y] = {limits}_{2} t}{C ⊢ table . copy x y : [i 32 i 32 i 32] \to []}

$table . init x y$ ¶

表 $C . tables [x]$ 必须在上下文中定义。
令 $limits t_{1}$ 为表类型 $C . tables [x]$ 。
元素段 $C . elems [y]$ 必须在上下文中定义。
令 $t_{2}$ 为引用类型 $C . elems [y]$ 。
引用类型 $t_{1}$ 必须与 $t_{2}$ 相同。
则该指令的类型为 $[i 32 i 32 i 32] \to []$ 时有效。

\frac{C . tables [x] = limits t C . elems [y] = t}{C ⊢ table . init x y : [i 32 i 32 i 32] \to []}

$elem . drop x$ ¶

元素段 $C . elems [x]$ 必须在上下文中定义。
则该指令的类型为 $[] \to []$ 时有效。

\frac{C . elems [x] = t}{C ⊢ elem . drop x : [] \to []}

内存指令¶

$t . load memarg$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
对齐 $2^{memarg . align}$ 不能大于 $t$ 的位宽除以 $8$ 。
则该指令类型有效值为 $[i 32] \to [t]$ 。

\frac{C . mems [0] = memtype 2^{memarg . align} \leq | t | / 8}{C ⊢ t . load memarg : [i 32] \to [t]}

$t . load N_sx memarg$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
对齐 $2^{memarg . align}$ 不能大于 $N / 8$ 。
则该指令类型有效值为 $[i 32] \to [t]$ 。

\frac{C . mems [0] = memtype 2^{memarg . align} \leq N / 8}{C ⊢ t . load N_sx memarg : [i 32] \to [t]}

$t . store memarg$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
对齐 $2^{memarg . align}$ 不能大于 $t$ 的位宽除以 $8$ 。
则该指令的类型为 $[i 32 t] \to []$ 时有效。

\frac{C . mems [0] = memtype 2^{memarg . align} \leq | t | / 8}{C ⊢ t . store memarg : [i 32 t] \to []}

$t . store N memarg$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
对齐 $2^{memarg . align}$ 不能大于 $N / 8$ 。
则该指令的类型为 $[i 32 t] \to []$ 时有效。

\frac{C . mems [0] = memtype 2^{memarg . align} \leq N / 8}{C ⊢ t . store N memarg : [i 32 t] \to []}

$v 128. load N x M_sx memarg$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
对齐 $2^{memarg . align}$ 不能大于 $N / 8 \cdot M$ 。
则该指令的类型为 $[i 32] \to [v 128]$ 时有效。

\frac{C . mems [0] = memtype 2^{memarg . align} \leq N / 8 \cdot M}{C ⊢ v 128. load N x M_sx memarg : [i 32] \to [v 128]}

$v 128. load N_splat memarg$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
对齐 $2^{memarg . align}$ 不能大于 $N / 8$ 。
则该指令的类型为 $[i 32] \to [v 128]$ 时有效。

\frac{C . mems [0] = memtype 2^{memarg . align} \leq N / 8}{C ⊢ v 128. load N_splat memarg : [i 32] \to [v 128]}

$v 128. load N_zero memarg$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
对齐 $2^{memarg . align}$ 不能大于 $N / 8$ 。
则该指令的类型为 $[i 32] \to [v 128]$ 时有效。

\frac{C . mems [0] = memtype 2^{memarg . align} \leq N / 8}{C ⊢ v 128. load N_zero memarg : [i 32] \to [v 128]}

$v 128. load N_lane memarg laneidx$ ¶

通道索引 $laneidx$ 必须小于 $128 / N$ 。
内存 $C . mems [0]$ 必须在上下文中定义。
对齐 $2^{memarg . align}$ 不能大于 $N / 8$ 。
然后，该指令的类型有效，为 $[i 32 v 128] \to [v 128]$ 。

\frac{laneidx < 128 / N C . mems [0] = memtype 2^{memarg . align} \leq N / 8}{C ⊢ v 128. load N_lane memarg laneidx : [i 32 v 128] \to [v 128]}

$v 128. store N_lane memarg laneidx$ ¶

通道索引 $laneidx$ 必须小于 $128 / N$ 。
内存 $C . mems [0]$ 必须在上下文中定义。
对齐 $2^{memarg . align}$ 不能大于 $N / 8$ 。
然后，该指令的类型有效，为 $[i 32 v 128] \to [v 128]$ 。

\frac{laneidx < 128 / N C . mems [0] = memtype 2^{memarg . align} \leq N / 8}{C ⊢ v 128. store N_lane memarg laneidx : [i 32 v 128] \to []}

$memory . size$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
则该指令的类型为 $[] \to [i 32]$ 时有效。

\frac{C . mems [0] = memtype}{C ⊢ memory . size : [] \to [i 32]}

$memory . grow$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
然后，该指令的类型有效，为 $[i 32] \to [i 32]$ 。

\frac{C . mems [0] = memtype}{C ⊢ memory . grow : [i 32] \to [i 32]}

$memory . fill$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
则该指令的类型为 $[i 32 i 32 i 32] \to []$ 时有效。

\frac{C . mems [0] = memtype}{C ⊢ memory . fill : [i 32 i 32 i 32] \to []}

$memory . copy$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
则该指令的类型为 $[i 32 i 32 i 32] \to []$ 时有效。

\frac{C . mems [0] = memtype}{C ⊢ memory . copy : [i 32 i 32 i 32] \to []}

$memory . init x$ ¶

内存 $C . mems [0]$ 必须在上下文中定义。
数据段 $C . datas [x]$ 必须在上下文中定义。
则该指令的类型为 $[i 32 i 32 i 32] \to []$ 时有效。

\frac{C . mems [0] = memtype C . datas [x] = ok}{C ⊢ memory . init x : [i 32 i 32 i 32] \to []}

$data . drop x$ ¶

数据段 $C . datas [x]$ 必须在上下文中定义。
则该指令的类型为 $[] \to []$ 时有效。

\frac{C . datas [x] = ok}{C ⊢ data . drop x : [] \to []}

控制指令¶

$nop$ ¶

该指令的类型有效，为 $[] \to []$ 。

\frac{}{C ⊢ nop : [] \to []}

$unreachable$ ¶

该指令的类型有效，为 $[t_{1}^{*}] \to [t_{2}^{*}]$ ，对于任何操作数类型序列 operand types $t_{1}^{*}$ 和 $t_{2}^{*}$ 。

\frac{}{C ⊢ unreachable : [t_{1}^{*}] \to [t_{2}^{*}]}

注意

$unreachable$ 指令是 stack-polymorphic 的。

$block blocktype {instr}^{*} end$ ¶

块类型必须作为某个函数类型 function type $[t_{1}^{*}] \to [t_{2}^{*}]$ 有效。
令 $C^{'}$ 与 $C$ 为相同的上下文 context，但将结果类型 result type $[t_{2}^{*}]$ 添加到 $labels$ 向量的前端。
在上下文 $C^{'}$ 下，指令序列 ${instr}^{*}$ 必须有效，其类型为 $[t_{1}^{*}] \to [t_{2}^{*}]$ 。
然后，复合指令的类型有效，为 $[t_{1}^{*}] \to [t_{2}^{*}]$ 。

\frac{C ⊢ blocktype : [t_{1}^{*}] \to [t_{2}^{*}] C, labels [t_{2}^{*}] ⊢ {instr}^{*} : [t_{1}^{*}] \to [t_{2}^{*}]}{C ⊢ block blocktype {instr}^{*} end : [t_{1}^{*}] \to [t_{2}^{*}]}

注意

符号 $C, labels [t^{*}]$ 将新的标签类型插入索引 $0$ 处，并将所有其他标签类型向后移动。notation

$loop blocktype {instr}^{*} end$ ¶

块类型必须作为某个函数类型 function type $[t_{1}^{*}] \to [t_{2}^{*}]$ 有效。
令 $C^{'}$ 与 $C$ 为相同的上下文 context，但将结果类型 result type $[t_{1}^{*}]$ 添加到 $labels$ 向量的前端。
在上下文 $C^{'}$ 下，指令序列 ${instr}^{*}$ 必须有效，其类型为 $[t_{1}^{*}] \to [t_{2}^{*}]$ 。
然后，复合指令的类型有效，为 $[t_{1}^{*}] \to [t_{2}^{*}]$ 。

\frac{C ⊢ blocktype : [t_{1}^{*}] \to [t_{2}^{*}] C, labels [t_{1}^{*}] ⊢ {instr}^{*} : [t_{1}^{*}] \to [t_{2}^{*}]}{C ⊢ loop blocktype {instr}^{*} end : [t_{1}^{*}] \to [t_{2}^{*}]}

注意

符号 $C, labels [t^{*}]$ 将新的标签类型插入索引 $0$ 处，并将所有其他标签类型向后移动。notation

$if blocktype {instr}_{1}^{} else {instr}_{2}^{} end$ ¶

块类型必须作为某个函数类型 function type $[t_{1}^{*}] \to [t_{2}^{*}]$ 有效。
令 $C^{'}$ 与 $C$ 为相同的上下文 context，但将结果类型 result type $[t_{2}^{*}]$ 添加到 $labels$ 向量的前端。
在上下文 $C^{'}$ 下，指令序列 ${instr}_{1}^{*}$ 必须有效，其类型为 $[t_{1}^{*}] \to [t_{2}^{*}]$ 。
在上下文 $C^{'}$ 下，指令序列 ${instr}_{2}^{*}$ 必须有效，其类型为 $[t_{1}^{*}] \to [t_{2}^{*}]$ 。
然后，复合指令的类型有效，为 $[t_{1}^{*} i 32] \to [t_{2}^{*}]$ 。

\frac{C ⊢ blocktype : [t_{1}^{*}] \to [t_{2}^{*}] C, labels [t_{2}^{*}] ⊢ {instr}_{1}^{*} : [t_{1}^{*}] \to [t_{2}^{*}] C, labels [t_{2}^{*}] ⊢ {instr}_{2}^{*} : [t_{1}^{*}] \to [t_{2}^{*}]}{C ⊢ if blocktype {instr}_{1}^{*} else {instr}_{2}^{*} end : [t_{1}^{*} i 32] \to [t_{2}^{*}]}

注意

符号 $C, labels [t^{*}]$ 将新的标签类型插入索引 $0$ 处，并将所有其他标签类型向后移动。notation

$br l$ ¶

标签 $C . labels [l]$ 必须在上下文中定义。
令 $[t^{*}]$ 为结果类型 $C . labels [l]$ 。
则该指令对于任何操作数类型序列 $t_{1}^{*}$ 和 $t_{2}^{*}$ ，其类型有效，为 $[t_{1}^{*} t^{*}] \to [t_{2}^{*}]$ 。

\frac{C . labels [l] = [t^{*}]}{C ⊢ br l : [t_{1}^{*} t^{*}] \to [t_{2}^{*}]}

注意

上下文 $C$ 中的标签索引空间将最新的标签放在最前面，以便 $C . labels [l]$ 按预期执行相对查找。

$br$ 指令是栈多态的。

$br_if l$ ¶

标签 $C . labels [l]$ 必须在上下文中定义。
令 $[t^{*}]$ 为结果类型 $C . labels [l]$ 。
则该指令类型有效，为 $[t^{*} i 32] \to [t^{*}]$ 。

\frac{C . labels [l] = [t^{*}]}{C ⊢ br_if l : [t^{*} i 32] \to [t^{*}]}

注意

上下文 $C$ 中的标签索引空间将最新的标签放在最前面，以便 $C . labels [l]$ 按预期执行相对查找。

$br_table l^{*} l_{N}$ ¶

标签 $C . labels [l_{N}]$ 必须在上下文中定义。
对于 $l^{*}$ 中的每个标签 $l_{i}$ ，标签 $C . labels [l_{i}]$ 必须在上下文中定义。
必须存在一个操作数类型序列 $t^{*}$ ，使得
- 序列 $t^{*}$ 的长度与序列 $C . labels [l_{N}]$ 的长度相同。
- 对于 $t^{*}$ 中的每个操作数类型 $t_{j}$ 和 $C . labels [l_{N}]$ 中对应的类型 $t_{N j}^{'}$ ， $t_{j}$ 匹配 $t_{N j}^{'}$ 。
- 对于 $l^{*}$ 中的每个标签 $l_{i}$
  - 序列 $t^{*}$ 的长度与序列 $C . labels [l_{i}]$ 的长度相同。
  - 对于 $t^{*}$ 中的每个操作数类型 $t_{j}$ 和 $C . labels [l_{i}]$ 中对应的类型 $t_{i j}^{'}$ ， $t_{j}$ 匹配 $t_{i j}^{'}$ 。
则该指令对于任何操作数类型序列 $t_{1}^{*}$ 和 $t_{2}^{*}$ ，其类型有效，为 $[t_{1}^{*} t^{*} i 32] \to [t_{2}^{*}]$ 。

\frac{(⊢ [t^{*}] \leq C . labels [l])^{*} ⊢ [t^{*}] \leq C . labels [l_{N}]}{C ⊢ br_table l^{*} l_{N} : [t_{1}^{*} t^{*} i 32] \to [t_{2}^{*}]}

注意

上下文 $C$ 中的标签索引空间将最新的标签放在最前面，以便 $C . labels [l_{i}]$ 按预期执行相对查找。

$br_table$ 指令是栈多态的。

$return$ ¶

返回类型 $C . return$ 在上下文中不能缺失。
令 $[t^{*}]$ 为 $C . return$ 的结果类型。
则该指令对于任何操作数类型序列 $t_{1}^{*}$ 和 $t_{2}^{*}$ ，其类型有效，为 $[t_{1}^{*} t^{*}] \to [t_{2}^{*}]$ 。

\frac{C . return = [t^{*}]}{C ⊢ return : [t_{1}^{*} t^{*}] \to [t_{2}^{*}]}

注意

$return$ 指令是栈多态的。

在验证不是函数体的表达式时， $C . return$ 缺失（设置为 $ϵ$ ）。这与将其设置为空结果类型 ( $[ϵ]$ ) 不同，后者是对于不返回任何内容的函数的情况。

$call x$ ¶

上下文必须定义函数 $C . funcs [x]$ 。
则该指令类型有效，为 $C . funcs [x]$ 。

\frac{C . funcs [x] = [t_{1}^{*}] \to [t_{2}^{*}]}{C ⊢ call x : [t_{1}^{*}] \to [t_{2}^{*}]}

$call_indirect x y$ ¶

表 $C . tables [x]$ 必须在上下文中定义。
令 $limits t$ 为表类型 $C . tables [x]$ 。
引用类型 $t$ 必须为 $funcref$ 。
类型 $C . types [y]$ 必须在上下文中定义。
令 $[t_{1}^{*}] \to [t_{2}^{*}]$ 为函数类型 $C . types [y]$ 。
则该指令类型有效，为 $[t_{1}^{*} i 32] \to [t_{2}^{*}]$ 。

\frac{C . tables [x] = limits funcref C . types [y] = [t_{1}^{*}] \to [t_{2}^{*}]}{C ⊢ call_indirect x y : [t_{1}^{*} i 32] \to [t_{2}^{*}]}

指令序列¶

指令序列的类型化是递归定义的。

空指令序列： $ϵ$ ¶

空指令序列对于任何操作数类型序列 $t^{*}$ ，其类型有效，为 $[t^{*}] \to [t^{*}]$ 。

\frac{}{C ⊢ ϵ : [t^{*}] \to [t^{*}]}

非空指令序列： ${instr}^{*} {instr}_{N}$ ¶

指令序列 ${instr}^{*}$ 必须对于某些操作数类型序列 $t_{1}^{*}$ 和 $t_{2}^{*}$ ，其类型有效，为 $[t_{1}^{*}] \to [t_{2}^{*}]$ 。
指令 ${instr}_{N}$ 必须对于某些操作数类型序列 $t^{*}$ 和 $t_{3}^{*}$ ，其类型有效，为 $[t^{*}] \to [t_{3}^{*}]$ 。
必须存在一个操作数类型序列 $t_{0}^{*}$ ，使得 $t_{2}^{*} = t_{0}^{*} {t^{'}}^{*}$ ，其中类型序列 ${t^{'}}^{*}$ 与 $t^{*}$ 一样长。
对于 ${t^{'}}^{*}$ 中的每个操作数类型 $t_{i}^{'}$ 和 $t^{*}$ 中对应的类型 $t_{i}$ ， $t_{i}^{'}$ 匹配 $t_{i}$ 。
则组合后的指令序列类型有效，为 $[t_{1}^{*}] \to [t_{0}^{*} t_{3}^{*}]$ 。

\frac{C ⊢ {instr}^{*} : [t_{1}^{*}] \to [t_{0}^{*} {t^{'}}^{*}] ⊢ [{t^{'}}^{*}] \leq [t^{*}] C ⊢ {instr}_{N} : [t^{*}] \to [t_{3}^{*}]}{C ⊢ {instr}^{*} {instr}_{N} : [t_{1}^{*}] \to [t_{0}^{*} t_{3}^{*}]}

表达式¶

表达式 $expr$ 由结果类型分类，结果类型的形式为 $[t^{*}]$ 。

${instr}^{*} end$ ¶

指令序列 ${instr}^{*}$ 必须是有效的，并具有某种栈类型 $[] \to [{t^{'}}^{*}]$ 。
对于 ${t^{'}}^{*}$ 中的每个操作数类型 $t_{i}^{'}$ 以及 $t^{*}$ 中对应的值类型 $t_{i}$ ， $t_{i}^{'}$ 匹配 $t_{i}$ 。
然后，表达式对于结果类型 $[t^{*}]$ 是有效的。

\frac{C ⊢ {instr}^{*} : [] \to [{t^{'}}^{*}] ⊢ [{t^{'}}^{*}] \leq [t^{*}]}{C ⊢ {instr}^{*} end : [t^{*}]}

常量表达式¶

在常量表达式 ${instr}^{*} end$ 中， ${instr}^{*}$ 中的所有指令都必须是常量。
常量指令 $instr$ 必须是
- 形式为 $t . const c$ ，
- 或形式为 $ref . null$ ，
- 或形式为 $ref . func x$ ，
- 或形式为 $global . get x$ ，在这种情况下， $C . globals [x]$ 必须是形式为 $const t$ 的全局类型。

\frac{(C ⊢ instr const)^{*}}{C ⊢ {instr}^{*} end const}

\frac{}{C ⊢ t . const c const} \frac{}{C ⊢ ref . null t const} \frac{}{C ⊢ ref . func x const}

\frac{C . globals [x] = const t}{C ⊢ global . get x const}

注意

目前，出现在全局变量、元素或数据段中的常量表达式受到进一步的约束，其中包含的 $global . get$ 指令仅允许引用导入的全局变量。这在模块验证规则中通过相应地约束上下文 $C$ 来执行。

常量表达式的定义可能会在 WebAssembly 的未来版本中扩展。

指令¶

数值指令¶

t.const c¶

t.unop¶

t.binop¶

t.testop¶

t.relop¶

t2.cvtop_t1_sx?¶

引用指令¶

ref.null t¶

ref.is_null¶

ref.func x¶

向量指令¶

v128.const c¶

v128.vvunop¶

v128.vvbinop¶

v128.vvternop¶

v128.vvtestop¶

i8x16.swizzle¶

i8x16.shuffle laneidx16¶

shape.splat¶

shape.extract_lane_sx? laneidx¶

shape.replace_lane laneidx¶

shape.vunop¶

shape.vbinop¶

shape.vrelop¶

ishape.vishiftop¶

shape.vtestop¶

shape.vcvtop_half?_shape_sx?_zero?¶

ishape1.narrow_ishape2_sx¶

ishape.bitmask¶

ishape1.dot_ishape2_s¶

ishape1.extmul_half_ishape2_sx¶

ishape1.extadd_pairwise_ishape2_sx¶

参数化指令¶

drop¶

select (t∗)?¶

变量指令¶

local.get x¶

local.set x¶

local.tee x¶

global.get x¶

global.set x¶

表指令¶

table.get x¶

table.set x¶

table.size x¶

table.grow x¶

table.fill x¶

table.copy x y¶

table.init x y¶

elem.drop x¶

内存指令¶

t.load memarg¶

t.loadN_sx memarg¶

t.store memarg¶

t.storeN memarg¶

v128.loadNxM_sx memarg¶

v128.loadN_splat memarg¶

v128.loadN_zero memarg¶

v128.loadN_lane memarg laneidx¶

v128.storeN_lane memarg laneidx¶

memory.size¶

memory.grow¶

memory.fill¶

memory.copy¶

memory.init x¶

data.drop x¶

控制指令¶

nop¶

unreachable¶

block blocktype instr∗ end¶

loop blocktype instr∗ end¶

if blocktype instr1∗ else instr2∗ end¶

br l¶

br_if l¶

br_table l∗ lN¶

return¶

call x¶

call_indirect x y¶

$t . const c$ ¶

$t . unop$ ¶

$t . binop$ ¶

$t . testop$ ¶

$t . relop$ ¶

$t_{2} . cvtop_t_{1}_{sx}^{?}$ ¶

$ref . null t$ ¶

$ref . is_null$ ¶

$ref . func x$ ¶

$v 128 . const c$ ¶

$v 128 . vvunop$ ¶

$v 128 . vvbinop$ ¶

$v 128 . vvternop$ ¶

$v 128 . vvtestop$ ¶

$i 8 x 16. swizzle$ ¶

$i 8 x 16. shuffle {laneidx}^{16}$ ¶

$shape . splat$ ¶

$shape . extract_lane_{sx}^{?} laneidx$ ¶

$shape . replace_lane laneidx$ ¶

$shape . vunop$ ¶

$shape . vbinop$ ¶

$shape . vrelop$ ¶

$ishape . vishiftop$ ¶

$shape . vtestop$ ¶

$shape . vcvtop_{half}^{?}_shape_{sx}^{?} {_zero}^{?}$ ¶

${ishape}_{1} . narrow_{ishape}_{2}_sx$ ¶

$ishape . bitmask$ ¶

${ishape}_{1} . dot_{ishape}_{2}_s$ ¶

${ishape}_{1} . extmul_half_{ishape}_{2}_sx$ ¶

${ishape}_{1} . extadd_pairwise_{ishape}_{2}_sx$ ¶

$drop$ ¶

$select (t^{*})^{?}$ ¶

$local . get x$ ¶

$local . set x$ ¶

$local . tee x$ ¶

$global . get x$ ¶

$global . set x$ ¶

$table . get x$ ¶

$table . set x$ ¶

$table . size x$ ¶

$table . grow x$ ¶

$table . fill x$ ¶

$table . copy x y$ ¶

$table . init x y$ ¶

$elem . drop x$ ¶

$t . load memarg$ ¶

$t . load N_sx memarg$ ¶

$t . store memarg$ ¶

$t . store N memarg$ ¶

$v 128. load N x M_sx memarg$ ¶

$v 128. load N_splat memarg$ ¶

$v 128. load N_zero memarg$ ¶

$v 128. load N_lane memarg laneidx$ ¶

$v 128. store N_lane memarg laneidx$ ¶

$memory . size$ ¶

$memory . grow$ ¶

$memory . fill$ ¶

$memory . copy$ ¶

$memory . init x$ ¶

$data . drop x$ ¶

$nop$ ¶

$unreachable$ ¶

$block blocktype {instr}^{*} end$ ¶

$loop blocktype {instr}^{*} end$ ¶

$if blocktype {instr}_{1}^{} else {instr}_{2}^{} end$ ¶

$br l$ ¶

$br_if l$ ¶

$br_table l^{*} l_{N}$ ¶

$return$ ¶

$call x$ ¶

$call_indirect x y$ ¶

空指令序列： $ϵ$ ¶

非空指令序列： ${instr}^{*} {instr}_{N}$ ¶

${instr}^{*} end$ ¶