约定

当实例化模块或调用结果模块实例上的导出函数时，WebAssembly 代码会被执行。

执行行为是根据一个模拟程序状态的抽象机来定义的。它包括一个堆栈，用于记录操作数的值和控制结构，以及一个包含全局状态的抽象存储。

对于每条指令，都有一个规则指定其执行对程序状态的影响。此外，还有一些规则描述了模块的实例化。与验证一样，所有规则都以两种等效的形式给出

  1. 以散文形式，以直观的形式描述执行。

  2. 以形式符号形式，以数学形式描述规则。 [1]

注意

与验证一样，散文和形式规则是等效的，因此不需要理解形式符号就可以阅读本规范。形式主义以在编程语言语义中广泛使用的符号提供了更简洁的描述，并且很容易进行数学证明。

散文符号

执行是通过对指令的每条抽象语法的风格化、逐步规则来指定的。在陈述这些规则时采用了以下约定。

  • 执行规则隐式地假定给定的存储 \(S\)。

  • 执行规则还假设存在一个隐式堆栈，该堆栈通过推入或弹出值、标签和帧来修改。

  • 某些规则要求堆栈至少包含一个帧。最新的帧称为当前帧。

  • 存储和当前帧都通过替换它们的某些组件来进行变异。假定这种替换是全局应用的。

  • 指令的执行可能会陷阱，在这种情况下，整个计算会被中止，并且不会对其进行任何进一步的存储修改。（之后仍然可以启动其他计算。）

  • 指令的执行也可能以跳转到指定的目标而结束，该目标定义了要执行的下一条指令。

  • 执行可以进入和退出形成块的指令序列。

  • 指令序列隐式地按顺序执行，除非发生陷阱或跳转。

  • 在各种地方，规则包含表达程序状态的关键不变式的断言。

形式符号

注意

本节简要说明了正式指定执行的符号。对于感兴趣的读者，可以在相应的教科书中找到更详细的介绍。 [2]

正式执行规则使用一种标准方法来指定操作语义，将其呈现为归约规则。每个规则都具有以下一般形式

\[\mathit{配置} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad \mathit{配置}\]

配置是程序状态的句法描述。每个规则指定执行的一步。只要最多只有一个归约规则适用于给定的配置，归约（以及由此产生的执行）就是确定性的。WebAssembly 只有很少的例外，在本规范中明确指出了这些例外。

对于 WebAssembly，配置通常是一个元组 \((S; F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast)\)，它由当前存储 \(S\)、当前函数的调用帧 \(F\) 以及要执行的指令序列组成。（更精确的定义在后面给出。）

为了避免不必要的混乱，存储 \(S\) 和帧 \(F\) 从不触及它们的归约规则中省略。

没有堆栈的单独表示。相反，它可以方便地表示为配置的指令序列的一部分。特别是，值 被定义为与 \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) 指令一致，并且\(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) 指令的序列可以解释为向右增长的操作数“堆栈”。

注意

例如，\(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\) 指令的归约规则 可以给出如下

\[(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n_2)~\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad (\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~(n_1 + n_2) \mathbin{\mathrm{mod}} 2^{32})\]

根据此规则，两个 \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) 指令和\(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}\) 指令本身从指令流中删除，并替换为一个新的\(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) 指令。这可以解释为从堆栈中弹出两个值并推入结果。

当没有产生结果时，指令归约为空序列

\[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad \epsilon\]

标签 和 帧 类似地定义 为指令序列的一部分。

归约的顺序由适当评估上下文的定义决定。

当不再适用任何归约规则时，归约终止。 WebAssembly 的健全性类型系统保证只有当原始指令序列被归约为 \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) 指令的序列时，才会发生这种情况，该序列可以解释为结果操作数堆栈的值，或者如果发生了陷阱。

注意

例如，以下指令序列，

\[(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_2)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{neg}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_3)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{mul}}\]

在三个步骤后终止

\[\begin{split}\begin{array}{ll} & (\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_2)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{neg}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_3)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{mul}} \\ \href{../exec/conventions.html#exec-notation}{\hookrightarrow} & (\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_4)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_3)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{mul}} \\ \href{../exec/conventions.html#exec-notation}{\hookrightarrow} & (\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_5)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{mul}} \\ \href{../exec/conventions.html#exec-notation}{\hookrightarrow} & (\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_6) \\ \end{array}\end{split}\]

其中 \(x_4 = -x_2\) 并且 \(x_5 = -x_2 + x_3\) 并且 \(x_6 = x_1 \cdot (-x_2 + x_3)\)。