模块

对于模块,执行语义主要定义实例化,它分配模块及其包含定义的实例,从包含的内存初始化元素数据段,并在存在时调用启动函数。它还包括导出函数的调用

实例化依赖于一些辅助概念来进行导入类型检查分配实例。

外部类型

为了根据导入检查外部值,这些值通过外部类型进行分类。以下辅助类型规则相对于存储\(S\)指定此类型关系,其中引用的实例位于其中。

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a\)

  • 存储条目\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a]\)必须存在。

  • 然后\(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a\)外部类型\(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\)有效。

\[\frac{ }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}} }\]

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a\)

  • 存储条目\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\)必须存在。

  • 然后\(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a\)外部类型\(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}\)有效。

\[\frac{ }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}} }\]

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a\)

  • 存储条目\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\)必须存在。

  • 然后\(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a\)外部类型\(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\)有效。

\[\frac{ }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}} }\]

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a\)

  • 存储条目\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a]\)必须存在。

  • 然后\(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a\)外部类型\(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}\)有效。

\[\frac{ }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}} }\]

值类型

为了根据导出函数的参数类型检查参数,值通过值类型进行分类。以下辅助类型规则相对于存储\(S\)指定此类型关系,其中可能引用的地址位于其中。

数值 \(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)

\[\frac{ }{ S \href{../exec/modules.html#valid-val}{\vdash} t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c : t }\]

空引用 \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t\)

\[\frac{ }{ S \href{../exec/modules.html#valid-val}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t : t }\]

函数引用 \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~a\)

  • 外部值\(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a\)必须有效

  • 然后该值与引用类型\(\href{../syntax/types.html#syntax-reftype}{\mathsf{funcref}}\)有效。

\[\frac{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ S \href{../exec/modules.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~a : \href{../syntax/types.html#syntax-reftype}{\mathsf{funcref}} }\]

外部引用 \(\href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}~a\)

  • 该值与引用类型\(\href{../syntax/types.html#syntax-reftype}{\mathsf{externref}}\)有效。

\[\frac{ }{ S \href{../exec/modules.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}~a : \href{../syntax/types.html#syntax-reftype}{\mathsf{externref}} }\]

分配

存储\(S\)分配函数内存全局变量的新实例,如下面的辅助函数所定义。

函数

  1. \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}\)为要分配的函数\(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)为其模块实例

  2. \(a\)\(S\)中第一个空闲的函数地址

  3. \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)函数类型\(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[\href{../syntax/modules.html#syntax-func}{\mathit{func}}.\href{../syntax/modules.html#syntax-func}{\mathsf{type}}]\)

  4. \(\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}} \}\)

  5. \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\)追加到\(S\)\(\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\)中。

  6. 返回\(a\)

\[\begin{split}~\\[-1ex] \begin{array}{rlll} \href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}(S, \href{../syntax/modules.html#syntax-func}{\mathit{func}}, \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}) &=& S', \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}| \\ \href{../syntax/types.html#syntax-functype}{\mathit{functype}} &=& \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[\href{../syntax/modules.html#syntax-func}{\mathit{func}}.\href{../syntax/modules.html#syntax-func}{\mathsf{type}}] \\ \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}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\} \\ \end{array}\end{split}\]

主机函数

  1. \(\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}\) 为用于分配的主机函数,并令 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) 为其函数类型

  2. \(a\)\(S\)中第一个空闲的函数地址

  3. \(\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{hostcode}}~\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} \}\)

  4. \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\)追加到\(S\)\(\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\)中。

  5. 返回\(a\)

\[\begin{split}~\\[-1ex] \begin{array}{rlll} \href{../exec/modules.html#alloc-hostfunc}{\mathrm{allochostfunc}}(S, \href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}) &=& S', \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\[1ex] \mbox{其中:} \hfill \\ \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}| \\ \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{hostcode}}~\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\} \\ \end{array}\end{split}\]

注意

主机函数永远不会由 WebAssembly 语义本身分配,但可能由嵌入器分配。

表格

  1. \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) 为要分配的表格类型,并令 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\) 为初始化值。

  2. \((\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}})\)表格类型 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) 的结构。

  3. \(a\)\(S\) 中第一个空闲的表格地址

  4. \(\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{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n \}\),其中有 \(n\) 个元素设置为 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\)

  5. \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\) 附加到 \(S\)\(\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\) 中。

  6. 返回\(a\)

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}(S, \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) &=& S', \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} \\[1ex] \mbox{其中:} \hfill \\ \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} &=& \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \\ \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}| \\ \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{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\} \\ \end{array}\end{split}\]

内存

  1. \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) 为要分配的内存类型

  2. \(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}\)内存类型 \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) 的结构。

  3. \(a\)\(S\) 中第一个空闲的内存地址

  4. \(\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}}~(\def\mathdef2203#1{\mathtt{0x#1}}\mathdef2203{00})^{n \cdot 64\,\mathrm{Ki}} \}\),它包含 \(n\) 页清零的字节

  5. \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\) 附加到 \(S\)\(\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\) 中。

  6. 返回\(a\)

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}(S, \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}) &=& S', \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} \\[1ex] \mbox{其中:} \hfill \\ \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} &=& \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\} \\ \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}| \\ \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}}~(\def\mathdef2204#1{\mathtt{0x#1}}\mathdef2204{00})^{n \cdot 64\,\mathrm{Ki}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\} \\ \end{array}\end{split}\]

全局变量

  1. \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) 为要分配的全局变量类型,并令 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\) 为用于初始化全局变量的

  2. \(a\)\(S\) 中第一个空闲的全局变量地址

  3. \(\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}} \}\)

  4. \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\) 附加到 \(S\)\(\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\) 中。

  5. 返回\(a\)

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}(S, \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}) &=& S', \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} \\[1ex] \mbox{其中:} \hfill \\ \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}| \\ \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}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\} \\ \end{array}\end{split}\]

元素段

  1. \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\) 为元素的类型,并令 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast\) 为要分配的引用 向量。

  2. \(a\)\(S\) 中第一个空闲的元素地址

  3. \(\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{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \}\)

  4. \(\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}\) 附加到 \(S\)\(\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}\) 中。

  5. 返回\(a\)

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}(S, \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast) &=& S', \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}} \\[1ex] \mbox{其中:} \hfill \\ \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}| \\ \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{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}~\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}\} \\ \end{array}\end{split}\]

数据段

  1. \(b^\ast\) 为要分配的字节 向量。

  2. \(a\)\(S\) 中第一个空闲的数据地址

  3. \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\)数据实例 \(\{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~b^\ast \}\)

  4. \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\) 附加到 \(S\)\(\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}\) 中。

  5. 返回\(a\)

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}(S, b^\ast) &=& S', \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}} \\[1ex] \mbox{其中:} \hfill \\ \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}| \\ \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}} &=& \{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~b^\ast \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}~\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\} \\ \end{array}\end{split}\]

增长

  1. \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\) 为要增长的表实例\(n\) 为要增长的元素数量,\(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\) 为初始化值。

  2. \(\mathit{len}\)\(n\) 加上 \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\) 的长度。

  3. 如果\(\mathit{len}\) 大于或等于 \(2^{32}\),则失败。

  4. \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\)表类型 \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}\) 的结构。

  5. \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'\)\(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\),其中 \(\href{../syntax/types.html#syntax-limits}{\mathsf{min}}\) 更新为 \(\mathit{len}\)

  6. 如果\(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'\) 不是有效的,则失败。

  7. \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n\) 附加到 \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\)

  8. \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}\) 设置为表类型 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'~t\)

\[\begin{split}\begin{array}{rllll} \href{../exec/modules.html#grow-table}{\mathrm{growtable}}(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}, n, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) &=& \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}} = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}'~t \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}} = \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n \\ && ( \begin{array}[t]{@{}r@{~}l@{}} \mathrel{\mbox{if}} & \mathit{len} = n + |\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}| \\ \wedge & \mathit{len} < 2^{32} \\ \wedge & \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t = \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}} \\ \wedge & \href{../syntax/types.html#syntax-limits}{\mathit{limits}}' = \href{../syntax/types.html#syntax-limits}{\mathit{limits}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../syntax/types.html#syntax-limits}{\mathsf{min}} = \mathit{len} \\ \wedge & \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}' \mathrel{\mbox{ok}}) \\ \end{array} \\ \end{array}\end{split}\]

增长内存

  1. \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\) 为要增长的内存实例\(n\) 为要增长的页面 数量。

  2. 断言:\(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度可以被页面大小 \(64\,\mathrm{Ki}\) 整除。

  3. \(\mathit{len}\)\(n\) 加上 \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) 的长度除以页面大小 \(64\,\mathrm{Ki}\)

  4. 如果\(\mathit{len}\) 大于 \(2^{16}\),则失败。

  5. \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\)内存类型 \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\) 的结构。

  6. \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'\)\(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\),其中 \(\href{../syntax/types.html#syntax-limits}{\mathsf{min}}\) 更新为 \(\mathit{len}\)

  7. 如果\(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'\) 不是有效的,则失败。

  8. \(n\)\(64\,\mathrm{Ki}\) 字节(值为 \(\def\mathdef2205#1{\mathtt{0x#1}}\mathdef2205{00}\))附加到 \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\)

  9. \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\) 设置为内存类型 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'\)

\[\begin{split}\begin{array}{rllll} \href{../exec/modules.html#grow-mem}{\mathrm{growmem}}(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}, n) &=& \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}} = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}' \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}} = \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~(\def\mathdef2206#1{\mathtt{0x#1}}\mathdef2206{00})^{n \cdot 64\,\mathrm{Ki}} \\ && ( \begin{array}[t]{@{}r@{~}l@{}} \mathrel{\mbox{if}} & \mathit{len} = n + |\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| / 64\,\mathrm{Ki} \\ \wedge & \mathit{len} \leq 2^{16} \\ \wedge & \href{../syntax/types.html#syntax-limits}{\mathit{limits}} = \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}} \\ \wedge & \href{../syntax/types.html#syntax-limits}{\mathit{limits}}' = \href{../syntax/types.html#syntax-limits}{\mathit{limits}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../syntax/types.html#syntax-limits}{\mathsf{min}} = \mathit{len} \\ \wedge & \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}' \mathrel{\mbox{ok}}) \\ \end{array} \\ \end{array}\end{split}\]

模块

模块的分配函数需要一个合适的外部值列表,这些值假定与模块的导入向量匹配,一个模块的全局变量的初始化列表,以及模块的元素段引用向量列表。

  1. \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) 为要分配的模块\(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\) 为提供模块导入的外部值向量,\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 为模块全局变量的初始化\((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast\) 为模块元素段引用向量。

  2. 对于 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}\) 中的每个函数 \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}_i\),执行以下操作

    1. \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i\) 为从分配 \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}_i\)(用于下面定义的模块实例 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\))得到的函数地址

  3. 对于 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}}\) 中的每个 \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i\),执行以下操作

    1. \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_i~t_i\)表类型 \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i.\href{../syntax/modules.html#syntax-table}{\mathsf{type}}\)

    2. \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\) 为从分配 \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i.\href{../syntax/modules.html#syntax-table}{\mathsf{type}}\)(初始化值为 \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t_i\))得到的表地址

  4. 对于 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}}\) 中的每个内存 \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i\),执行以下操作

    1. \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i\) 为从分配 \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i.\href{../syntax/modules.html#syntax-mem}{\mathsf{type}}\) 得到的内存地址

  5. 对于 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}\) 中的每个全局变量 \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i\),执行以下操作

    1. \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\) 为从分配 \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i.\href{../syntax/modules.html#syntax-global}{\mathsf{type}}\)(初始化值为 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast[i]\))得到的全局变量地址

  6. 对于模块 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\) 中的每个 元素段 \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\),执行以下操作

    1. \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}_i\) 为通过 分配 一个 引用类型 \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}\)元素实例(其内容为 \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast[i]\))而得到的 元素地址

  7. 对于模块 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}\) 中的每个 数据段 \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i\),执行以下操作

    1. \(\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}_i\) 为通过 分配 一个内容为 \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{init}}\)数据实例 而得到的 数据地址

  8. \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast\) 为按索引顺序连接的 函数地址 \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i\)

  9. \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast\) 为按索引顺序连接的 表地址 \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\)

  10. \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast\) 为按索引顺序连接的 内存地址 \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i\)

  11. \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast\) 为按索引顺序连接的 全局地址 \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\)

  12. \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast\) 为按索引顺序连接的 元素地址 \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}_i\)

  13. \(\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast\) 为按索引顺序连接的 数据地址 \(\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}_i\)

  14. \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{\mathrm{mod}}^\ast\) 为从 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\) 中提取的 函数地址 列表,与 \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast\) 连接。

  15. \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_{\mathrm{mod}}^\ast\) 为从 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\) 中提取的 表地址 列表,与 \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast\) 连接。

  16. \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_{\mathrm{mod}}^\ast\) 为从 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\) 中提取的 内存地址 列表,与 \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast\) 连接。

  17. \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_{\mathrm{mod}}^\ast\) 为从 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\) 中提取的 全局地址 列表,与 \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast\) 连接。

  18. 对于模块 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}\) 中的每个 导出 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\),执行以下操作

    1. 如果 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\)函数索引 \(x\) 的函数导出,则令 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\)外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{\mathrm{mod}}^\ast[x])\)

    2. 否则,如果 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\)表索引 \(x\) 的表导出,则令 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\)外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_{\mathrm{mod}}^\ast[x])\)

    3. 否则,如果 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\)内存索引 \(x\) 的内存导出,则令 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\)外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_{\mathrm{mod}}^\ast[x])\)

    4. 否则,如果 \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\)全局索引 \(x\) 的全局导出,则令 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\)外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_{\mathrm{mod}}^\ast[x])\)

    5. \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\)导出实例 \(\{\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}), \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\}\)

  19. \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast\) 为按索引顺序连接的 导出实例 \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\)

  20. \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)模块实例 \(\{\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}),\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}~\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast\}\)

  21. 返回 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)

\[\begin{split}~\\ \begin{array}{rlll} \href{../exec/modules.html#alloc-module}{\mathrm{allocmodule}}(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, (\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast) &=& S', \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} \end{array}\end{split}\]

其中

\[\begin{split}\begin{array}{@{}rlll@{}} \href{../syntax/modules.html#syntax-table}{\mathit{table}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}} \\ \href{../syntax/modules.html#syntax-mem}{\mathit{mem}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}} \\ \href{../syntax/modules.html#syntax-global}{\mathit{global}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}} \\ \href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}} \\ \href{../syntax/modules.html#syntax-data}{\mathit{data}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}} \\ \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}} \\[1ex] \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} &=& \{~ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\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} \\[1ex] S_1, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast &=& \href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}^\ast(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}, \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}) \\ S_2, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast &=& \href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}^\ast(S_1, (\href{../syntax/modules.html#syntax-table}{\mathit{table}}.\href{../syntax/modules.html#syntax-table}{\mathsf{type}})^\ast, (\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t)^\ast) \quad (\mathrel{\mbox{where}} (\href{../syntax/modules.html#syntax-table}{\mathit{table}}.\href{../syntax/modules.html#syntax-table}{\mathsf{type}})^\ast = (\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t)^\ast) \\ S_3, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast &=& \href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}^\ast(S_2, (\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}.\href{../syntax/modules.html#syntax-mem}{\mathsf{type}})^\ast) \\ S_4, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast &=& \href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}^\ast(S_3, (\href{../syntax/modules.html#syntax-global}{\mathit{global}}.\href{../syntax/modules.html#syntax-global}{\mathsf{type}})^\ast, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast) \\ S_5, \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast &=& \href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}^\ast(S_4, (\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}.\href{../syntax/modules.html#syntax-elem}{\mathsf{type}})^\ast, (\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast) \\ S', \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast &=& \href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}^\ast(S_5, (\href{../syntax/modules.html#syntax-data}{\mathit{data}}.\href{../syntax/modules.html#syntax-data}{\mathsf{init}})^\ast) \\ \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast &=& \{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~(\href{../syntax/modules.html#syntax-export}{\mathit{export}}.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}), \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}} \}^\ast \\[1ex] \href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[x])^\ast \qquad~ (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{funcs}}(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast)) \\ \href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x])^\ast \qquad (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{tables}}(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast)) \\ \href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x])^\ast \qquad (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{mems}}(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast)) \\ \href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}[x])^\ast \qquad\!\!\! (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{globals}}(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast)) \\ \end{array}\end{split}\]

这里,符号 \(\mathrm{allocx}^\ast\) 是多个 分配 对象类型 \(X\) 的简写,定义如下:

\[\begin{split}\begin{array}{rlll} \mathrm{allocx}^\ast(S_0, X^n, \dots) &=& S_n, a^n \\[1ex] \mbox{其中对于所有 $i < n$:} \hfill \\ S_{i+1}, a^n[i] &=& \mathrm{allocx}(S_i, X^n[i], \dots) \end{array}\end{split}\]

此外,如果省略号 \(\dots\) 是一个序列 \(A^n\)(如全局变量或表格),则此序列的元素将逐点传递给分配函数。

注意

模块分配的定义与其关联函数的分配是相互递归的,因为生成的模块实例 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) 作为参数传递给函数分配器,以形成必要的闭包。在实现中,这种递归可以通过在辅助步骤中更改一个或另一个来轻松地解开。

实例化

给定一个 存储 \(S\),一个 模块 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) 使用 外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\) 的列表进行实例化,如下所示,这些值提供所需的导入。

实例化检查模块是否 有效 以及提供的导入是否 匹配 已声明的类型,否则可能会 *失败* 并出现错误。实例化也可能导致来自初始化活动段的表格或内存或执行开始函数的 陷阱。由 嵌入器 定义如何报告此类条件。

  1. 如果 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) 不是 有效 的,则

    1. 失败。

  2. 断言:\(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\)有效 的,具有 外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}}^m\) 对其 导入 进行分类。

  3. 如果 导入 的数量 \(m\) 不等于提供的 外部值 的数量 \(n\),则

    1. 失败。

  4. 对于 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\) 中的每个 外部值 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\)\(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}}^n\) 中的 外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\),执行以下操作:

    1. 如果 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) 在存储 \(S\) 中不是 有效 的,且具有 外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\),则

      1. 失败。

    2. 如果 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\)匹配 \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\),则

      1. 失败。

  1. \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}_{\mathrm{init}}\) 为辅助模块 实例 \(\{\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n), \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}\}\),它仅包含导入的全局变量以及来自最终模块实例 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\)(定义如下)的导入和分配的函数。

  2. \(F_{\mathrm{init}}\) 为辅助 \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}_{\mathrm{init}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}\)

  3. 将帧 \(F_{\mathrm{init}}\) 推入堆栈。

  4. \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 为由 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\)\(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\) 确定的 全局 初始化 的向量。这些可以按如下方式计算。

    1. 对于 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}\) 中的每个全局变量 \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i\),执行以下操作

      1. \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\)评估 初始化表达式 \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i.\href{../syntax/modules.html#syntax-global}{\mathsf{init}}\) 的结果。

    2. 断言:由于 验证,帧 \(F_{\mathrm{init}}\) 现在位于堆栈顶部。

    3. \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\)\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) 按索引顺序的串联。

  5. \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast\) 为由 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) 中的 元素段 确定的 引用 向量列表。这些可以按如下方式计算。

    1. 对于 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\) 中的每个 元素段 \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\),以及对于 \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}\) 中的每个元素 表达式 \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{ij}\),执行以下操作:

      1. \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{ij}\) 为对初始化表达式 \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{ij}\) 进行 求值 的结果。

    2. \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast_i\) 为按照索引 \(j\) 的顺序连接函数元素 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{ij}\) 的结果。

    3. \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast\) 为按照索引 \(i\) 的顺序连接函数元素向量 \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast_i\) 的结果。

  6. 从栈中弹出帧 \(F_{\mathrm{init}}\)

  7. \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) 为一个新的模块实例,该实例从存储 \(S\) 中的 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) 分配,具有导入 \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\)、全局初始化值 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 和元素段内容 \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast\),并令 \(S'\) 为模块分配产生的扩展存储。

  8. \(F\) 为辅助 \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}\)

  9. 将帧 \(F\) 推入栈中。

  10. 对于 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\) 中的每个 元素段 \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\),其 模式\(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}_i, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~\mathit{einstr}^\ast_i~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \}\) 形式,执行以下操作:

    1. \(n\) 为向量 \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}\) 的长度。

    2. 执行 指令序列 \(\mathit{einstr}^\ast_i\)

    3. 执行 指令 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0\)

    4. 执行 指令 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\)

    5. 执行 指令 \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}_i~i\)

    6. 执行 指令 \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~i\)

  11. 对于 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\) 中的每个 元素段 \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\),其 模式\(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{declarative}}\) 形式,执行以下操作:

    1. 执行 指令 \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~i\)

  12. 对于 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}\) 中的每个 数据段 \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i\),其 模式\(\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}_i, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~\mathit{dinstr}^\ast_i~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \}\) 形式,执行以下操作:

    1. 断言:\(\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}_i\)\(0\)

    2. \(n\) 为向量 \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{init}}\) 的长度。

    3. 执行 指令序列 \(\mathit{dinstr}^\ast_i\)

    4. 执行 指令 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0\)

    5. 执行 指令 \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\)

    6. 执行 指令 \(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~i\)

    7. 执行 指令 \(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data.drop}}~i\)

  13. 如果 起始函数 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}\) 不为空,则

    1. \(\href{../syntax/modules.html#syntax-start}{\mathit{start}}\)起始函数 \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}\)

    2. 执行 指令 \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~\href{../syntax/modules.html#syntax-start}{\mathit{start}}.\href{../syntax/modules.html#syntax-start}{\mathsf{func}}\)

  14. 断言:由于 验证,帧 \(F\) 现在位于栈顶。

  15. 从栈中弹出帧 \(F\)

\[\begin{split}~\\ \begin{array}{@{}rcll} \href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^k) &=& S'; F; \begin{array}[t]{@{}l@{}} \mathrm{runelem}_0(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^n[0])~\dots~\mathrm{runelem}_{n-1}(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^n[n-1]) \\ \mathrm{rundata}_0(\href{../syntax/modules.html#syntax-data}{\mathit{data}}^m[0])~\dots~\mathrm{rundata}_{m-1}(\href{../syntax/modules.html#syntax-data}{\mathit{data}}^m[m-1]) \\ (\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~\href{../syntax/modules.html#syntax-start}{\mathit{start}}.\href{../syntax/modules.html#syntax-start}{\mathsf{func}})^? \\ \end{array} \\ &(\mathrel{\mbox{if}} & \href{../valid/modules.html#valid-module}{\vdash} \href{../syntax/modules.html#syntax-module}{\mathit{module}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}}^k \href{../syntax/types.html#syntax-functype}{\rightarrow} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{ex}}^\ast \\ &\wedge& (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^k \\ &\wedge& (\href{../valid/types.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} \href{../valid/types.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}})^k \\[1ex] &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}} = \href{../syntax/modules.html#syntax-global}{\mathit{global}}^\ast \\ &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}} = \href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^n \\ &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}} = \href{../syntax/modules.html#syntax-data}{\mathit{data}}^m \\ &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \href{../syntax/modules.html#syntax-start}{\mathit{start}}^? \\ &\wedge& (\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{\mathrm{g}} = \href{../syntax/modules.html#syntax-global}{\mathit{global}}.\href{../syntax/modules.html#syntax-global}{\mathsf{init}})^\ast \\ &\wedge& (\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{\mathrm{e}}^\ast = \href{../syntax/modules.html#syntax-elem}{\mathit{elem}}.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}})^n \\[1ex] &\wedge& S', \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} = \href{../exec/modules.html#alloc-module}{\mathrm{allocmodule}}(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^k, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, (\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^n) \\ &\wedge& F = \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \} \\[1ex] &\wedge& (S'; F; \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{\mathrm{g}} \href{../exec/conventions.html#exec-notation}{\hookrightarrow}^\ast S'; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})^\ast \\ &\wedge& ((S'; F; \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{\mathrm{e}} \href{../exec/conventions.html#exec-notation}{\hookrightarrow}^\ast S'; F; \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})^\ast)^n) \\ \end{array}\end{split}\]

其中

\[\begin{split}\begin{array}{@{}l} \mathrm{runelem}_i(\{\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~\mathit{et}, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}^n, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}}\}) \quad=\quad \epsilon \\ \mathrm{runelem}_i(\{\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~\mathit{et}, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}^n, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}} \{\href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~x, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\}\}) \quad=\\ \qquad \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~x~i)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~i) \\ \mathrm{runelem}_i(\{\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~\mathit{et}, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}^n, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{declarative}}\}) \quad=\\ \qquad (\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~i) \\[1ex] \mathrm{rundata}_i(\{\href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^n, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}}\}) \quad=\quad \epsilon \\ \mathrm{rundata}_i(\{\href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^n, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}} \{\href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~0, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\}\}) \quad=\\ \qquad \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~i)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data.drop}}~i) \\ \end{array}\end{split}\]

注意

模块 分配评估 全局 初始化程序和 元素段 是相互递归的,因为全局初始化 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 和元素段内容 \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast\) 被传递给模块分配器,同时依赖于模块实例 \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) 和分配返回的存储 \(S'\)。但是,这种递归只是一个规范工具。在实践中,初始化值可以 预先确定,方法是分阶段进行模块分配,首先,在存储中预分配模块自己的 函数实例,然后评估初始化表达式,然后分配模块实例的其余部分,最后将新函数实例的 \(\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}\) 字段设置为该模块实例。这是可能的,因为 验证 确保初始化表达式实际上不能调用函数,只能获取它们的引用。

在发生任何可观察到的存储修改之前,都会检查所有失败条件。存储修改不是原子的;它以可能与其他线程交错的单个步骤发生。

评估 常量表达式 不会影响存储。

调用

一旦 模块实例化,任何导出的函数都可以通过其 函数地址 \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\)存储 \(S\) 中以及适当的参数 列表 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 从外部进行 调用

如果参数不符合 函数类型,则调用可能会 失败 并出现错误。调用也可能导致 陷阱。由 嵌入器 定义如何报告此类条件。

注意

如果 嵌入器 API 在执行调用之前,静态或动态地自行执行类型检查,则不会发生除陷阱之外的其他故障。

执行以下步骤

  1. 断言:\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}]\) 存在。

  2. \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\)函数实例 \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}]\)

  3. \([t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m]\)函数类型 \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\)

  4. 如果提供的参数值的长度 \(|\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast|\) 与预期参数的数量 \(n\) 不同,则

    1. 失败。

  5. 对于 \(t_1^n\) 中的每个 值类型 \(t_i\)\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 中对应的 \(val_i\),执行

    1. 如果 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) 对值类型 \(t_i\) 不是 有效的,则

      1. 失败。

  6. \(F\) 为虚拟 \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{\}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}\)

  7. 将帧 \(F\) 推入栈中。

  8. 将值 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) 推送到堆栈。

  9. 调用 地址为 \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) 的函数实例。

函数返回后,执行以下步骤

  1. 断言:由于 验证,堆栈顶部有 \(m\)

  2. 从堆栈中弹出 \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{res}}^m\)

  3. 断言:由于 验证,帧 \(F\) 现在位于栈顶。

  4. 从栈中弹出帧 \(F\)

\(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{res}}^m\) 作为调用的结果返回。

\[\begin{split}~\\[-1ex] \begin{array}{@{}lcl} \href{../exec/modules.html#exec-invocation}{\mathrm{invoke}}(S, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n) &=& S; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) \\ &(\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}} = [t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m] \\ &\wedge& (S \href{../exec/modules.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t_1)^n \\ &\wedge& F = \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{\}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}) \\ \end{array}\end{split}\]