运行时结构¶

存储、栈和 WebAssembly 抽象机中形成其他运行时结构，例如值或模块实例，都是通过额外的辅助语法来精确定义的。

值¶

WebAssembly 计算操作四种基本数值类型的值，即分别为 32 位或 64 位宽度的整数和浮点数数据，或 128 位宽度的向量，或引用类型。

在语义的大多数地方，不同类型的值都会出现。为了避免歧义，因此使用一种抽象语法来表示值，使其类型明确。方便的是，可以重复使用与 \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) 指令和 \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}\) 相同的符号来生成它们。

除了空引用之外的其他引用都使用额外的管理指令来表示。它们要么是函数引用，指向特定的函数地址，要么是外部引用，指向外部地址的未解释形式，由嵌入器定义以表示其自身的对象。

\[\begin{split}\begin{array}{llcl} \def\mathdef2246#1{{}}\mathdef2246{number} & \href{../exec/runtime.html#syntax-num}{\mathit{num}} &::=& \href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-int}{\mathit{i32}} \\&&|& \href{../syntax/types.html#syntax-valtype}{\mathsf{i64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-int}{\mathit{i64}} \\&&|& \href{../syntax/types.html#syntax-valtype}{\mathsf{f32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-float}{\mathit{f32}} \\&&|& \href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-float}{\mathit{f64}} \\ \def\mathdef2246#1{{}}\mathdef2246{vector} & \href{../exec/runtime.html#syntax-vecc}{\mathit{vec}} &::=& \href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-int}{\mathit{i128}} \\ \def\mathdef2246#1{{}}\mathdef2246{reference} & \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} &::=& \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t \\&&|& \href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\&&|& \href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}} \\ \def\mathdef2246#1{{}}\mathdef2246{value} & \href{../exec/runtime.html#syntax-val}{\mathit{val}} &::=& \href{../exec/runtime.html#syntax-num}{\mathit{num}} ~|~ \href{../exec/runtime.html#syntax-vecc}{\mathit{vec}} ~|~ \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} \\ \end{array}\end{split}\]

注意

WebAssembly 的未来版本可能会添加其他形式的引用。

每个值类型都有一个关联的默认值；它对于数值类型是相应的值 \(0\)，对于向量类型是 \(0\)，对于引用类型是空值。

\[\begin{split}\begin{array}{lcl@{\qquad}l} \href{../exec/runtime.html#default-val}{\mathrm{default}}_t &=& t{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0 & (\mathrel{\mbox{if}} t = \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}) \\ \href{../exec/runtime.html#default-val}{\mathrm{default}}_t &=& t{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0 & (\mathrel{\mbox{if}} t = \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}) \\ \href{../exec/runtime.html#default-val}{\mathrm{default}}_t &=& \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t & (\mathrel{\mbox{if}} t = \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}) \\ \end{array}\end{split}\]

约定¶

元变量 \(r\) 表示引用值，其中从上下文中可以清楚地了解。

结果¶

结果是计算的结果。它要么是一系列值，要么是陷阱。

\[\begin{split}\begin{array}{llcl} \def\mathdef2246#1{{}}\mathdef2246{result} & \href{../exec/runtime.html#syntax-result}{\mathit{result}} &::=& \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast \\&&|& \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \end{array}\end{split}\]

存储¶

存储表示 WebAssembly 程序可以操作的所有全局状态。它包含所有函数、表格、内存和全局变量、元素段和数据段的运行时表示形式，这些段在抽象机的生命周期中已被分配。[1]

语义的另一个不变式是，没有任何元素或数据实例从除拥有模块实例之外的其他任何地方被寻址。

在语法上，存储被定义为一个记录，其中列出了每个类别中现有的实例。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{store} & \href{../exec/runtime.html#syntax-store}{\mathit{store}} &::=& \{~ \begin{array}[t]{l@{~}ll} \href{../exec/runtime.html#syntax-store}{\mathsf{funcs}} & \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}^\ast, \\ \href{../exec/runtime.html#syntax-store}{\mathsf{tables}} & \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}^\ast, \\ \href{../exec/runtime.html#syntax-store}{\mathsf{mems}} & \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}^\ast, \\ \href{../exec/runtime.html#syntax-store}{\mathsf{globals}} & \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}^\ast, \\ \href{../exec/runtime.html#syntax-store}{\mathsf{elems}} & \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}^\ast, \\ \href{../exec/runtime.html#syntax-store}{\mathsf{datas}} & \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}^\ast ~\} \\ \end{array} \end{array}\end{split}\]

约定¶

元变量 \(S\) 表示存储，其中从上下文中可以清楚地了解。

地址¶

函数实例、表格实例、内存实例和全局变量实例、元素实例和数据实例在存储中使用抽象的地址进行引用。这些地址只是对相应存储组件的索引。此外，嵌入器可以提供一组未解释的主机地址。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{address} & \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} &::=& 0 ~|~ 1 ~|~ 2 ~|~ \dots \\ \def\mathdef2246#1{{}}\mathdef2246{function address} & \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} &::=& \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ \def\mathdef2246#1{{}}\mathdef2246{table address} & \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} &::=& \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ \def\mathdef2246#1{{}}\mathdef2246{memory address} & \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} &::=& \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ \def\mathdef2246#1{{}}\mathdef2246{global address} & \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} &::=& \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ \def\mathdef2246#1{{}}\mathdef2246{element address} & \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}} &::=& \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ \def\mathdef2246#1{{}}\mathdef2246{data address} & \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}} &::=& \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ \def\mathdef2246#1{{}}\mathdef2246{extern address} & \href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}} &::=& \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\ \end{array}\end{split}\]

嵌入器可以为与它们的地址相对应的导出存储对象分配标识，即使该标识从 WebAssembly 代码本身内部无法观察到（例如对于函数实例或不可变的全局变量）。

注意

地址是动态的，是针对运行时对象的全局唯一引用，与索引相反，后者是静态的，是针对其原始定义的模块级局部引用。内存地址 \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}\) 表示存储中内存实例的抽象地址，而不是内存实例内部的偏移量。

存储对象分配数量没有具体限制，因此逻辑地址可以是任意大的自然数。

模块实例¶

模块实例 是模块的运行时表示形式。它是通过实例化模块来创建的，它收集了模块导入、定义或导出的所有实体的运行时表示形式。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{module instance} & \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} &::=& \{ \begin{array}[t]{l@{~}ll} \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}} & \href{../syntax/types.html#syntax-functype}{\mathit{functype}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}} & \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}} & \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}} & \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}} & \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}} & \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}} & \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}} & \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast ~\} \\ \end{array} \end{array}\end{split}\]

每个组件引用对应于原始模块（无论是导入的还是定义的）中的相应声明的运行时实例，按照它们静态索引的顺序。函数实例、表实例、内存实例和全局实例通过它们在存储中的相应地址进行间接引用。

语义的不变性是，给定模块实例中的所有导出实例具有不同的名称。

函数实例¶

函数实例 是函数的运行时表示。它实际上是原始函数在它起源的模块的运行时模块实例上的闭包。模块实例用于在执行函数期间解析对其他定义的引用。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{函数实例} & \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} &::=& \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}} \} \\ &&|& \{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} \} \\ \def\mathdef2246#1{{}}\mathdef2246{主机函数} & \href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} &::=& \dots \\ \end{array}\end{split}\]

主机函数 是在 WebAssembly 之外表达的函数，但作为模块的导入传递给它。主机函数的定义和行为超出了本规范的范围。为了本规范的目的，假定当调用时，主机函数的行为是非确定性的，但在某些约束内，以确保运行时的完整性。

注意

函数实例是不可变的，它们的身份无法被 WebAssembly 代码观察到。但是，嵌入器可能会提供隐式或显式的方法来区分它们的地址。

表实例¶

表实例 是表的运行时表示。它记录了它的类型并保存一个引用值的向量。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{表实例} & \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} &::=& \{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~\href{../syntax/conventions.html#syntax-vec}{\mathit{vec}}(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) \} \\ \end{array}\end{split}\]

表元素可以通过表指令、活动元素段的执行或由嵌入器提供的外部手段进行修改。

语义的不变性是所有表元素的类型都等于 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) 的元素类型。另一个不变性是，如果存在，元素向量的长度永远不会超过 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) 的最大大小。

内存实例¶

内存实例 是线性内存的运行时表示。它记录了它的类型并保存一个字节的向量。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{内存实例} & \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} &::=& \{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~\href{../syntax/conventions.html#syntax-vec}{\mathit{vec}}(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}) \} \\ \end{array}\end{split}\]

向量的长度始终是 WebAssembly 页面大小 的倍数，页面大小被定义为常量 \(65536\) —— 简写为 \(64\,\mathrm{Ki}\)。

字节可以通过内存指令、活动数据段的执行或由嵌入器提供的外部手段进行修改。

语义的不变性是，字节向量长度除以页面大小永远不会超过 \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) 的最大大小（如果存在）。

全局实例¶

全局实例 是全局变量的运行时表示。它记录了它的类型并保存一个单独的值。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{全局实例} & \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}} &::=& \{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}, \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}} \} \\ \end{array}\end{split}\]

可变全局的值可以通过变量指令或由嵌入器提供的外部手段进行修改。

语义的不变性是，该值具有与 \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) 的值类型相同的类型。

元素实例¶

元素实例 是元素段的运行时表示。它保存一个引用向量及其共同的类型。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{元素实例} & \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}} &::=& \{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\href{../syntax/conventions.html#syntax-vec}{\mathit{vec}}(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) \} \\ \end{array}\end{split}\]

数据实例¶

数据实例 是数据段的运行时表示。它保存一个字节的向量。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{数据实例} & \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}} &::=& \{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~\href{../syntax/conventions.html#syntax-vec}{\mathit{vec}}(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}) \} \\ \end{array}\end{split}\]

导出实例¶

导出实例 是导出的运行时表示。它定义了导出的名称和关联的外部值。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{导出实例} & \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}} &::=& \{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}} \} \\ \end{array}\end{split}\]

外部值¶

外部值 是可以导入或导出的实体的运行时表示。它是一个地址，表示共享存储中的函数实例、表实例、内存实例或全局实例。

\[\begin{split}\begin{array}{llcl} \def\mathdef2246#1{{}}\mathdef2246{外部值} & \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} &::=& \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\&&|& \href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} \\&&|& \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} \\&&|& \href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} \\ \end{array}\end{split}\]

约定¶

为外部值的序列定义了以下辅助符号。它以保持顺序的方式过滤掉特定种类的条目

\(\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)
\(\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)
\(\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)
\(\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)

栈¶

除了存储之外，大多数指令都与一个隐式的堆栈交互。堆栈包含三种类型的条目

值：指令的操作数。
标签：活跃的结构化控制指令，可以被分支目标指向。
激活：活跃的函数调用的调用帧。

这些条目可以在程序执行期间以任何顺序出现在堆栈上。堆栈条目由以下抽象语法描述。

注意

可以使用单独的堆栈来模拟 WebAssembly 语义，分别用于操作数、控制结构和调用。然而，由于堆栈是相互依赖的，因此需要关于关联堆栈高度的额外记录。为了本规范的目的，交错表示更简单。

值¶

值由自身表示。

标签¶

标签带有参数元数 \(n\) 及其关联的分支目标，在语法上表示为指令序列

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{label} & \href{../exec/runtime.html#syntax-label}{\mathit{label}} &::=& \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\} \\ \end{array}\end{split}\]

直观地，\(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) 是在分支被执行时要执行的延续，代替了原始的控制结构。

注意

例如，循环标签的形式为

\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~\dots~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\}\]

在执行到该标签的分支时，将执行循环，有效地从头开始重新启动。相反，简单的块标签的形式为

\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\epsilon\}\]

在分支时，空延续将结束目标块，以便执行可以继续进行后续指令。

激活帧¶

激活帧带有相应函数的返回元数 \(n\)，保存其局部变量（包括参数）的值，顺序对应于它们的静态局部变量索引，以及对函数自身模块实例的引用

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{frame} & \href{../exec/runtime.html#syntax-frame}{\mathit{frame}} &::=& \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{ \href{../exec/runtime.html#syntax-framestate}{\mathit{framestate}} \} \\ \def\mathdef2246#1{{}}\mathdef2246{frame state} & \href{../exec/runtime.html#syntax-framestate}{\mathit{framestate}} &::=& \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} \} \\ \end{array}\end{split}\]

局部变量的值通过各自的变量指令进行修改。

约定¶

元变量 \(L\) 在上下文中明确的情况下范围为标签。
元变量 \(F\) 在上下文中明确的情况下范围为帧状态。
以下辅助定义接受一个块类型，并在当前帧中查找它所表示的函数类型

\[\begin{split}\begin{array}{lll} \href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}) &=& F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}] \\ \href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F([\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?]) &=& [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?] \\ \end{array}\end{split}\]

管理指令¶

注意

本节仅与正式符号相关。

为了表达陷阱、调用和控制指令的归约，指令的语法扩展为包含以下管理指令

\[\begin{split}\begin{array}{llcl} \def\mathdef2246#1{{}}\mathdef2246{administrative instruction} & \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} &::=& \dots \\ &&|& \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ &&|& \href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\ &&|& \href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}} \\ &&|& \href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\ &&|& \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ &&|& \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{\href{../exec/runtime.html#syntax-framestate}{\mathit{framestate}}\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ \end{array}\end{split}\]

\(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\) 指令表示陷阱的发生。陷阱通过嵌套的指令序列冒泡，最终将整个程序归约为单个 \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\) 指令，表示意外终止。

\(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}\) 指令表示函数引用值。类似地，\(\href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}\) 表示外部引用。

\(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}\) 指令表示即将调用函数实例，由其地址标识。它统一了不同形式调用的处理方式。

\(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\) 和 \(\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}\) 指令对标签和帧 “在堆栈上”进行建模。此外，管理语法保持原始结构化控制指令或函数体及其指令序列的嵌套结构，使用一个 \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\) 标记。这样，在作为外部序列的一部分时，可以知道内部指令序列的结束位置。

注意

例如，归约规则用于 \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}\) 是

\[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~[t^n]~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad \href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\epsilon\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\]

这将块替换为标签指令，可以解释为“将标签压入堆栈”。当到达 \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\) 时，即内部指令序列已归约为空序列——或者更确切地说，是表示结果值的 \(n\) 个 \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) 指令序列——那么 \(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\) 指令将通过其自身的归约规则被消除

\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_m\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\]

这可以解释为从堆栈中删除标签，只留下本地累积的操作数值。

块上下文¶

为了指定分支的归约，定义了以下块上下文语法，由包围空洞 \([\_]\) 的标签数量 \(k\) 索引，空洞标记了下一步计算发生的位置

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{block contexts} & \href{../exec/runtime.html#syntax-ctxt-block}{B}^0 &::=& \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast~[\_]~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \\ \def\mathdef2246#1{{}}\mathdef2246{block contexts} & \href{../exec/runtime.html#syntax-ctxt-block}{B}^{k+1} &::=& \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast~\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^k~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \\ \end{array}\end{split}\]

此定义允许索引包围分支或返回指令的活动标签。

注意

例如，简单分支的归约可以定义如下

\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_0\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^l[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l]~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \quad\href{../exec/conventions.html#exec-notation}{\hookrightarrow}\quad \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\]

在此，上下文的空洞 \([\_]\) 被实例化为分支指令。当发生分支时，此规则将目标标签及其关联的指令序列替换为标签的延续。所选标签通过标签索引 \(l\) 标识，它对应于必须跳过的包围 \(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\) 指令的数量——这正是块上下文索引中编码的计数。

配置¶

配置由当前存储和正在执行的线程组成。

线程是在指令上进行的计算，相对于当前帧的状态进行操作，该帧引用了计算运行的模块实例，即当前函数源自的位置。

\[\begin{split}\begin{array}{llcl} \def\mathdef2246#1{{}}\mathdef2246{配置} & \href{../exec/runtime.html#syntax-config}{\mathit{配置}} &::=& \href{../exec/runtime.html#syntax-store}{\mathit{存储}}; \href{../exec/runtime.html#syntax-thread}{\mathit{线程}} \\ \def\mathdef2246#1{{}}\mathdef2246{线程} & \href{../exec/runtime.html#syntax-thread}{\mathit{线程}} &::=& \href{../exec/runtime.html#syntax-framestate}{\mathit{帧状态}}; \href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}^\ast \\ \end{array}\end{split}\]

注意

当前版本的 WebAssembly 是单线程的，但将来可能会支持多线程配置。

评估上下文¶

最后，以下关于评估上下文的定义和相关结构规则，允许在指令序列和管理表单内部进行规约，以及传播陷阱。

\[\begin{split}\begin{array}{llll} \def\mathdef2246#1{{}}\mathdef2246{评估上下文} & E &::=& [\_] ~|~ \href{../exec/runtime.html#syntax-val}{\mathit{值}}^\ast~E~\href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}^\ast ~|~ \href{../exec/runtime.html#syntax-label}{\mathsf{标签}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}^\ast\}~E~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{结束}} \\ \end{array}\end{split}\]

\[\begin{split}\begin{array}{rcl} S; F; E[\href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}^\ast] &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F'; E[{\href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}'}^\ast] \\ && (\mathrel{\mbox{如果}} S; F; \href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}^\ast \href{../exec/conventions.html#exec-notation}{\hookrightarrow} S'; F'; {\href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}'}^\ast) \\ S; F; \href{../exec/runtime.html#syntax-frame}{\mathsf{帧}}_n\{F'\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{结束}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; \href{../exec/runtime.html#syntax-frame}{\mathsf{帧}}_n\{F''\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}'^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{结束}} \\ && (\mathrel{\mbox{如果}} S; F'; \href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}^\ast \href{../exec/conventions.html#exec-notation}{\hookrightarrow} S'; F''; {\href{../syntax/instructions.html#syntax-instr}{\mathit{指令}}'}^\ast) \\[1ex] S; F; E[\href{../exec/runtime.html#syntax-trap}{\mathsf{陷阱}}] &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{陷阱}} \qquad (\mathrel{\mbox{如果}} E \neq [\_]) \\ S; F; \href{../exec/runtime.html#syntax-frame}{\mathsf{帧}}_n\{F'\}~\href{../exec/runtime.html#syntax-trap}{\mathsf{陷阱}}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{结束}} &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{陷阱}} \\ \end{array}\end{split}\]

当线程的指令序列规约为一个结果时，规约结束，即一个值序列或一个\(\href{../exec/runtime.html#syntax-trap}{\mathsf{陷阱}}\)。

注意

对评估上下文的限制排除了诸如\([\_]\)和\(\epsilon~[\_]~\epsilon\)这样的上下文，对于这些上下文，\(E[\href{../exec/runtime.html#syntax-trap}{\mathsf{陷阱}}] = \href{../exec/runtime.html#syntax-trap}{\mathsf{陷阱}}\)。

关于评估上下文下规约的一个例子，考虑以下指令序列。

\[(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{常量}}~x_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{常量}}~x_2)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{负}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{常量}}~x_3)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{加}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{乘}}\]

这可以分解为\(E[(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{常量}}~x_2)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{负}}]\)，其中

\[E = (\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{常量}}~x_1)~[\_]~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{常量}}~x_3)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{加}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{乘}}\]

此外，这是唯一可能的评估上下文选择，其中孔的内容与规约规则的左侧匹配。