嵌入¶

WebAssembly 实现通常会被嵌入到一个宿主环境中。嵌入器实现了这样的宿主环境与本规范主体中定义的 WebAssembly 语义之间的连接。预期嵌入器会以明确定义的方式与语义进行交互。

本节以入口点的形式定义了 WebAssembly 语义的合适接口，嵌入器可以通过这些入口点访问它。该接口旨在完整，即嵌入器无需直接引用 WebAssembly 规范的其他功能部分。

注意

另一方面，嵌入器不需要向宿主环境提供对本接口中定义的所有功能的访问权限。例如，实现可能不支持解析文本格式。

类型¶

在嵌入器接口的描述中，来自抽象语法和运行时的抽象机的语法类被用作变量的名称，这些变量范围涵盖该类中可能的对象。因此，这些语法类也可以解释为类型。

对于数值参数，使用类似\(n:\href{../syntax/values.html#syntax-int}{\mathit{u32}}\)的表示法来指定符号名称以及相应的取值范围。

错误¶

接口操作失败由辅助语法类指示

\[\begin{split}\begin{array}{llll} \def\mathdef120#1{{}}\mathdef120{error} & \href{../appendix/embedding.html#embed-error}{\mathit{error}} &::=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} \\ \end{array}\end{split}\]

除了本节中明确指定的错误条件外，当达到特定的实现限制时，实现也可能会返回错误。

注意

根据此定义，错误是抽象的且不具体的。实现可以对其进行细化以承载合适的分类和诊断消息。

先决条件和后置条件¶

某些操作会声明其参数的先决条件或其结果的后置条件。满足先决条件是嵌入器的责任。如果满足，则语义保证后置条件。

除了每个操作明确声明的先决条件和后置条件外，规范还采用了以下约定用于运行时对象（\(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\)、\(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)、\(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}\)、地址）

作为参数传递的每个运行时对象都必须根据隐式先决条件为有效。
作为结果返回的每个运行时对象都必须根据隐式后置条件为有效。

注意

只要嵌入器将运行时对象视为抽象，并且仅通过此处定义的接口创建和操作它们，所有隐式先决条件就会自动满足。

存储¶

\(\mathrm{store\_init}() : \href{../exec/runtime.html#syntax-store}{\mathit{store}}\)¶

返回空存储。

\[\begin{split}\begin{array}{lclll} \mathrm{store\_init}() &=& \{ \href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\epsilon,~ \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~\epsilon,~ \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~\epsilon,~ \href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~\epsilon \} \\ \end{array}\end{split}\]

模块¶

\(\mathrm{module\_decode}(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}^\ast) : \href{../syntax/modules.html#syntax-module}{\mathit{module}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

如果存在字节序列\(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}^\ast\)作为\(\href{../binary/modules.html#binary-module}{\mathtt{module}}\)的推导，根据模块的二进制语法，产生一个模块\(m\)，则返回\(m\)。
否则，返回\(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。

\[\begin{split}\begin{array}{lclll} \mathrm{module\_decode}(b^\ast) &=& m && (\mathrel{\mbox{if}} \href{../binary/modules.html#binary-module}{\mathtt{module}} \stackrel\ast\Longrightarrow m{:}b^\ast) \\ \mathrm{module\_decode}(b^\ast) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{module\_parse}(\href{../syntax/values.html#syntax-name}{\mathit{char}}^\ast) : \href{../syntax/modules.html#syntax-module}{\mathit{module}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

如果存在源代码\(\href{../syntax/values.html#syntax-name}{\mathit{char}}^\ast\)作为\(\href{../text/modules.html#text-module}{\mathtt{module}}\)的推导，根据模块的文本语法，产生一个模块\(m\)，则返回\(m\)。
否则，返回\(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。

\[\begin{split}\begin{array}{lclll} \mathrm{module\_parse}(c^\ast) &=& m && (\mathrel{\mbox{if}} \href{../text/modules.html#text-module}{\mathtt{module}} \stackrel\ast\Longrightarrow m{:}c^\ast) \\ \mathrm{module\_parse}(c^\ast) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{module\_validate}(\href{../syntax/modules.html#syntax-module}{\mathit{module}}) : \href{../appendix/embedding.html#embed-error}{\mathit{error}}^?\)¶

如果\(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\)是有效的，则不返回任何内容。
否则，返回\(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。

\[\begin{split}\begin{array}{lclll} \mathrm{module\_validate}(m) &=& \epsilon && (\mathrel{\mbox{if}} {} \href{../valid/modules.html#valid-module}{\vdash} m : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast \href{../syntax/types.html#syntax-functype}{\rightarrow} {\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast) \\ \mathrm{module\_validate}(m) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{module\_instantiate}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}})\)¶

尝试实例化\(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\)在\(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\)中，使用外部值\(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast\)作为导入。

如果它使用模块实例\(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)成功，则令\(\mathit{result}\)为\(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)。

否则，令\(\mathit{result}\)为\(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。

返回与\(\mathit{result}\)配对的新存储。

\[\begin{split}\begin{array}{lclll} \mathrm{module\_instantiate}(S, m, \mathit{ev}^\ast) &=& (S', F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}(S, m, \mathit{ev}^\ast) \href{../exec/conventions.html#exec-notation}{\hookrightarrow}^\ast S'; F; \epsilon) \\ \mathrm{module\_instantiate}(S, m, \mathit{ev}^\ast) &=& (S', \href{../appendix/embedding.html#embed-error}{\mathsf{error}}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}(S, m, \mathit{ev}^\ast) \href{../exec/conventions.html#exec-notation}{\hookrightarrow}^\ast S'; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}) \\ \end{array}\end{split}\]

注意

即使发生错误，存储也可能会被修改。

\(\mathrm{module\_imports}(\href{../syntax/modules.html#syntax-module}{\mathit{module}}) : (\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^\ast\)¶

先决条件：\(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\)是有效的，具有外部导入类型\(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast\)和外部导出类型\({\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast\)。
令\(\href{../syntax/modules.html#syntax-import}{\mathit{import}}^\ast\)为导入\(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{imports}}\)。
断言：\(\href{../syntax/modules.html#syntax-import}{\mathit{import}}^\ast\)的长度等于\(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast\)的长度。
对于\(\href{../syntax/modules.html#syntax-import}{\mathit{import}}^\ast\)中的每个\(\href{../syntax/modules.html#syntax-import}{\mathit{import}}_i\)和\(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast\)中对应的\(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\)，执行以下操作

令\(\mathit{result}_i\)为三元组\((\href{../syntax/modules.html#syntax-import}{\mathit{import}}_i.\href{../syntax/modules.html#syntax-import}{\mathsf{module}}, \href{../syntax/modules.html#syntax-import}{\mathit{import}}_i.\href{../syntax/modules.html#syntax-import}{\mathsf{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i)\)。

返回所有\(\mathit{result}_i\)的连接，按索引顺序。
后置条件：每个\(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\)都是有效的。

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{module\_imports}(m) &=& (\mathit{im}.\href{../syntax/modules.html#syntax-import}{\mathsf{module}}, \mathit{im}.\href{../syntax/modules.html#syntax-import}{\mathsf{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^\ast \\ && \qquad (\mathrel{\mbox{if}} \mathit{im}^\ast = m.\href{../syntax/modules.html#syntax-module}{\mathsf{imports}} \wedge {} \href{../valid/modules.html#valid-module}{\vdash} m : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast \href{../syntax/types.html#syntax-functype}{\rightarrow} {\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast) \\ \end{array}\end{split}\]

\(\mathrm{module\_exports}(\href{../syntax/modules.html#syntax-module}{\mathit{module}}) : (\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^\ast\)¶

先决条件：\(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\)是有效的，具有外部导入类型\(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast\)和外部导出类型\({\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast\)。
令 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast\) 为导出 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}\)。
断言：\(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast\) 的长度等于 \({\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast\) 的长度。
对于 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast\) 中的每个 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) 以及 \({\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast\) 中对应的 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\)，执行以下操作

令 \(\mathit{result}_i\) 为对 \((\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i)\)。

返回所有\(\mathit{result}_i\)的连接，按索引顺序。
后置条件：每个 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\) 都是有效的。

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{module\_exports}(m) &=& (\mathit{ex}.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}, \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}')^\ast \\ && \qquad (\mathrel{\mbox{如果}} \mathit{ex}^\ast = m.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}} \wedge {} \href{../valid/modules.html#valid-module}{\vdash} m : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}^\ast \href{../syntax/types.html#syntax-functype}{\rightarrow} {\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'}^\ast) \\ \end{array}\end{split}\]

模块实例¶

\(\mathrm{instance\_export}(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../syntax/values.html#syntax-name}{\mathit{name}}) : \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

断言：由于有效性的模块实例 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)，其所有导出名称都不相同。
如果存在 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}\) 中的 \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\)，使得名称 \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i.\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}\) 等于 \(\href{../syntax/values.html#syntax-name}{\mathit{name}}\)，则
1. 返回外部值 \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i.\href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}\)。
否则，返回\(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{instance\_export}(m, \href{../syntax/values.html#syntax-name}{\mathit{name}}) &=& m.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}[i].\href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}} && (\mathrel{\mbox{如果}} m.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}[i].\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}} = \href{../syntax/values.html#syntax-name}{\mathit{name}}) \\ \mathrm{instance\_export}(m, \href{../syntax/values.html#syntax-name}{\mathit{name}}) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]

函数¶

\(\mathrm{func\_alloc}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}})\)¶

前置条件：\(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) 是有效的。
令 \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) 为在 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) 中分配主机函数的结果，具有函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) 和主机函数代码 \(\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}\)。
返回新的存储与 \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) 配对。

\[\begin{split}\begin{array}{lclll} \mathrm{func\_alloc}(S, \mathit{ft}, \mathit{code}) &=& (S', \mathit{a}) && (\mathrel{\mbox{如果}} \href{../exec/modules.html#alloc-hostfunc}{\mathrm{allochostfunc}}(S, \mathit{ft}, \mathit{code}) = S', \mathit{a}) \\ \end{array}\end{split}\]

注意

此操作假设 \(\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}\) 满足类型为 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) 的函数实例所需的前置和后置条件。

常规（非主机）函数实例只能通过模块实例化间接创建。

\(\mathrm{func\_type}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) : \href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)¶

返回 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\)。
后置条件：返回的函数类型是有效的。

\[\begin{split}\begin{array}{lclll} \mathrm{func\_type}(S, a) &=& S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}} \\ \end{array}\end{split}\]

\(\mathrm{func\_invoke}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}})\)¶

尝试调用 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) 中的函数 \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\)，使用值 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 作为参数

如果它成功并使用值 \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^\ast\) 作为结果，则令 \(\mathit{result}\) 为 \({\href{../exec/runtime.html#syntax-val}{\mathit{val}}'}^\ast\)。

否则它已陷入陷阱，因此令 \(\mathit{result}\) 为 \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。

返回与\(\mathit{result}\)配对的新存储。

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{func\_invoke}(S, a, v^\ast) &=& (S', {v'}^\ast) && (\mathrel{\mbox{如果}} \href{../exec/modules.html#exec-invocation}{\mathrm{invoke}}(S, a, v^\ast) \href{../exec/conventions.html#exec-notation}{\hookrightarrow}^\ast S'; F; {v'}^\ast) \\ \mathrm{func\_invoke}(S, a, v^\ast) &=& (S', \href{../appendix/embedding.html#embed-error}{\mathsf{error}}) && (\mathrel{\mbox{如果}} \href{../exec/modules.html#exec-invocation}{\mathrm{invoke}}(S, a, v^\ast) \href{../exec/conventions.html#exec-notation}{\hookrightarrow}^\ast S'; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}) \\ \end{array}\end{split}\]

注意

即使发生错误，存储也可能会被修改。

表¶

\(\mathrm{table\_alloc}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}})\)¶

前置条件：\(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) 是有效的。
令 \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}\) 为在 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) 中分配表的结果，具有表类型 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) 和初始化值 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\)。
返回新的存储与 \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}\) 配对。

\[\begin{split}\begin{array}{lclll} \mathrm{table\_alloc}(S, \mathit{tt}, r) &=& (S', \mathit{a}) && (\mathrel{\mbox{如果}} \href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}(S, \mathit{tt}, r) = S', \mathit{a}) \\ \end{array}\end{split}\]

\(\mathrm{table\_type}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}) : \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\)¶

返回 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}\)。
后置条件：返回的表类型是有效的。

\[\begin{split}\begin{array}{lclll} \mathrm{table\_type}(S, a) &=& S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}} \\ \end{array}\end{split}\]

\(\mathrm{table\_read}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}, i:\href{../syntax/values.html#syntax-int}{\mathit{u32}}) : \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

令 \(\mathit{ti}\) 为表实例 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\)。
如果 \(i\) 大于或等于 \(\mathit{ti}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\) 的长度，则返回 \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。
否则，返回引用值 \(\mathit{ti}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i]\)。

\[\begin{split}\begin{array}{lclll} \mathrm{table\_read}(S, a, i) &=& r && (\mathrel{\mbox{如果}} S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i] = r) \\ \mathrm{table\_read}(S, a, i) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{否则}}) \\ \end{array}\end{split}\]

\(\mathrm{table\_write}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}, i:\href{../syntax/values.html#syntax-int}{\mathit{u32}}, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

令 \(\mathit{ti}\) 为表实例 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\)。
如果 \(i\) 大于或等于 \(\mathit{ti}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\) 的长度，则返回 \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。
将 \(\mathit{ti}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i]\) 替换为引用值 reference value \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\)。
返回更新后的存储。

\[\begin{split}\begin{array}{lclll} \mathrm{table\_write}(S, a, i, r) &=& S' && (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i] = r) \\ \mathrm{table\_write}(S, a, i, r) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{table\_size}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}) : \href{../syntax/values.html#syntax-int}{\mathit{u32}}\)¶

返回 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\) 的长度。

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{table\_size}(S, a) &=& n && (\mathrel{\mbox{if}} |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}| = n) \\ \end{array}\end{split}\]

\(\mathrm{table\_grow}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}, n:\href{../syntax/values.html#syntax-int}{\mathit{u32}}, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

尝试扩展表实例 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}]\) \(n\) 个元素，初始化值为 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\)
1. 如果成功，则返回更新后的存储。
2. 否则，返回\(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{table\_grow}(S, a, n, r) &=& S' && (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a] = \href{../exec/modules.html#grow-table}{\mathrm{growtable}}(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a], n, r)) \\ \mathrm{table\_grow}(S, a, n, r) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

内存¶

\(\mathrm{mem\_alloc}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}})\)¶

前提条件：\(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) 是有效的。
令 \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}\) 为在 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) 中分配内存的结果，内存类型为 \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\)。
返回新的存储和 \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}\) 的组合。

\[\begin{split}\begin{array}{lclll} \mathrm{mem\_alloc}(S, \mathit{mt}) &=& (S', \mathit{a}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}(S, \mathit{mt}) = S', \mathit{a}) \\ \end{array}\end{split}\]

\(\mathrm{mem\_type}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}) : \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\)¶

返回 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\)。
后置条件：返回的内存类型是有效的。

\[\begin{split}\begin{array}{lclll} \mathrm{mem\_type}(S, a) &=& S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}} \\ \end{array}\end{split}\]

\(\mathrm{mem\_read}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}, i:\href{../syntax/values.html#syntax-int}{\mathit{u32}}) : \href{../syntax/values.html#syntax-byte}{\mathit{byte}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

令 \(\mathit{mi}\) 为内存实例 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\)。
如果 \(i\) 大于或等于 \(\mathit{mi}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则返回 \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。
否则，返回字节 \(\mathit{mi}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[i]\)。

\[\begin{split}\begin{array}{lclll} \mathrm{mem\_read}(S, a, i) &=& b && (\mathrel{\mbox{if}} S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[i] = b) \\ \mathrm{mem\_read}(S, a, i) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{mem\_write}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}, i:\href{../syntax/values.html#syntax-int}{\mathit{u32}}, \href{../syntax/values.html#syntax-byte}{\mathit{byte}}) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

令 \(\mathit{mi}\) 为内存实例 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\)。
如果 \(\href{../syntax/values.html#syntax-int}{\mathit{u32}}\) 大于或等于 \(\mathit{mi}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度，则返回 \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。
将 \(\mathit{mi}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[i]\) 替换为 \(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}\)。
返回更新后的存储。

\[\begin{split}\begin{array}{lclll} \mathrm{mem\_write}(S, a, i, b) &=& S' && (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[i] = b) \\ \mathrm{mem\_write}(S, a, i, b) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

\(\mathrm{mem\_size}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}) : \href{../syntax/values.html#syntax-int}{\mathit{u32}}\)¶

返回 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度除以页面大小。

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{mem\_size}(S, a) &=& n && (\mathrel{\mbox{if}} |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| = n \cdot 64\,\mathrm{Ki}) \\ \end{array}\end{split}\]

\(\mathrm{mem\_grow}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}, n:\href{../syntax/values.html#syntax-int}{\mathit{u32}}) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

尝试扩展内存实例 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}]\) \(n\) 个页面
1. 如果成功，则返回更新后的存储。
2. 否则，返回\(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{mem\_grow}(S, a, n) &=& S' && (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a] = \href{../exec/modules.html#grow-mem}{\mathrm{growmem}}(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a], n)) \\ \mathrm{mem\_grow}(S, a, n) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]

全局变量¶

\(\mathrm{global\_alloc}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}) : (\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}})\)¶

前提条件：\(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) 是有效的。
令 \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}\) 为在 \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}\) 中分配全局变量的结果，全局变量类型为 \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\)，初始化值为 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)。
返回新的存储和 \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}\) 的组合。

\[\begin{split}\begin{array}{lclll} \mathrm{global\_alloc}(S, \mathit{gt}, v) &=& (S', \mathit{a}) && (\mathrel{\mbox{if}} \href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}(S, \mathit{gt}, v) = S', \mathit{a}) \\ \end{array}\end{split}\]

\(\mathrm{global\_type}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}) : \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\)¶

返回 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}\)。
后置条件：返回的全局变量类型是有效的。

\[\begin{split}\begin{array}{lclll} \mathrm{global\_type}(S, a) &=& S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}} \\ \end{array}\end{split}\]

\(\mathrm{global\_read}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}) : \href{../exec/runtime.html#syntax-val}{\mathit{val}}\)¶

令 \(\mathit{gi}\) 为全局实例 global instance \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}]\)。
返回 value \(\mathit{gi}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}\)。

\[\begin{split}\begin{array}{lclll} \mathrm{global\_read}(S, a) &=& v && (\mathrel{\mbox{if}} S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}} = v) \\ \end{array}\end{split}\]

\(\mathrm{global\_write}(\href{../exec/runtime.html#syntax-store}{\mathit{store}}, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}) : \href{../exec/runtime.html#syntax-store}{\mathit{store}} ~|~ \href{../appendix/embedding.html#embed-error}{\mathit{error}}\)¶

令 \(\mathit{gi}\) 为全局实例 global instance \(\href{../exec/runtime.html#syntax-store}{\mathit{store}}.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}]\)。
令 \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t\) 为全局类型 global type \(\mathit{gi}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}\) 的结构。
如果 \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\) 不是 \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\)，则返回 \(\href{../appendix/embedding.html#embed-error}{\mathsf{error}}\)。
将 \(\mathit{gi}.\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}\) 替换为 value \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\)。
返回更新后的存储。

\[\begin{split}~ \\ \begin{array}{lclll} \mathrm{global\_write}(S, a, v) &=& S' && (\mathrel{\mbox{if}} S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}} = \href{../syntax/types.html#syntax-mut}{\mathsf{var}}~t \wedge S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}} = v) \\ \mathrm{global\_write}(S, a, v) &=& \href{../appendix/embedding.html#embed-error}{\mathsf{error}} && (\mathrel{\mbox{otherwise}}) \\ \end{array}\end{split}\]