验证算法¶
WebAssembly 的 验证 规范完全是声明式的。它描述了 模块 或 指令 序列要有效必须满足的约束。
本节概述了用于有效验证代码（即 指令 序列）的健全且完整的算法框架。（验证的其他方面很容易实现。）
实际上，该算法是在 二进制格式 中出现的操作码的扁平序列上表达的，并且只执行一次遍历。因此，它可以被直接集成到解码器中。
该算法是用类型化的伪代码表达的，其语义旨在不言自明。
数据结构¶
类型可以用枚举来表示。
type val_type = I32 | I64 | F32 | F64 | V128 | Funcref | Externref
func is_num(t : val_type | Unknown) : bool =
return t = I32 || t = I64 || t = F32 || t = F64 || t = Unknown
func is_vec(t : val_type | Unknown) : bool =
return t = V128 || t = Unknown
func is_ref(t : val_type | Unknown) : bool =
return t = Funcref || t = Externref || t = Unknown
该算法使用两个独立的堆栈：值堆栈和控制堆栈。前者跟踪 类型 操作数的值在 堆栈 上，后者围绕着 结构化控制指令 及其关联的 块。
type val_stack = stack(val_type | Unknown)
type ctrl_stack = stack(ctrl_frame)
type ctrl_frame = {
opcode : opcode
start_types : list(val_type)
end_types : list(val_type)
height : nat
unreachable : bool
}
对于每个值，值堆栈记录其 值类型，或者当类型未知时记录 Unknown。
对于每个进入的块，控制堆栈记录一个控制帧，其中包含起始操作码，块开始和结束时操作数堆栈顶部的类型（用于检查其结果以及分支），块开始时操作数堆栈的高度（用于检查操作数是否未从当前块下溢），以及记录块的剩余部分是否不可达的标志（用于处理 堆栈多态 类型化后的分支）。
为了呈现算法，操作数堆栈和控制堆栈只是作为全局变量维护的
var vals : val_stack
var ctrls : ctrl_stack
但是，这些变量不是由主检查函数直接操作的，而是通过一组辅助函数操作的
func push_val(type : val_type | Unknown) =
vals.push(type)
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_val(expect : val_type | Unknown) : val_type | Unknown =
let actual = pop_val()
error_if(actual =/= expect && actual =/= Unknown && expect =/= Unknown)
return actual
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.prepend(pop_val(t))
return popped
推送一个操作数值只是将相应的类型推送到值堆栈。
弹出操作数值会检查值堆栈是否未从当前块下溢，然后删除一个类型。但首先，将处理一个特殊情况，即该块不包含任何已知值，但已被标记为不可达。这种情况可能在无条件分支之后发生，此时堆栈被类型化 多态。在这种情况下，将返回一个未知类型。
第二个用于弹出操作数值的函数接受一个预期类型，实际操作数类型将与其进行检查。如果其中一个是 Unknown，则类型可能不同。该函数返回从堆栈中弹出的实际类型。
最后，有用于推送或弹出多个操作数类型的累加函数。
注意
符号 stack[i] 旨在从顶部索引堆栈，因此，例如，ctrls[0] 访问最后推送的元素。
控制堆栈同样通过辅助函数进行操作
func push_ctrl(opcode : opcode, in : list(val_type), out : list(val_type)) =
let frame = ctrl_frame(opcode, in, out, vals.size(), false)
ctrls.push(frame)
push_vals(in)
func pop_ctrl() : ctrl_frame =
error_if(ctrls.is_empty())
let frame = ctrls[0]
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() =
vals.resize(ctrls[0].height)
ctrls[0].unreachable := true
推送控制帧需要标签值和结果值的类型。它分配一个新的帧记录，记录它们以及操作数堆栈的当前高度，并将该块标记为可达。
弹出帧首先检查控制堆栈是否为空。然后，它验证操作数堆栈是否包含退出块末尾预期值的正确类型，并将它们从操作数堆栈中弹出。之后，它检查堆栈是否已缩回其初始高度。
与控制帧关联的 标签 的类型是堆栈在帧开始或结束时的类型，由它起源的操作码决定。
最后，当前帧可以被标记为不可达。在这种情况下，所有现有的操作数类型都将从值堆栈中清除，以允许 pop_val 中的 堆栈多态 逻辑生效。因为每个函数都具有一个隐式的最外层标签，该标签对应于一个隐式的块帧，所以验证算法的一个不变量是，在验证指令时控制堆栈上始终至少有一个帧，因此，ctrls[0] 始终是已定义的。
注意
即使设置了不可达标志，连续操作数仍然被推送到操作数堆栈并从其中弹出。这是为了检测无效的 示例，例如 \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}})~\href{../syntax/types.html#syntax-valtype}{\mathsf{i64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}})\)。但是，多态堆栈不能下溢，而是根据需要生成 Unknown 类型。
操作码序列的验证¶
以下函数展示了对一些代表性的操作指令进行验证，这些操作指令会操作堆栈。其他指令的检查方式类似。
func validate(opcode) =
switch (opcode)
case (i32.add)
pop_val(I32)
pop_val(I32)
push_val(I32)
case (drop)
pop_val()
case (select)
pop_val(I32)
let t1 = pop_val()
let t2 = pop_val()
error_if(not ((is_num(t1) && is_num(t2)) || (is_vec(t1) && is_vec(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_vals([t1*])
push_ctrl(block, [t1*], [t2*])
case (loop t1*->t2*)
pop_vals([t1*])
push_ctrl(loop, [t1*], [t2*])
case (if t1*->t2*)
pop_val(I32)
pop_vals([t1*])
push_ctrl(if, [t1*], [t2*])
case (end)
let frame = pop_ctrl()
push_vals(frame.end_types)
case (else)
let frame = pop_ctrl()
error_if(frame.opcode =/= if)
push_ctrl(else, frame.start_types, frame.end_types)
case (br n)
error_if(ctrls.size() < n)
pop_vals(label_types(ctrls[n]))
unreachable()
case (br_if n)
error_if(ctrls.size() < 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)
error_if(label_types(ctrls[n]).size() =/= arity)
push_vals(pop_vals(label_types(ctrls[n])))
pop_vals(label_types(ctrls[m]))
unreachable()
注意
在当前的 WebAssembly 指令集中，类型为 Unknown 的操作数永远不会在堆栈中重复。如果语言扩展了类似 dup 的堆栈指令，情况就会改变。在这种扩展下，上述算法需要通过用适当的类型变量替换 Unknown 类型来进行改进，以确保所有使用情况都是一致的。