1. 简介
1.1. 简介
WebAssembly(缩写为 Wasm [1])是一种为高效执行和紧凑表示而设计的安全、可移植、低级代码格式。它的主要目标是在 Web 上启用高性能应用程序,但它不做出任何特定于 Web 的假设或提供特定于 Web 的功能,因此它也可以在其他环境中使用。
WebAssembly 是一种由 W3C 社区小组 开发的开放标准。
本文档描述了 WebAssembly 核心标准的 2.0 版(2024-09-13 草案)。它旨在被未来的增量版本取代,这些版本将包含更多新功能。
1.1.1. 设计目标
WebAssembly 的设计目标如下
-
快速、安全、可移植的语义
-
快速:以接近原生代码的性能执行,利用所有当代硬件通用的功能。
-
安全:代码在内存安全的 [2]、沙盒环境中执行,以防止数据损坏或安全漏洞。
-
定义明确:以易于非正式和正式推理的方式完整准确地定义有效程序及其行为。
-
硬件无关:可以在所有现代架构上编译,包括台式机或移动设备和嵌入式系统。
-
语言无关:不偏袒任何特定语言、编程模型或对象模型。
-
平台无关:可以嵌入到浏览器中,作为独立的 VM 运行,或集成到其他环境中。
-
开放:程序可以通过简单通用的方式与其环境进行交互。
-
-
高效、可移植的表示
-
紧凑:具有二进制格式,该格式速度快,因为比典型的文本或原生代码格式更小。
-
模块化:程序可以分成更小的部分,这些部分可以分别传输、缓存和使用。
-
高效:可以在快速单次传递中进行解码、验证和编译,无论是即时 (JIT) 还是提前 (AOT) 编译。
-
可流式传输:允许在看到所有数据之前尽早开始解码、验证和编译。
-
可并行化:允许将解码、验证和编译分成许多独立的并行任务。
-
可移植:不做出现代硬件普遍支持的架构假设。
-
WebAssembly 代码还旨在易于检查和调试,尤其是在像 Web 浏览器这样的环境中,但这些功能超出了本规范的范围。
1.1.2. 范围
本质上,WebAssembly 是一种虚拟指令集架构(虚拟 ISA)。因此,它有许多用例,可以嵌入到许多不同的环境中。为了涵盖它们的各种用途并实现最大程度的重复使用,WebAssembly 规范被分成多个文档并分层。
本文档关注 WebAssembly 的核心 ISA 层。它定义了指令集、二进制编码、验证和执行语义,以及文本表示。但是,它没有定义 WebAssembly 程序如何与其执行的特定环境交互,也没有定义如何从这样的环境中调用它们。
相反,本规范由其他文档补充,这些文档定义了与特定嵌入环境(例如 Web)的接口。这些将分别定义适合给定环境的 WebAssembly 应用程序编程接口(API)。
1.1.3. 安全注意事项
WebAssembly 并没有提供访问代码执行环境的任何环境访问权限。任何与环境的交互,例如 I/O、访问资源或操作系统调用,只能通过调用由 嵌入器 提供并导入到 WebAssembly 模块 的 函数 来执行。嵌入器可以通过控制或限制其提供导入的函数功能来建立适合相应环境的安全策略。这些考虑因素是嵌入器的责任,也是特定环境 API 定义 的主题。
由于 WebAssembly 旨在被翻译成直接在主机硬件上运行的机器代码,因此它可能容易受到硬件级别侧信道攻击。在存在此问题的环境中,嵌入器可能需要采取适当的缓解措施来隔离 WebAssembly 计算。
1.1.4. 依赖项
WebAssembly 依赖于两个现有标准
但是,为了使本规范自包含,上述标准的相关方面在本规范中定义并形式化,例如 二进制表示 和 舍入 浮点值,以及 值范围 和 UTF-8 编码 Unicode 字符。
注意
上述标准是所有相应定义的权威来源。本规范中给出的形式化旨在与这些定义相匹配。描述的语法或语义中存在的任何差异应视为错误。
1.2. 概述
1.2.1. 概念
WebAssembly 编码了一种低级、类似汇编的编程语言。这种语言围绕以下概念构建。
- 值
-
WebAssembly 只提供四种基本数字类型。这些是整数和 [IEEE-754-2019] 数字,每种类型都具有 32 位和 64 位宽度。32 位整数也用作布尔值和内存地址。这些类型上的常见运算可用,包括它们之间所有转换的完整矩阵。没有区分有符号和无符号整数类型。相反,整数由各自的运算解释为二进制补码表示中的无符号或有符号。
除了这些基本数字类型之外,还有一个单一的 128 位宽向量类型,表示不同类型的打包数据。支持的表示形式是 4 个 32 位或 2 个 64 位 [IEEE-754-2019] 数字,或不同宽度的打包整数值,特别是 2 个 64 位整数、4 个 32 位整数、8 个 16 位整数或 16 个 8 位整数。
最后,值可以由表示指向不同类型实体的指针的不透明引用组成。与其他类型不同,它们的大小或表示形式不可观察。
- 指令
-
WebAssembly 的计算模型基于堆栈机。代码由按顺序执行的指令序列组成。指令操作隐式操作数堆栈 [1] 上的值,并分为两大类。简单指令对数据执行基本操作。它们从操作数堆栈中弹出参数,并将结果压回堆栈。控制指令改变控制流。控制流是结构化的,这意味着它用嵌套良好的结构(例如块、循环和条件语句)来表达。分支只能针对此类结构。
- 陷阱
-
在某些情况下,某些指令可能会产生陷阱,这会立即中止执行。陷阱无法由 WebAssembly 代码处理,而是报告给外部环境,在那里它们通常可以被捕获。
- 函数
-
代码被组织成单独的函数。每个函数都接受一系列值作为参数,并返回一系列值作为结果。函数可以相互调用,包括递归调用,从而产生一个无法直接访问的隐式调用堆栈。函数还可以声明可变的局部变量,这些变量可用作虚拟寄存器。
- 表
-
表是具有特定元素类型的不透明值的数组。它允许程序通过动态索引操作数间接选择这些值。目前,唯一可用的元素类型是无类型函数引用或对外部主机值的引用。因此,程序可以通过对表的动态索引间接调用函数。例如,这允许通过表索引模拟函数指针。
- 线性内存
-
线性内存是原始字节的连续可变数组。这种内存是在初始大小下创建的,但可以动态增长。程序可以在任何字节地址(包括未对齐的地址)从线性内存加载值或存储值。整数加载和存储可以指定一个比相应值类型大小更小的存储大小。如果访问超出当前内存大小的范围,则会发生陷阱。
- 模块
-
WebAssembly 二进制文件采用模块的形式,其中包含函数、表和线性内存的定义,以及可变或不可变的全局变量。定义也可以被导入,指定一个模块/名称对以及合适的类型。每个定义可以选择在多个名称下被导出。除了定义之外,模块还可以定义其内存或表的初始化数据,这些数据采用复制到给定偏移量的段的形式。它们还可以定义一个启动函数,该函数会自动执行。
- 嵌入器
-
WebAssembly 实现通常会嵌入到主机环境中。此环境定义了如何启动模块加载、如何提供导入(包括主机端定义)以及如何访问导出。但是,任何特定嵌入的细节超出了本规范的范围,而是由补充的、环境特定的 API 定义提供。
在实践中,实现不必维护实际的操作数堆栈。相反,可以将堆栈视为一组匿名寄存器,这些寄存器由指令隐式引用。类型系统 确保堆栈高度,以及任何引用的寄存器,始终是静态已知的。
1.2.2. 语义阶段
从概念上讲,WebAssembly 的语义分为三个阶段。对于语言的每个部分,规范都指定了每个阶段。
- 解码
-
WebAssembly 模块以二进制格式分发。解码处理该格式并将其转换为模块的内部表示。在本规范中,此表示形式由抽象语法建模,但实际实现可以改为直接编译为机器代码。
- 验证
-
已解码的模块必须是有效的。验证检查许多良好格式条件,以保证模块是有意义且安全的。特别是,它执行函数及其主体中指令序列的类型检查,确保例如操作数堆栈始终一致地使用。
- 执行
-
最后,有效的模块可以被执行。执行可以进一步分为两个阶段
实例化。模块实例是模块的动态表示,包含其自己的状态和执行堆栈。实例化执行模块主体本身,为其所有导入提供定义。它初始化全局变量、内存和表,并在定义的情况下调用模块的启动函数。它返回模块导出的实例。
调用。实例化后,可以通过调用模块实例上的导出函数来启动进一步的 WebAssembly 计算。给定必需的参数,这将执行相应函数并返回其结果。
实例化和调用是嵌入环境中的操作。
2. 结构
2.1. 约定
WebAssembly 是一种编程语言,具有多种具体表示形式(其 二进制格式 和 文本格式)。两者都映射到一个通用结构。为了简洁起见,这种结构以抽象语法的形式描述。本规范的所有部分都根据此抽象语法定义。
2.1.1. 语法表示法
在定义抽象语法的语法规则时,采用以下约定。
-
终结符(原子)以无衬线字体或符号形式编写: i32,end,→,[,].
-
非终结符以斜体形式编写: valtype,instr.
-
An 是 n≥0 次 A 的序列。
-
A∗ 是一个可能是空的 A 迭代序列。 (这是 An 的简写,在 n 不相关的情况下使用。)
-
A+ 是一个非空的 A 迭代序列。 (这是 An 的简写,其中 n≥1。)
-
A? 是 A 的可选出现。 (这是 An 的简写,其中 n≤1。)
-
产生式写作 sym::=A1 ∣ … ∣ An.
-
大型产生式可以拆分为多个定义,用显式省略号 (sym::=A1 ∣ …) 结束第一个定义,并用省略号 (sym::=… ∣ A2) 开始后续定义。
-
有些产生式用圆括号 (“(ifcondition)”) 附加了边条件,用于简化将产生式组合扩展为多个独立情况的写法。
-
如果同一个元变量或非终结符在产生式中多次出现,则所有这些出现必须具有相同的实例化。 (这是对多个不同变量相等的要求的简写。)
2.1.2. 辅助符号
在处理语法结构时,还会使用以下符号
-
ϵ 表示空序列。
-
∣s∣ 表示序列 s 的长度。
-
s[i] 表示序列 s 的第 i 个元素,从 0 开始。
-
s[i:n] 表示序列 s[i] … s[i+n−1] 的子序列。
-
swith[i]=A 表示与 s 相同的序列,但将第 i 个元素替换为 A。
-
concat(s∗) 表示通过连接所有序列 si(在 s∗ 中)而形成的扁平序列。
此外,采用以下约定。
-
符号 xn,其中 x 是一个非终结符,被视为一个元变量,它遍历 x 的相应序列(类似于 x∗,x+,x?)。
-
当给定一个序列 xn 时,则假设序列 (A1 x A2)n 中的 x 的出现与 xn 呈逐点对应关系(类似于 x∗,x+,x?)。这隐式地表达了一种在序列上映射语法结构的形式。
以下形式的产生式被解释为记录,它们将一组固定的字段 fieldi 分别映射到“值” Ai.
采用以下符号来操作这些记录。
-
r.field 表示 field 组件在 r 中的内容。
-
rwithfield=A 表示与 r 相同的记录,只是 field 组件的内容被替换为 A.
-
r1⊕r2 表示两个具有相同字段序列的记录的组合,通过逐点追加每个序列来完成。
{field1A1∗,field2A2∗,…}⊕{field1B1∗,field2B2∗,…}={field1A1∗ B1∗,field2A2∗ B2∗,…} -
⨁r∗ 表示对一个记录序列进行组合,按顺序进行;如果序列为空,则结果记录的所有字段都为空。
序列和记录的更新符号递归地推广到通过“路径”访问的嵌套组件 pth::=([…]∣.field)+
2.1.3. 向量
向量 是形式为 An(或 A∗)的有界序列,其中 A 可以是值或复杂结构。一个向量最多可以有 232−1 个元素。
2.2. 值
WebAssembly 程序操作原始数值值。此外,在程序的定义中,值的不变序列用来表示更复杂的数据,例如文本字符串或其他向量。
2.2.1. 字节
最简单的值形式是原始的未解释字节。在抽象语法中,它们用十六进制文字表示。
2.2.1.1. 约定
-
元变量 b 代表字节。
-
字节有时被解释为自然数 n<256。
2.2.2. 整数
不同类别的整数具有不同的值范围,它们由它们的位宽 N 以及它们是无符号还是有符号来区分。
类 iN 定义了未解释的整数,其有符号解释可能根据上下文而有所不同。在抽象语法中,它们表示为无符号值。但是,某些操作会 转换 它们为基于二进制补码解释的有符号值。
2.2.2.1. 约定
-
元变量 m,n,i 表示整数。
-
数字可以用简单的算术表示,如上面的语法所示。为了区分 2N 这样的算术运算和 (1)N 这样的序列,后者用括号来区分。
2.2.3. 浮点数
浮点数数据表示与 [IEEE-754-2019] 标准(第 3.3 节)中相应的二进制格式相对应的 32 位或 64 位值。
每个值都有一个符号和一个大小。 大小可以表示为形式为 m0.m1m2…mM⋅2e, 其中 e 是指数,m 是尾数,其最高有效位 m0 是 1,或者表示为非规格化数,其中指数固定为最小可能值,m0 是 0; 非规格化数中包括正零和负零值。 由于尾数是二进制值,因此规格化数表示为 (1+m⋅2−M)⋅2e, 其中 M 是 m 的位宽; 非规格化数也是如此。
可能的大小还包括特殊值 ∞ (无穷大)和 nan (NaN,非数字)。 NaN 值具有一个有效载荷,它描述了底层 二进制表示 中的尾数位。 信号 NaN 和安静 NaN 之间没有区别。
规范 NaN 是一个浮点值 ±nan(canonN),其中 canonN 是一个有效载荷,其最高有效位为 1,而其他所有位都为 0。
算术 NaN 是一个浮点值 ±nan(n),其中 n≥canonN,使得最高有效位为 1,而其他所有位都为任意值。
注意
在抽象语法中,次正规数通过尾数的开头 0 来区分。次正规数的指数与正规数的最小可能指数相同。仅在 二进制表示 中,次正规数的指数以与任何正规数的指数不同的方式编码。
这里定义的规范 NaN 概念与 [IEEE-754-2019] 标准(第 3.5.2 节)为十进制交换格式定义的规范 NaN 概念无关。
2.2.3.1. 约定
-
元变量 z 涵盖浮点值,其含义从上下文中清楚。
2.2.4. 向量
数值向量 是 128 位值,由向量指令(也称为 SIMD 指令,单指令多数据)处理。它们在抽象语法中使用 i128 表示。通道类型(整数 或 浮点数)和通道大小的解释由对它们进行操作的特定指令确定。
2.2.5. 名称
名称 是字符的序列,字符是 [UNICODE](第 2.4 节)中定义的标量值。
由于 二进制格式 的限制,名称的长度受其 UTF-8 编码长度的限制。
2.2.5.1. 约定
-
字符(Unicode 标量值)有时与自然数 n<1114112 可互换使用。
2.3. 类型
WebAssembly 中的各种实体按类型分类。类型在 验证、实例化 以及可能 执行 期间进行检查。
2.3.1. 数值类型
数值类型 用于对数值进行分类。
类型 i32 和 i64 分别对应于 32 位和 64 位整数。整数本身并非有符号或无符号,它们的解释由各个操作决定。
类型 f32 和 f64 分别对应于 32 位和 64 位浮点数。它们分别对应于二进制浮点数表示,也称为单精度和双精度,如 [IEEE-754-2019] 标准(第 3.3 节)中所定义。
数值类型是透明的,这意味着它们的位模式是可以观察到的。数值类型的值可以存储在 内存 中。
2.3.1.1. 约定
2.3.2. 向量类型
向量类型 用于对由向量指令处理的 数值 向量进行分类(也称为SIMD 指令,单指令多数据)。
类型 v128 对应一个包含128位整型或浮点型数据的打包向量。打包数据可以解释为有符号或无符号整型,单精度或双精度浮点型值,或单个128位类型。解释方式由各个操作确定。
向量类型,如同 数字类型,是透明的,这意味着它们的位模式是可以观察到的。向量类型的值可以存储在 内存 中。
2.3.2.1. 约定
2.3.3. 引用类型
引用类型对运行时 存储 中对象的的一级引用进行分类。
类型 funcref 表示所有对 函数 的引用的无限并集,无论它们的 函数类型 是什么。
类型 externref 表示所有由 嵌入器 拥有并可以以这种类型传递到 WebAssembly 中的引用的无限并集。
引用类型是不透明的,这意味着它们的尺寸或位模式都无法观察到。引用类型的值可以存储在 表格 中。
2.3.4. 值类型
值类型对 WebAssembly 代码可以计算的值和变量接受的值进行分类。它们要么是 数字类型,要么是 向量类型,要么是 引用类型。
2.3.4.1. 约定
-
元变量 t 在上下文中明确的情况下,表示值类型或其子类。
2.3.5. 结果类型
结果类型对 执行 指令 或 函数 的结果进行分类,结果是一个值序列,用方括号表示。
2.3.6. 函数类型
函数类型对 函数 的签名进行分类,将参数向量映射到结果向量。它们也用于对 指令 的输入和输出进行分类。
2.3.7. 限制
限制 用于对与 内存类型 和 表格类型 相关的可调整大小的存储的大小范围进行分类。
如果没有指定最大值,则相应的存储可以增长到任何大小。
2.3.8. 内存类型
内存类型 用于对线性 内存 及其大小范围进行分类。
这些限制会约束内存的最小大小以及可选的最大大小。限制以 页面大小 为单位。
2.3.9. 表格类型
表格类型 用于对在给定大小范围内包含 引用类型 元素的 表格 进行分类。
与内存类似,表格也会受到限制,用于约束其最小大小和可选的最大大小。限制以条目数为单位。
注意
在 WebAssembly 的未来版本中,可能会引入其他元素类型。
2.3.10. 全局类型
全局类型 用于对 全局变量 进行分类,这些变量会保存一个值,并且可以是可变的,也可以是不可变的。
2.3.11. 外部类型
外部类型 用于对 导入 和 外部值 及其相应的类型进行分类。
2.3.11.1. 约定
以下辅助符号用于外部类型序列。它以保留顺序的方式筛选出特定类型的条目。
-
funcs(externtype∗)=[functype ∣ (func functype)∈externtype∗]
-
tables(externtype∗)=[tabletype ∣ (table tabletype)∈externtype∗]
-
mems(externtype∗)=[memtype ∣ (mem memtype)∈externtype∗]
-
globals(externtype∗)=[globaltype ∣ (global globaltype)∈externtype∗]
2.4. 指令
WebAssembly 代码由一系列指令组成。其计算模型基于堆栈机,指令在隐式操作数堆栈上操作值,消耗(弹出)参数值并生成或返回(压入)结果值。
除了来自堆栈的动态操作数之外,一些指令还具有静态立即参数,通常是索引或类型注释,它们是指令本身的一部分。
一些指令在结构上是结构化的,因为它们对嵌套的指令序列进行括号。
以下部分将指令分为多个不同的类别。
2.4.1. 数值指令
数值指令提供对特定类型的数值值的基本操作。这些操作与硬件中可用的相应操作密切匹配。
数值指令按数值类型划分。对于每种类型,可以区分几个子类别
-
常量:返回一个静态常量。
-
一元运算:消耗一个操作数并生成一个相应类型的结果。
-
二元运算:消耗两个操作数并生成一个相应类型的结果。
-
测试:消耗一个相应类型的操作数并生成一个布尔整型结果。
-
比较:消耗两个相应类型的操作数并生成一个布尔整型结果。
-
转换:消耗一个类型的值并生成另一个类型的结果(转换的源类型是“_”之后的那个)。
一些整型指令有两种形式,其中一个符号位注释sx区分操作数是作为解释为无符号还是有符号整数。对于其他整型指令,使用二进制补码进行有符号解释意味着它们的行为相同,无论符号位如何。
2.4.1.1. 约定
有时,根据以下语法简写将运算符分组在一起会很方便。
2.4.2. 向量指令
向量指令(也称为SIMD 指令,即单指令多数据)提供了对值 的基本操作向量类型.
向量指令的命名约定包括一个前缀,该前缀决定了操作数的解释方式。该前缀描述了操作数的 *形状*,写成 txN,由一个打包的 数值类型 t 和该类型的 *通道* 数 N 组成。操作在每个通道的值上逐点执行。
以 v128 为前缀的指令不涉及特定解释,并将 v128 视为 i128 值或 128 个独立位的向量。
向量指令可以分组到几个子类别中
-
常量:返回一个静态常量。
-
测试:消耗一个 v128 操作数并生成一个布尔整型结果。
-
扩展:消耗一个数值类型的值并生成一个指定形状的 v128 结果。
-
提取通道:消耗一个 v128 操作数并返回给定通道中的数值。
一些向量指令有一个有符号性注释 sx,它区分操作数中的元素是 解释 为 无符号 还是 有符号 整数。对于其他向量指令,使用二进制补码进行有符号解释意味着它们的行为相同,无论有符号性如何。
2.4.2.1. 约定
有时,根据以下语法简写将运算符分组在一起会很方便。
2.4.3. 引用指令
此组指令与访问引用相关。
这些指令分别生成空值、检查空值或生成对给定函数的引用。
2.4.4. 参数指令
此组指令可以在任何值类型的操作数上进行操作。
The drop instruction simply throws away a single operand.
The select instruction selects one of its first two operands based on whether its third operand is zero or not. It may include a value type determining the type of these operands. If missing, the operands must be of numeric type.
注意
In future versions of WebAssembly, the type annotation on select may allow for more than a single value being selected at the same time.
2.4.5. 变量指令
这些指令分别获取或设置变量的值。The local.tee instruction is like local.set but also returns its argument.
2.4.6. 表指令
这组指令与表 table 相关。
指令 table.get 和 table.set 分别用于加载或存储表中的元素。
指令 table.size 返回表的当前大小。指令 table.grow 按给定的增量扩展表,并返回之前的大小,如果无法分配足够的空间,则返回 −1。它还接受新分配的条目的初始化值。
指令 table.fill 将指定范围内所有条目设置为给定值。
指令 table.copy 将元素从源表区域复制到可能重叠的目标区域;第一个索引表示目标。指令 table.init 将元素从 被动元素段 复制到表中。指令 elem.drop 防止进一步使用被动元素段。此指令旨在用作优化提示。在元素段被丢弃后,其元素将无法再被检索,因此此段使用的内存可能会被释放。
另一个访问表的指令是 控制指令 call_indirect。
2.4.7. 内存指令
这组指令涉及线性 内存。
使用 load 和 store 指令访问内存,这些指令对应不同的 数字类型。它们都接受一个 *内存立即数* memarg,其中包含地址 *偏移量* 和预期 *对齐方式*(用 2 的幂的指数表示)。整数加载和存储可以选择指定一个比相应值类型 位宽 更小的 *存储大小*。在加载的情况下,需要一个符号扩展模式 sx 来选择适当的行为。
向量加载可以指定一个大小为 v128 位宽 一半的形状。每个车道的大小是其正常大小的一半,符号扩展模式 sx 随后指定如何将较小的车道扩展到较大的车道。或者,向量加载可以执行 *splat*,这样只加载指定存储大小的单个车道,并将结果复制到所有车道。
静态地址偏移量加到动态地址操作数,产生一个 33 位 *有效地址*,该地址是访问内存的零基索引。所有值都以 小端 字节顺序读取和写入。如果任何被访问的内存字节位于内存当前大小暗示的地址范围之外,则会导致 陷阱。
注意
WebAssembly 的未来版本可能会提供具有 64 位地址范围的内存指令。
指令 memory.size 返回内存的当前大小。指令 memory.grow 通过给定的增量扩展内存并返回之前的大小,如果无法分配足够的内存,则返回 −1。这两个指令都以 页大小 为单位。
指令 memory.fill 将区域中的所有值设置为给定的字节。指令 memory.copy 将数据从源内存区域复制到可能重叠的目标区域。指令 memory.init 将数据从 被动数据段 复制到内存中。指令 data.drop 阻止进一步使用被动数据段。此指令旨在用作优化提示。在数据段被丢弃后,其数据将无法再检索,因此此段使用的内存可能会被释放。
2.4.8. 控制指令
此组中的指令影响控制流。
指令 nop 什么也不做。
unreachable 指令会导致无条件的 陷阱。
block、loop 和 if 指令是结构化指令。它们将嵌套的指令序列(称为块)括起来,并以 end 或 else 伪指令终止或分隔。根据语法规定,它们必须是嵌套良好的。
结构化指令可以根据其注释的块类型在操作数栈上消耗输入并产生输出。它可以作为一个 类型索引,该索引引用一个合适的 函数类型,或者作为一个可选的 值类型 内联,这是一种函数类型 []→[valtype?] 的简写。
每个结构化控制指令都引入一个隐式的标签。标签是分支指令的目标,这些分支指令使用 标签索引 引用它们。与其他 索引空间 不同,标签的索引是按嵌套深度相对的,也就是说,标签 0 指的是包围引用分支指令的最内层结构化控制指令,而增加的索引指的是更外层的那些指令。因此,标签只能从内部关联的结构化控制指令中引用。这也意味着分支只能被定向到外部,“中断”它们所针对的控制结构的块。确切的效果取决于该控制结构。在 block 或 if 的情况下,它是一个向前跳转,在匹配的 end 之后恢复执行。在 loop 的情况下,它是一个向后跳转到循环的开头。
注意
这强制执行结构化控制流。直观地,一个针对 block 或 if 的分支的行为类似于大多数类似 C 的语言中的 break 语句,而一个针对 loop 的分支的行为类似于 continue 语句。
分支指令有几种形式:br 执行无条件分支,br_if 执行条件分支,br_table 通过操作数索引到标签向量执行间接分支,该标签向量是指令的立即数,或者如果操作数越界,则索引到默认目标。 return 指令是针对最外层块的无条件分支的快捷方式,该块隐式地是当前函数的主体。执行分支会展开操作数栈,直到到达目标结构化控制指令被输入的高度。但是,分支本身可能会额外消耗操作数,它们会在展开后将操作数压回操作数栈。向前分支需要根据目标块类型的输出来提供操作数,即代表已终止块所产生的值。向后分支需要根据目标块类型的输入来提供操作数,即代表已重新启动块所消耗的值。
call 指令调用另一个 函数,从栈中消耗必要的参数,并返回调用的结果值。 call_indirect 指令通过操作数索引到一个 表格 间接调用函数,该表格由一个 表格索引 表示,并且必须具有类型 funcref。由于它可能包含不同类型的函数,因此被调用者会动态地与指令第二个立即数所索引的 函数类型 进行检查,如果它们不匹配,则调用会被中止并产生一个 陷阱。
2.4.9. 表达式
函数 主体、全局变量 的初始化值、元素 段的元素和偏移量以及 数据 段的偏移量都以表达式给出,表达式是 指令 的序列,以一个 end 标记终止。
在某些情况下,验证限制表达式为常量,这限制了允许指令集。
2.5. 模块
WebAssembly 程序被组织成模块,它们是部署、加载和编译的单元。模块收集类型、函数、表、内存和全局变量的定义。此外,它可以声明导入和导出,并以数据和元素段的形式提供初始化,或一个开始函数。
每个向量(以及整个模块)都可能是空的。
2.5.1. 索引
定义使用从零开始的索引进行引用。每类定义都有自己的索引空间,由以下类别区分。
函数、表格、内存和全局变量的索引空间包括同一模块中声明的相应导入。这些导入的索引位于同一索引空间中其他定义的索引之前。
元素索引引用元素段,数据索引引用数据段。
局部变量的索引空间仅在函数内部可访问,并且包括该函数的参数,参数位于局部变量之前。
标签索引引用指令序列内的结构化控制指令。
2.5.1.1. 约定
-
元变量 l 指代标签索引。
-
元变量 x,y 指代任何其他索引空间中的索引。
-
符号 idx(A) 表示在 idx 索引空间中自由出现的索引集。有时该集合被重新解释为其元素的向量。
注意
例如,如果 instr∗ 是 (data.drop x)(memory.init y), 那么 dataidx(instr∗)={x,y}, 或等效地,向量 x y.
2.5.2. 类型
模块的 types 组件定义了一个函数类型的向量。
模块中使用的所有函数类型都必须在此组件中定义。它们由类型索引引用。
注意
WebAssembly 的未来版本可能会添加其他形式的类型定义。
2.5.3. 函数
模块的 funcs 组件定义了一个具有以下结构的函数向量
函数的 type 通过引用模块中定义的 类型 来声明其签名。 函数的参数通过函数体中以 0 为基的 局部索引 来引用;它们是可变的。
The locals 声明一个可变局部变量及其类型的向量。 这些变量通过函数体中的 局部索引 来引用。 第一个局部的索引是未引用参数的最小索引。
The body 是一个 指令 序列,该序列在终止时必须生成与函数类型的 结果类型 匹配的堆栈。
Functions are referenced through function indices, starting with the smallest index not referencing a function import.
2.5.4. 表
模块的 tables 组件定义了一个由其 表类型 描述的表向量。
表是特定 引用类型 的不透明值的向量。 表类型中的 min 大小指定了该表的初始大小,而其 max(如果存在)限制了其以后可以增长的尺寸。
Tables can be initialized through element segments.
Tables are referenced through table indices, starting with the smallest index not referencing a table import. Most constructs implicitly reference table index 0.
2.5.5. 内存
模块的 mems 组件定义了一个由其 内存类型 描述的线性内存(或简称内存)向量。
内存是原始未解释字节的向量。 内存类型中的 min 大小指定了该内存的初始大小,而其 max(如果存在)限制了其以后可以增长的尺寸。 两者都以 页面大小 为单位。
Memories can be initialized through data segments.
Memories are referenced through memory indices, starting with the smallest index not referencing a memory import. Most constructs implicitly reference memory index 0.
注意
在 WebAssembly 的当前版本中,单个模块中最多可以定义或导入一个内存,并且所有结构都隐式地引用了这个内存 0。 此限制可能会在将来的版本中解除。
2.5.6. 全局变量
模块的 globals 组件定义了一个全局变量(或简称全局变量)向量。
每个全局变量存储给定全局类型的单个值。其type还指定全局变量是不可变还是可变的。此外,每个全局变量都使用init值初始化,该值由常量初始化器表达式给出。
2.5.7. 元素段
表的初始内容未初始化。元素段可用于从静态向量元素中初始化表的子范围。
模块的elems组件定义元素段向量。每个元素段定义一个引用类型以及相应的常量元素表达式列表。
元素段具有一个模式,用于将它们标识为被动、主动或声明式。被动元素段的元素可以使用table.init指令复制到表中。主动元素段在实例化期间将元素复制到表中,如表索引和定义表中偏移量的常量表达式指定。声明式元素段在运行时不可用,但仅用于向前声明在代码中使用ref.func等指令形成的引用。
元素段通过元素索引引用。
2.5.8. 数据段
内存的初始内容为零字节。数据段可用于从静态向量字节中初始化内存范围。
模块的datas组件定义数据段向量。
与元素段类似,数据段具有一个模式,用于将它们标识为被动或主动。被动数据段的内容可以使用memory.init指令复制到内存中。主动数据段在实例化期间将内容复制到内存中,如内存索引和定义内存中偏移量的常量表达式指定。
数据段通过 数据索引 引用。
注意
在当前版本的 WebAssembly 中,模块中最多允许一个内存。因此,唯一有效的 memidx 是 0。
2.5.9. 开始函数
模块的 start 组件声明一个 开始函数 的 函数索引,该函数在模块被 实例化 时自动调用,在 表格 和 内存 初始化之后。
注意
开始函数用于初始化模块的状态。在此初始化完成之前,模块及其导出无法从外部访问。
2.5.10. 导出
模块的 exports 组件定义了一组 导出,这些导出在模块被 实例化 后对主机环境可用。
每个导出都由一个唯一的 名称 标记。可导出定义是 函数、表格、内存 和 全局变量,它们通过相应的描述符引用。
2.5.10.1. 约定
以下辅助符号定义了导出序列,以按顺序保留的方式筛选出特定类型的索引
2.5.11. 导入
每个导入都由一个两级名称空间标记,包括一个module名称和一个name,用于该模块中的一个实体。可导入的定义是函数、表、内存和全局变量。每个导入都由一个描述符指定,该描述符具有一个相应的类型,实例化期间提供的定义需要与该类型匹配。
每个导入都在相应的索引空间中定义一个索引。在每个索引空间中,导入的索引都位于模块本身包含的任何定义的第一个索引之前。
3. 验证
3.1. 约定
验证检查 WebAssembly 模块是否格式正确。只有有效的模块才能 实例化。
有效性由 抽象语法 上的类型系统定义,该系统定义了 模块 及其内容。对于每个抽象语法,都有一个类型规则,指定适用于它的约束。所有规则都以两种等效形式给出
-
以散文形式描述直观的含义。
-
以正式符号形式描述规则,以数学形式表示。 [1]
注意
散文和正式规则是等效的,因此不需要理解正式符号就可以阅读本规范。形式主义提供了一种更简洁的描述,它使用的是编程语言语义中广泛使用的符号,并且很容易进行数学证明。
在这两种情况下,规则都是以声明式方式制定的。也就是说,它们只制定约束,并不定义算法。在 附录 中提供了根据本规范对指令序列进行类型检查的健全且完整的算法的框架。
3.1.1. 上下文
单个定义的有效性是相对于上下文指定的,上下文收集了有关周围 模块 和作用域内的定义的相关信息
-
类型:当前模块中定义的类型列表。
-
函数:当前模块中声明的函数列表,用它们的函数类型表示。
-
表:当前模块中声明的表列表,用它们的表类型表示。
-
内存:当前模块中声明的内存列表,用它们的内存类型表示。
-
全局变量:当前模块中声明的全局变量列表,用它们的全局变量类型表示。
-
元素段:当前模块中声明的元素段列表,用它们的元素类型表示。
-
数据段:当前模块中声明的数据段列表,每个数据段都用 ok 条目表示。
-
局部变量:当前函数(包括参数)中声明的局部变量列表,用它们的值类型表示。
-
标签:从当前位置可以访问的标签堆栈,用它们的返回值类型表示。
-
返回值:当前函数的返回值类型,表示为可选的返回值类型,当不允许返回值时(如在独立表达式中)不存在。
-
引用:模块中函数外部出现的 函数索引 列表,因此可以在函数内部使用它们来形成引用。
换句话说,上下文包含一系列适合的 类型,用于每个 索引空间,描述该空间中每个定义的条目。局部变量、标签和返回值类型仅用于验证 指令 在 函数体 中,在其他地方为空。标签堆栈是上下文唯一在验证指令序列时发生变化的部分。
更具体地说,上下文被定义为 记录 C,其抽象语法为
除了以 C.field 形式编写的字段访问之外,以下符号用于操作上下文。
-
当拼写出上下文时,空字段会被省略。
-
C,fieldA∗ 表示与 C 相同的上下文,但元素 A∗ 被预先添加到其 field 组件序列中。
3.1.2. 散文符号
验证由针对 抽象语法 的每个相关部分的程式化规则指定。这些规则不仅陈述了定义何时短语有效的约束条件,还将其归类为一种类型。在陈述这些规则时,采用以下约定。
-
如果且仅当某个词组 A 满足了相应规则所表达的所有约束,那么该词组就被称为“在类型 T 下有效”。 T 的形式取决于 A 是什么。
-
这些规则隐含地假设了给定的 上下文 C。
-
在某些地方,该上下文被局部扩展为上下文 C′,其中包含了额外的条目。 “在上下文 C′ 下,… 语句 …” 这种表述用于表达以下语句必须在扩展上下文所蕴含的假设下适用。
3.1.3. 形式符号
注意
本节简要介绍了用于正式指定类型规则的符号。 对于感兴趣的读者,可以在相应的教科书中找到更全面的介绍。 [2]
一个词组 A 具有相应的类型 T 的命题写成 A:T。 然而,一般来说,类型取决于上下文 C。 为了明确表达这一点,完整形式是 判断 C⊢A:T,它表明 A:T 在 C 中编码的假设下成立。
形式类型规则采用了一种标准方法来指定类型系统,将其呈现为 推导规则。 每个规则都有以下一般形式
这种规则被解读为一个大的蕴涵:如果所有前提都成立,那么结论就成立。 有些规则没有前提;它们是结论无条件成立的 公理。 结论始终是一个判断 C⊢A:T,并且每个相关的抽象语法结构 A 都对应一个规则。
注意
该指令始终在类型 [i32 i32]→[i32] 下有效(表明它消耗两个 i32 值并生成一个),与任何辅助条件无关。
像 local.get 这样的指令可以这样类型化
这里,前提要求立即的 局部索引 x 存在于上下文中。指令会产生一个与其类型 t 相对应的值(并且不会消耗任何值)。如果 C.locals[x] 不存在,则前提不成立,指令类型错误。
最后,一个 结构化 指令需要一个递归规则,其中前提本身就是一个类型判断。
一个 block 指令只有在它主体中的指令序列有效时才有效。此外,结果类型必须与块的注释 blocktype 匹配。如果是这样,则 block 指令具有与主体相同的类型。在主体内部,有一个额外的对应结果类型的标签可用,这可以通过将上下文 C 扩展到前提中包含额外的标签信息来表达。
语义来自以下文章:Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. Bringing the Web up to Speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.
例如:Benjamin Pierce. Types and Programming Languages. The MIT Press 2002
3.2. 类型
大多数 类型 都是普遍有效的。但是,对 限制 的限制适用,这些限制必须在验证期间进行检查。此外, 块类型 被转换为普通 函数类型 以便于处理。
3.2.1. 限制
限制 必须具有有意义的边界,这些边界必须在给定范围内。
3.2.1.1. {min n,max m?}
-
n 的值不能大于 k.
-
如果最大值 m? 非空,则
-
它的值不能大于 k.
-
它的值不能小于 n.
-
-
那么这个限制在 k 范围内是有效的。
3.2.2. 块类型
块类型 可以用两种形式表示,这两种形式都将被以下规则转换为普通的 函数类型。
3.2.2.1. typeidx
3.2.2.2. [valtype?]
3.2.3. 函数类型
函数类型 始终有效。
3.2.3.1. [t1n]→[t2m]
-
函数类型是有效的。
3.2.4. 表类型
3.2.4.1. limits reftype
3.2.5. 内存类型
3.2.5.1. limits
3.2.6. 全局类型
3.2.6.1. mut valtype
-
全局类型有效。
3.2.7. 外部类型
3.2.7.1. func functype
3.2.7.2. table tabletype
3.2.7.3. mem memtype
3.2.7.4. global globaltype
-
The global type globaltype must be valid.
-
然后外部类型有效。
3.2.8. 导入子类型
当 实例化 模块时,外部值 必须提供,其 类型 与每个导入所分类的相应 外部类型 相匹配。 在某些情况下,这允许使用简单的子类型形式(正式写为“≤”),如这里所定义。
3.2.8.1. 限制
限制 {min n1,max m1?} 匹配限制 {min n2,max m2?} 当且仅当
-
n1 大于或等于 n2.
-
要么
-
m2? 为空。
-
-
或者
-
两者 m1? 和 m2? 均不为空。
-
m1 小于或等于 m2.
-
3.2.8.2. 函数
3.2.8.3. 表
一个外部类型 table (limits1 reftype1) 与 table (limits2 reftype2) 匹配,当且仅当
3.2.8.4. 内存
3.2.8.5. 全局变量
一个 外部类型 global globaltype1 与 global globaltype2 相匹配当且仅当
-
globaltype1 和 globaltype2 相同。
3.3. 指令
指令 通过堆栈类型 [t1∗]→[t2∗] 进行分类,这些分类描述了指令如何操作 操作数堆栈.
这些类型描述了指令弹出所需的输入栈,其中包含操作数类型 t1∗,以及提供的输出栈,其中包含类型为 t2∗ 的结果值,它会将这些值压回栈中。栈类型类似于 函数类型,但它们允许将单个操作数分类为 ⊥(底部),表示该类型不受约束。作为辅助概念,操作数类型 t1 与另一个操作数类型 t2 匹配,如果 t1 是 ⊥ 或等于 t2。这以逐点方式扩展到栈类型。
输入扩展到 指令序列 instr∗. 这样的序列具有 栈类型 [t1∗]→[t2∗],如果执行指令的累积效果是从操作数栈中消耗类型为 t1∗ 的值,并将类型为 t2∗ 的新值压入栈。
对于某些指令,类型规则并不能完全约束类型,因此允许多种类型。这些指令被称为多态。可以区分两种程度的多态性
在这两种情况下,只要满足程序周围部分施加的约束,就可以任意选择不受约束的类型或类型序列。
注意
例如,select 指令在类型 [t t i32]→[t] 下有效,对于任何可能的 数字类型 t。因此,这两个指令序列
和
是有效的,其中 t 在 select 的类型中分别实例化为 i32 或 f64.
指令 unreachable 在任何可能的 操作数类型 序列 t1∗ 和 t2∗ 下都是有效的,类型为 [t1∗]→[t2∗]。因此,
假设指令 unreachable 的类型为 []→[i32 i32] 是有效的。相反,
是无效的,因为没有可以为指令 unreachable 选择的类型可以使序列类型正确。
在附录中描述了一种类型检查 算法,它可以有效地实现这里给出的规则所规定的指令序列验证。
3.3.1. 数值指令
3.3.1.1. t.const c
-
该指令的类型为 []→[t] 是有效的。
3.3.1.2. t.unop
-
该指令的类型为 [t]→[t] 是有效的。
3.3.1.3. t.binop
-
该指令的类型为 [t t]→[t] 是有效的。
3.3.1.4. t.testop
3.3.1.5. t.relop
3.3.1.6. t2.cvtop_t1_sx?
-
该指令在类型 [t1]→[t2]下有效。
3.3.2. 引用指令
3.3.2.1. ref.null t
-
该指令的类型为 []→[t] 是有效的。
注意
在未来的 WebAssembly 版本中,可能存在不允许空引用的引用类型。
3.3.2.2. ref.is_null
3.3.2.3. ref.func x
3.3.3. 向量指令
向量指令可以带有前缀来描述操作数的 形状。打包数值类型,i8 和 i16, 不是 值类型。辅助函数将这种打包类型形状映射到值类型
以下辅助函数表示向量形状的通道数,即其 *维度*
3.3.3.1. v128.const c
3.3.3.2. v128.vvunop
3.3.3.3. v128.vvbinop
3.3.3.4. v128.vvternop
3.3.3.5. v128.vvtestop
3.3.3.6. i8x16.swizzle
3.3.3.7. i8x16.shuffle laneidx16
3.3.3.8. shape.splat
3.3.3.9. shape.extract_lane_sx? laneidx
3.3.3.10. shape.replace_lane laneidx
3.3.3.11. shape.vunop
3.3.3.12. shape.vbinop
3.3.3.13. shape.vrelop
3.3.3.14. ishape.vishiftop
3.3.3.15. shape.vtestop
3.3.3.16. shape.vcvtop_half?_shape_sx?_zero?
3.3.3.17. ishape1.narrow_ishape2_sx
3.3.3.18. ishape.bitmask
3.3.3.19. ishape1.dot_ishape2_s
3.3.3.20. ishape1.extmul_half_ishape2_sx
3.3.3.21. ishape1.extadd_pairwise_ishape2_sx
3.3.4. 参数指令
3.3.4.1. drop
3.3.4.2. select (t∗)?
-
如果 t∗ 存在,那么
-
否则
注意
在 WebAssembly 的未来版本中,select 可能允许每个选择有多个值。
3.3.5. 变量指令
3.3.5.1. local.get x
3.3.5.2. local.set x
3.3.5.3. local.tee x
3.3.5.4. global.get x
-
全局变量 C.globals[x] 必须在上下文环境中定义。
-
令 mut t 为全局类型 global type C.globals[x].
-
那么该指令在类型为 []→[t] 时有效。
3.3.5.5. global.set x
-
全局变量 C.globals[x] 必须在上下文环境中定义。
-
令 mut t 为全局类型 global type C.globals[x].
-
那么该指令在类型为 [t]→[] 时有效。
3.3.6. 表格指令
3.3.6.1. table.get x
3.3.6.2. table.set x
3.3.6.3. table.size x
3.3.6.4. table.grow x
3.3.6.5. table.fill x
3.3.6.6. table.copy x y
3.3.6.7. table.init x y
3.3.6.8. elem.drop x
3.3.7. 内存指令
3.3.7.1. t.load memarg
3.3.7.2. t.loadN_sx memarg
3.3.7.3. t.store memarg
3.3.7.4. t.storeN memarg
3.3.7.5. v128.loadNxM_sx memarg
3.3.7.6. v128.loadN_splat memarg
3.3.7.7. v128.loadN_zero memarg
3.3.7.8. v128.loadN_lane memarg laneidx
3.3.7.9. v128.storeN_lane memarg laneidx
3.3.7.10. memory.size
3.3.7.11. memory.grow
3.3.7.12. memory.fill
3.3.7.13. memory.copy
3.3.7.14. memory.init x
3.3.7.15. data.drop x
3.3.8. 控制指令
3.3.8.1. nop
-
该指令类型有效 []→[].
3.3.8.2. unreachable
注意
unreachable 指令是 栈多态的。
3.3.8.3. block blocktype instr∗ end
-
那么复合指令是有效的,类型为 [t1∗]→[t2∗].
注意
符号 C,labels[t∗] 将新的标签类型插入到索引为 0 的位置,并向后移动所有其他标签类型。
3.3.8.4. loop blocktype instr∗ end
3.3.8.5. if blocktype instr1∗ else instr2∗ end
注意
符号 C,labels[t∗] 将新的标签类型插入到索引为 0 的位置,并向后移动所有其他标签类型。
3.3.8.6. br l
3.3.8.7. br_if l
3.3.8.8. br_table l∗ lN
3.3.8.9. return
3.3.8.10. call x
3.3.8.11. call_indirect x y
3.3.9. 指令序列
指令序列的类型递归定义。
3.3.9.1. 空指令序列: ϵ
3.3.9.2. 非空指令序列: instr∗ instrN
3.3.10. 表达式
表达式 expr 通过 结果类型 进行分类,形式为 [t∗].
3.3.10.1. instr∗ end
3.3.10.2. 常量表达式
-
常量指令 instr 必须是
注意
目前,出现在 globals、element 或 data 段的常量表达式受到进一步约束,因为其中包含的 global.get 指令只能引用*导入的*全局变量。这在 模块验证规则 中通过相应地约束上下文 C 来强制执行。
常量表达式的定义可能会在 WebAssembly 的未来版本中扩展。
3.4. 模块
模块 在它们包含的所有组件都有效时才有效。此外,大多数定义本身都用合适的类型进行分类。
3.4.1. 函数
函数 func 通过形式为 [t1∗]→[t2∗] 的 函数类型 进行分类。
3.4.1.1. {type x,locals t∗,body expr}
3.4.2. 表
3.4.2.1. {type tabletype}
-
The table type tabletype 必须是 valid 的。
-
然后表格定义在类型为 tabletype 时是有效的。
3.4.3. 内存
3.4.3.1. {type memtype}
3.4.4. Globals
Globals global are classified by global types of the form mut t.
3.4.4.1. {type mut t,init expr}
-
The global type mut t must be valid.
-
The expression expr must be valid with result type [t].
-
Then the global definition is valid with type mut t.
3.4.5. Element Segments
Element segments elem are classified by the reference type of their elements.
3.4.5.1. {type t,init e∗,mode elemmode}
3.4.5.2. passive
-
元素模式对于任何 引用类型 都是有效的。
3.4.5.3. active {table x,offset expr}
3.4.5.4. declarative
-
元素模式对于任何 引用类型 都是有效的。
3.4.6. 数据段
数据段 data 不按任何类型分类,只检查其是否格式正确。
3.4.6.1. {init b∗,mode datamode}
-
数据模式 datamode 必须有效。
-
然后数据段就有效。
3.4.6.2. passive
-
数据模式有效。
3.4.6.3. active {memory x,offset expr}
3.4.7. 起始函数
起始函数声明 start 不按任何类型分类。
3.4.7.1. {func x}
3.4.8. 导出
导出 export 和导出描述 exportdesc 按其 外部类型 进行分类。
3.4.8.1. {name name,desc exportdesc}
-
导出描述 exportdesc 必须与 外部类型 externtype 匹配。
-
然后,导出与 外部类型 externtype 匹配。
3.4.8.2. func x
3.4.8.3. table x
3.4.8.4. mem x
3.4.8.5. global x
3.4.9. 导入
导入 import 和导入描述 importdesc 由 外部类型 分类。
3.4.9.1. {module name1,name name2,desc importdesc}
-
导入描述 importdesc 必须是有效的,类型为 externtype.
-
那么,该导入就是有效的,类型为 externtype.
3.4.9.2. func x
3.4.9.3. table tabletype
3.4.9.4. mem memtype
3.4.9.5. global globaltype
-
全局类型 globaltype 必须是 有效的。
-
然后导入描述的类型为 global globaltype 的有效描述。
3.4.10. 模块
模块完全是*封闭*的,也就是说,其组件只能引用模块本身中出现的定义。因此,不需要任何初始 上下文。相反,模块内容验证的上下文 C 由模块中的定义构建。
-
令 module 为要验证的模块。
-
令 C 为一个 上下文,其中
-
C.funcs 是 funcs(it∗) 与 ft∗ 的连接,其中导入的 外部类型 为 it∗,内部 函数类型 为 ft∗,如下所示:
-
C.tables 是 tables(it∗) 与 tt∗ 的连接,其中导入的 外部类型 为 it∗,内部 表格类型 为 tt∗,如下所示:
-
C.mems 是 mems(it∗) 与 mt∗ 的连接,其中导入的 外部类型 为 it∗,内部 内存类型 为 mt∗,如下所示:
-
C.globals 是 globals(it∗) 与 gt∗ 的连接,其中导入的 外部类型 为 it∗,内部 全局类型 为 gt∗,如下所示:
-
C.elems 是 rt∗,如下所示:
-
C.locals 是空的。
-
C.labels 是空的。
-
C.return 为空。
-
C.refs 是集合 funcidx(modulewithfuncs=ϵwithstart=ϵ),即模块中出现的 函数索引 集合,但其 函数 或 起始函数 除外。
-
在上下文 C′ 下
-
在上下文 C
-
的长度 C.mems 必须不超过 1.
-
令 ft∗ 为内部 函数类型 fti 的级联,按索引顺序。
-
令 tt∗ 为内部 表格类型 tti 的级联,按索引顺序。
-
令 mt∗ 为内部 内存类型 mti 的级联,按索引顺序。
-
令 gt∗ 为内部 全局类型 gti 的级联,按索引顺序。
-
令 rt∗ 为 引用类型 rti 的级联,按索引顺序。
-
令 it∗ 为 外部类型 iti 在导入中的级联,按索引顺序。
-
令 et∗ 为 外部类型 eti 在导出中的级联,按索引顺序。
注意
模块中的大多数定义——特别是函数——是相互递归的。因此,此规则中 上下文 C 的定义是递归的:它依赖于模块中包含的函数、表格、内存和全局定义的验证结果,而这些验证结果本身又依赖于 C。然而,这种递归仅仅是一种规范手段。构建 C 所需的所有类型都可以很容易地从模块上的一次简单的预处理中确定,该预处理不会执行任何实际的验证。
但是,全局变量不是递归的,并且在它们被局部定义时,不能在 常量表达式 中访问。定义有限上下文 C′ 用于验证某些定义的效果是,它们只能访问函数和导入的全局变量,而不能访问其他任何内容。
注意
WebAssembly 的未来版本可能会取消对内存数量的限制。
4. 执行
4.1. 约定
当 实例化 模块或 调用 结果模块 实例 上的 导出 函数时,WebAssembly 代码就会被执行。
执行行为是在模拟程序状态的抽象机的术语中定义的。它包含一个堆栈,用于记录操作数的值和控制结构,以及一个包含全局状态的抽象存储。
对于每条指令,都有一个规则指定其执行对程序状态的影响。此外,还有一些规则描述了模块的实例化。与 验证 一样,所有规则都以两种等效形式给出
-
以散文形式描述执行,以直观的方式。
-
以形式化符号形式描述规则,以数学形式。 [1]
注意
与验证一样,散文和形式化规则是等效的,因此不需要理解形式化符号来阅读本规范。形式化符号以编程语言语义中广泛使用的符号提供了更简洁的描述,并且易于进行数学证明。
4.1.1. 散文符号
4.1.2. 形式符号
注意
本节简要解释了正式指定执行的符号。对于感兴趣的读者,可以在相应的教科书中找到更深入的介绍。 [2]
正式执行规则使用一种标准方法来指定操作语义,将它们呈现为规约规则。每个规则都有以下一般形式
配置是对程序状态的句法描述。每个规则指定执行的一步。只要最多有一个规约规则适用于给定的配置,规约(从而执行)就是确定性的。WebAssembly 只有极少数例外,这些例外在本规范中明确指出。
对于 WebAssembly,配置通常是一个元组(S;F;instr∗),它由当前存储 S、当前函数的调用帧 F 以及要执行的指令 序列组成。(更精确的定义稍后给出。)
为了避免不必要的混乱,存储 S 和帧 F 从不涉及它们的规约规则中省略。
没有堆栈 的独立表示。相反,它很方便地表示为配置的指令序列的一部分。特别是,值 被定义为与const 指令一致,并且const 指令的序列可以解释为一个向右增长的操作数“堆栈”。
规约的顺序由适当的求值上下文 的定义决定。
当没有更多规约规则适用时,规约终止。WebAssembly 类型系统 的健壮性 保证这仅在原始指令序列已简化为const 指令序列(可以解释为结果操作数堆栈的值)或发生陷阱 时才会发生。
注意
例如,以下指令序列:
在三个步骤后终止
其中 x4=−x2 且 x5=−x2+x3 以及 x6=x1⋅(−x2+x3).
语义来自以下文章:Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. Bringing the Web up to Speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.
例如:Benjamin Pierce. Types and Programming Languages. The MIT Press 2002
4.2. 运行时结构
存储器、栈以及其他构成 WebAssembly 抽象机的运行时结构,例如值或模块实例,在额外的辅助语法中被精确定义。
4.2.1. 值
WebAssembly 计算操作四种基本数值类型的值,即整数和浮点数(分别为 32 位和 64 位),或向量(128 位),或引用类型。
在语义的大部分地方,不同类型的值可能出现。为了避免歧义,因此使用抽象语法表示值,该语法明确了值的类型。方便起见,可以使用与const 指令和ref.null 相同的符号来表示它们。
非空引用由附加的管理指令表示。它们要么是函数引用,指向特定的函数地址,要么是外部引用,指向外部地址的未解释形式,可由嵌入器定义以表示其自己的对象。
注意
WebAssembly 的未来版本可能会添加其他形式的引用。
每个 值类型 都有一个关联的默认值;对于 数值类型,它分别是 0;对于 向量类型,它是 0;对于 引用类型,它是 null。
4.2.1.1. 约定
-
元变量 r 在上下文中清晰的情况下,表示引用值。
4.2.2. 结果
4.2.3. 存储
存储表示 WebAssembly 程序可以操作的所有全局状态。它包含所有函数、表格、内存和全局变量、元素段以及数据段的运行时表示,这些实例在抽象机器的生命周期中已被分配。 [1]
语义的一个不变式是,没有任何元素或数据实例从除拥有模块实例以外的任何地方被寻址。
从语法上讲,存储被定义为一个记录,列出每种类型的现有实例。
在实践中,实现可能会应用诸如垃圾收集之类的技术来从存储中移除不再被引用的对象。但是,这些技术在语义上是不可观察的,因此不在本规范的范围内。
4.2.3.1. 约定
-
元变量S在上下文中明确时,表示存储。
4.2.4. 地址
函数实例、表格实例、内存实例和全局变量实例、元素实例以及数据实例在存储中用抽象的地址引用。这些地址只是对各自存储组件的索引。此外,嵌入器可以提供一组未解释的主机地址。
一个 嵌入器 可以为与它们的地址相对应的 导出 的存储对象分配标识,即使此标识在 WebAssembly 代码本身内部不可观察(例如,对于 函数实例 或不可变的 全局变量)。
4.2.5. 模块实例
模块实例是 模块 的运行时表示。它是通过 实例化 模块创建的,它收集了由模块导入、定义或导出的所有实体的运行时表示。
每个组件引用其原始模块中相应声明(无论是导入还是定义)的运行时实例,按照其静态索引的顺序。 函数实例、表实例、内存实例和全局实例通过它们各自在存储区中的地址进行间接引用。
4.2.6. 函数实例
函数实例是函数的运行时表示。它实际上是对其原始函数的运行时模块实例(来自其原始模块)的闭包。模块实例用于在执行函数期间解析对其他定义的引用。
宿主函数是在 WebAssembly 外部表达的函数,但作为导入传递给模块。宿主函数的定义和行为超出了本规范的范围。为了本规范的目的,假设当调用时,宿主函数的行为是不确定的,但在某些约束内,以确保运行时的完整性。
4.2.7. 表实例
表实例是表的运行时表示。它记录了它的类型,并包含一个引用值向量。
表元素可以通过表指令、活动元素段的执行或由嵌入器提供的外部手段进行修改。
语义的不变性要求所有表元素的类型都等于tabletype的元素类型。它也是一个不变性,即元素向量的长度永远不会超过tabletype的最大大小(如果存在)。
4.2.8. 内存实例
内存实例是线性内存的运行时表示。它记录了它的类型,并包含一个字节向量。
向量长度始终是 WebAssembly *页面大小* 的倍数,页面大小定义为常数 65536,简写为 64Ki.
字节可以通过 内存指令、活动 数据段 的执行或由 嵌入器 提供的外部手段进行修改。
语义的不变性在于,字节向量长度除以页面大小,永远不会超过 memtype 的最大大小(如果存在)。
4.2.9. 全局实例
全局实例 是 全局 变量的运行时表示。它记录了其 类型 并保存一个单独的 值。
可变全局变量的值可以通过 变量指令 或由 嵌入器 提供的外部手段进行修改。
语义的不变性在于,该值具有与 globaltype 的 值类型 相同的类型。
4.2.10. 元素实例
4.2.11. 数据实例
4.2.12. 导出实例
导出实例 是 导出 的运行时表示。它定义了导出的 名称 和关联的 外部值。
4.2.13. 外部值
外部值 是可以导入或导出的实体的运行时表示。它是一个 地址,表示共享 存储 中的 函数实例、表格实例、内存实例 或 全局实例。
4.2.13.1. 约定
以下定义了用于外部值序列的辅助符号。它以保留顺序的方式过滤掉特定类型的条目
4.2.14. 堆栈
除了存储之外,大多数指令与隐式堆栈进行交互。堆栈包含三种类型的条目
在程序执行期间,这些条目可以以任何顺序出现在堆栈中。堆栈条目由以下抽象语法描述。
注意
可以使用单独的操作数、控制结构和调用堆栈来对 WebAssembly 语义进行建模。但是,由于堆栈是相互依赖的,因此需要有关关联堆栈高度的额外簿记。为了便于本规范的目的,交错表示更简单。
4.2.14.1. 值
值由自身表示。
4.2.14.2. 标签
标签带有参数元数n,以及它们关联的分支目标,在语法上表示为指令序列
直观地说,instr∗是分支被执行时要执行的延续,它将替换原始控制结构。
4.2.14.3. 激活帧
激活帧承载着相应函数的返回值元数n,保存其局部变量(包括参数)的值,顺序对应于它们的静态局部变量索引,以及对该函数自身模块实例的引用。
局部变量的值由各自的变量指令修改。
4.2.14.4. 约定
4.2.15. 管理指令
注意
本节仅与正式符号相关。
为了表达陷阱、调用和控制指令的规约,指令的语法扩展到包含以下管理指令
指令trap表示发生陷阱。陷阱会通过嵌套的指令序列冒泡,最终将整个程序规约为单个trap指令,表示程序突然终止。
指令ref表示函数引用值。类似地,ref.extern表示外部引用.
指令invoke表示即将调用一个函数实例,由其地址标识。它统一了不同形式的调用处理。
在 label 和 frame 指令中,标签 和 帧 “在堆栈上” 建模。此外,管理语法维护了原始 结构化控制指令 或 函数体 及其 指令序列 的嵌套结构,并使用 end 标记。这样,当内部指令序列是外部序列的一部分时,便可以知道内部指令序列的结束位置。
注意
这将块替换为一个标签指令,可以解释为将标签“压入”堆栈。当遇到 end 时,即内部指令序列已规约为空序列 - 或者更确切地说,是一系列 n 个 const 指令,代表生成的数值 - 然后 label 指令将根据其自身的 规约规则 被消除。
这可以解释为从堆栈中移除标签,只保留本地累积的操作数。
4.2.15.1. 块上下文
为了指定 分支 的规约,定义了以下 块上下文 语法,以包围 空洞 [_] 的标签数量 k 进行索引,该空洞标记着计算的下一步将要进行的位置。
4.2.15.2. 配置
配置由当前的 存储 和正在执行的 线程 组成。
线程是在 指令 上的计算,它相对于当前 帧 的状态进行操作,该帧引用了计算运行的 模块实例,即当前函数源自的位置。
注意
当前版本的 WebAssembly 是单线程的,但在未来可能会支持多线程的配置。
4.2.15.3. 评估上下文
最后,评估上下文 的以下定义和相关的结构规则允许在指令序列和管理形式内部进行简化,以及陷阱的传播
4.3. 数值
数值基元以通用方式定义,通过按位宽索引的运算符 N 进行定义。
一些运算符是非确定性的,因为它们可以返回几种可能结果之一(例如不同的 NaN 值)。从技术上讲,每个运算符因此返回一组允许的值。为了方便起见,确定性结果表示为普通值,这些值被假定为与相应的单元素集一致。
一些运算符是偏函数的,因为它们在某些输入上没有定义。从技术上讲,对于这些输入,返回一个空的结果集。
在形式化表示中,每个运算符都由等式子句定义,这些子句按优先级降序应用。也就是说,第一个适用于给定参数的子句定义了结果。在某些情况下,类似的子句使用 ± 或 ∓ 符号组合成一个。当多个这样的占位符出现在单个子句中时,它们必须一致地解析:要么为所有占位符选择上符号,要么选择下符号。
数值运算符通过对输入序列逐元素应用运算符来提升到输入序列,返回结果序列。当有多个输入时,它们必须具有相同的长度。
约定
4.3.1. 表示
数字和数值向量具有作为比特序列的底层二进制表示。
这些函数中的每一个都是双射,因此它们是可逆的。
4.3.1.1. 整数
整数 被表示为二进制无符号数。
布尔运算符,如 ∧、∨ 或 ⊻,通过逐位应用于长度相等的比特序列来提升。
4.3.1.2. 浮点数
浮点值 在 [IEEE-754-2019] (第 3.4 节) 定义的相应二进制格式中表示。
4.3.1.3. 向量
类型为 vN 的数值向量具有与 iN 相同的底层表示。它们也可以解释为打包到 vN 中的数值序列,具有特定的 shape txM,前提是 N=∣t∣⋅M.
此函数是关于iN的双射,因此它是可逆的。
4.3.1.4. 存储
这些函数同样是可逆的双射。
4.3.2. 整数运算
4.3.2.1. 符号解释
整数运算符定义在iN值上。使用有符号解释的运算符使用以下定义来转换值,当值位于值范围的上半部分时(即其最高有效位为1),它采用二进制补码。
此函数是双射的,因此是可逆的。
4.3.2.2. 布尔解释
4.3.2.3. iaddN(i1,i2)
-
返回 i1 和 i2 模 2N 的结果。
4.3.2.4. isubN(i1,i2)
-
返回从 i1 中减去 i2 模 2N 的结果。
4.3.2.5. imulN(i1,i2)
-
返回 i1 和 i2 模 2N 的乘积的结果。
4.3.2.6. idiv_uN(i1,i2)
-
如果 i2 为 0, 则结果未定义。
-
否则,返回将 i1 除以 i2 的结果,向零取整。
注意
此运算符是 部分 的。
4.3.2.7. idiv_sN(i1,i2)
-
令 j1 为 i1 的 有符号解释。
-
令 j2 为 i2 的 有符号解释。
-
如果 j2 为 0, 则结果未定义。
-
否则,如果 j1 除以 j2 的结果为 2N−1, 则结果未定义。
-
否则,返回将 j1 除以 j2 的结果,向零取整。
注意
此运算符是 部分 的。除了被 0 除外,结果 (−2N−1)/(−1)=+2N−1 不能表示为 N 位带符号整数。
4.3.2.8. irem_uN(i1,i2)
-
如果 i2 为 0, 则结果未定义。
-
否则,返回将 i1 除以 i2 的余数。
4.3.2.9. irem_sN(i1,i2)
4.3.2.10. inotN(i)
-
返回 i 的按位取反。
4.3.2.11. iandN(i1,i2)
-
返回 i1 和 i2 的按位与。
4.3.2.12. iandnotN(i1,i2)
-
返回 i1 和 i2 按位取反后的按位与。
4.3.2.13. iorN(i1,i2)
-
返回 i1 和 i2 的按位或运算结果。
4.3.2.14. ixorN(i1,i2)
-
返回 i1 和 i2 的按位异或运算结果。
4.3.2.15. ishlN(i1,i2)
-
设 k 为 i2 模 N 的结果。
-
返回将 i1 左移 k 位的结果,模 2N.
4.3.2.16. ishr_uN(i1,i2)
-
设 k 为 i2 模 N 的结果。
-
返回将 i1 右移 k 位的结果,并用 0 位扩展。
4.3.2.17. ishr_sN(i1,i2)
-
设 k 为 i2 模 N 的结果。
-
返回将 i1 右移 k 位的结果,并使用原始值的最高有效位进行扩展。
4.3.2.18. irotlN(i1,i2)
-
设 k 为 i2 模 N 的结果。
-
返回将 i1 左移 k 位的结果。
4.3.2.19. irotrN(i1,i2)
-
设 k 为 i2 模 N 的结果。
-
返回将 i1 右移 k 位的结果。
4.3.2.20. iclzN(i)
-
返回 i 中前导零位的数量;如果 i 是 0,则所有位都算作前导零位。
4.3.2.21. ictzN(i)
-
返回 i 中尾随零位的数量;如果 i 是 0,则所有位都算作尾随零位。
4.3.2.22. ipopcntN(i)
-
返回 i 中非零位的数量。
4.3.2.23. ieqzN(i)
-
如果 i 为零,则返回 1,否则返回 0。
4.3.2.24. ieqN(i1,i2)
-
如果 i1 等于 i2,则返回 1;否则返回 0。
4.3.2.25. ineN(i1,i2)
-
如果 i1 不等于 i2,则返回 1;否则返回 0。
4.3.2.26. ilt_uN(i1,i2)
-
如果 i1 小于 i2,则返回 1;否则返回 0。
4.3.2.27. ilt_sN(i1,i2)
4.3.2.28. igt_uN(i1,i2)
-
如果 i1 大于 i2, 则返回 1,否则返回 0.
4.3.2.29. igt_sN(i1,i2)
4.3.2.30. ile_uN(i1,i2)
-
返回 1 如果 i1 小于或等于 i2, 0 否则。
4.3.2.31. ile_sN(i1,i2)
4.3.2.32. ige_uN(i1,i2)
-
如果 i1 大于或等于 i2,则返回 1;否则返回 0。
4.3.2.33. ige_sN(i1,i2)
4.3.2.34. iextendM_sN(i)
4.3.2.35. ibitselectN(i1,i2,i3)
-
令 j1 为 i1 和 i3 的按位与运算结果。
-
令 j3′ 为 i3 的按位取反运算结果。
-
令 j2 为 i2 和 j3′ 的按位与运算结果。
-
返回 j1 和 j2 的按位或运算的结果。
4.3.2.36. iabsN(i)
-
令 j 为 i 的 有符号解释。
-
如果 j 大于或等于 0,则返回 i。
-
否则返回 j 的负数,对 2N 取模。
4.3.2.37. inegN(i)
-
返回对 i 取反的结果,模 2N.
4.3.2.38. imin_uN(i1,i2)
-
如果 ilt_uN(i1,i2) 为 1,则返回 i1,否则返回 i2.
4.3.2.39. imin_sN(i1,i2)
-
返回 i1 如果 ilt_sN(i1,i2) 为 1, 否则返回 i2.
4.3.2.40. imax_uN(i1,i2)
-
返回 i1 如果 igt_uN(i1,i2) 为 1, 返回 i2 否则。
4.3.2.41. imax_sN(i1,i2)
-
如果 igt_sN(i1,i2) 为 1, 则返回 i1, 否则返回 i2.
4.3.2.42. iadd_sat_uN(i1,i2)
-
设 i 为 i1 和 i2 相加的结果。
-
返回 sat_uN(i).
4.3.2.43. iadd_sat_sN(i1,i2)
-
令 j1 为 i1 的有符号解释。
-
令 j2 为 i2 的有符号解释。
-
令 j 为 j1 和 j2 相加的结果。
-
返回 sat_sN(j).
4.3.2.44. isub_sat_uN(i1,i2)
-
令 i 为从 i1 中减去 i2 的结果。
-
返回 sat_uN(i).
4.3.2.45. isub_sat_sN(i1,i2)
-
令 j1 为 i1 的有符号解释。
-
令 j2 为 i2 的有符号解释。
-
令 j 为从 j1 中减去 j2 的结果。
-
返回 sat_sN(j).
4.3.2.46. iavgr_uN(i1,i2)
-
令 j 为 i1, i2, 和 1 相加的结果。
-
返回 j 除以 2 的结果,向零取整。
4.3.2.47. iq15mulrsat_sN(i1,i2)
4.3.3. 浮点运算
浮点运算遵循 [IEEE-754-2019] 标准,并具有以下限定条件
-
所有运算符使用舍入到最接近的偶数,除非另有说明。不支持非默认定向舍入属性。
-
遵循从操作数传播 NaN 负载的建议是允许的,但不是必需的。
-
所有运算符使用“不停”模式,并且浮点异常不会以其他方式被观察到。特别是,不支持备用浮点异常处理属性或状态标志上的运算符。安静的 NaN 和信号 NaN 之间没有可观察到的区别。
注意
WebAssembly 的未来版本可能会解除其中一些限制。
4.3.3.1. 舍入
舍入始终是舍入到最接近的偶数,与 [IEEE-754-2019](第 4.3.1 节)一致。
精确浮点数是指可以被精确表示为给定位宽 N 的 浮点数 的有理数。
给定浮点位宽 N 的限制数是指其大小为不能被精确表示为位宽为 N 的浮点数的 2 的最小幂的正数或负数(该大小为 2128 对于 N=32 和 21024 对于 N=64)。
候选数是指给定位宽 N 的精确浮点数或正数或负数限制数。
候选对是指候选数对 z1,z2,其中不存在位于两者之间的候选数。
实数 r 转换为位宽为 N 的浮点值如下
-
如果 r 等于 0,则返回 +0.
-
否则,如果 r 是一个精确的浮点数,则返回 r.
-
否则,如果 r 大于或等于正极限,则返回 +∞.
-
否则,如果 r 小于或等于负极限,则返回 −∞.
-
否则,如果 z1 和 z2 是一个候选对,使得 z1<r<z2,则
-
如果 ∣r−z1∣<∣r−z2∣,则设 z 为 z1.
-
否则,如果 ∣r−z1∣>∣r−z2∣,则设 z 为 z2.
-
否则,如果 ∣r−z1∣=∣r−z2∣ 且 z1 的 尾数 是偶数,则设 z 为 z1.
-
否则,设 z 为 z2.
-
-
如果 z 等于 0,则
-
如果 r<0,则返回 −0.
-
否则,返回 +0.
-
-
否则如果 z 是一个极限数,那么
-
如果 r<0,则返回 −∞.
-
否则,返回 +∞.
-
-
否则,返回 z.
其中
4.3.3.2. NaN 传播
当浮点运算符(除 fneg, fabs, 或 fcopysign 之外)的结果为 NaN 时,其符号是不确定的,而 有效载荷 则按以下方式计算
-
如果运算符的所有 NaN 输入的有效载荷都为 规范的(包括没有 NaN 输入的情况),则输出的有效载荷也为规范的。
-
否则,有效载荷将在所有 算术 NaN 中非确定性地选择;也就是说,其最高有效位为 1,而其他所有位则未指定。
此非确定性结果由以下辅助函数表示,该函数从一组输入生成一组允许的输出
4.3.3.3. faddN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 nansN{z1,z2} 中的一个元素。
-
否则,如果 z1 和 z2 都是符号相反的无穷大,则返回 nansN{} 中的一个元素。
-
否则,如果 z1 和 z2 都是符号相同的无穷大,则返回该无穷大。
-
否则,如果 z1 或 z2 是无穷大,则返回该无穷大。
-
否则,如果 z1 和 z2 都是符号相反的零,则返回正零。
-
否则,如果 z1 和 z2 都是符号相同的零,则返回该零。
-
否则,如果 z1 或 z2 是零,则返回另一个操作数。
-
否则,如果 z1 和 z2 是大小相同但符号相反的值,则返回正零。
-
否则,返回 z1 和 z2 相加的结果,舍入到最接近的可表示值。
4.3.3.4. fsubN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 nansN{z1,z2} 中的一个元素。
-
否则,如果 z1 和 z2 都是符号相同的无穷大,则返回 nansN{}.
-
否则,如果 z1 和 z2 都是符号相反的无穷大,则返回 z1.
-
否则,如果 z1 是无穷大,则返回该无穷大。
-
否则,如果 z2 是无穷大,则返回该无穷大的负数。
-
否则,如果 z1 和 z2 都是符号相同的零,则返回正零。
-
否则,如果 z1 和 z2 都是符号相反的零,则返回 z1.
-
否则,如果 z2 是零,则返回 z1.
-
否则,如果 z1 是零,则返回 z2 的负数。
-
否则,如果 z1 和 z2 相同,则返回正零。
-
否则,返回从 z1 中减去 z2 的结果,四舍五入 到最接近的可表示值。
4.3.3.5. fmulN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 nansN{z1,z2} 中的一个元素。
-
否则,如果 z1 和 z2 之一是零,另一个是无穷大,则返回 nansN{} 的一个元素。
-
否则,如果 z1 和 z2 都是符号相同的无穷大,则返回正无穷大。
-
否则,如果 z1 和 z2 都是符号相反的无穷大,则返回负无穷大。
-
否则,如果 z1 或 z2 是无穷大,而另一个是符号相同的数值,则返回正无穷大。
-
否则,如果 z1 或 z2 是无穷大,而另一个是符号相反的数值,则返回负无穷大。
-
否则,如果 z1 和 z2 都是符号相同的零,则返回正零。
-
否则,如果 z1 和 z2 都是符号相反的零,则返回负零。
-
否则,返回 z1 和 z2 相乘的结果,四舍五入 到最近的可表示的值。
4.3.3.6. fdivN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 nansN{z1,z2} 中的一个元素。
-
否则,如果 z1 和 z2 都是无穷大,则返回 nansN{} 中的一个元素。
-
否则,如果 z1 和 z2 都是零,则返回 nansN{z1,z2}.
-
否则,如果 z1 是无穷大,而 z2 是一个符号相同的数值,则返回正无穷大。
-
否则,如果 z1 是无穷大,而 z2 是一个符号相反的数值,则返回负无穷大。
-
否则,如果 z2 是无穷大,而 z1 是一个符号相同的数值,则返回正零。
-
否则,如果 z2 是无穷大,而 z1 是一个符号相反的数值,则返回负零。
-
否则,如果 z1 是零,而 z2 是一个符号相同的数值,则返回正零。
-
否则,如果 z1 是零,而 z2 是一个符号相反的数值,则返回负零。
-
如果 z2 为零且 z1 为一个带有等号的值,则返回正无穷大。
-
如果 z2 为零且 z1 为一个带有相反符号的值,则返回负无穷大。
-
否则返回 z1 除以 z2 的结果,四舍五入 到最接近的可表示值。
4.3.3.7. fminN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 nansN{z1,z2} 中的一个元素。
-
如果 z1 或 z2 为负无穷大,则返回负无穷大。
-
如果 z1 或 z2 为正无穷大,则返回另一个值。
-
如果 z1 和 z2 都是带有相反符号的零,则返回负零。
-
否则返回 z1 和 z2 中较小的值。
4.3.3.8. fmaxN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 nansN{z1,z2} 中的一个元素。
-
如果 z1 或 z2 为正无穷大,则返回正无穷大。
-
如果 z1 或 z2 是负无穷大,则返回另一个值。
-
如果 z1 和 z2 都是符号相反的零,则返回正零。
-
否则,返回 z1 和 z2 中较大的值。
4.3.3.9. fcopysignN(z1,z2)
-
如果 z1 和 z2 符号相同,则返回 z1.
-
否则,返回符号取反后的 z1.
4.3.3.10. fabsN(z)
-
如果 z 是 NaN,则返回符号为正的 z.
-
如果 z 是无穷大,则返回正无穷大。
-
如果 z 是零,则返回正零。
-
如果 z 是正值,则 z.
-
否则,返回取反后的 z.
4.3.3.11. fnegN(z)
-
如果 z 是 NaN,则返回符号取反后的 z。
-
否则,如果 z 是无穷大,则返回符号取反后的无穷大。
-
否则,如果 z 是零,则返回符号取反后的零。
-
否则,返回取反后的 z.
4.3.3.12. fsqrtN(z)
4.3.3.13. fceilN(z)
-
如果 z 是 NaN,则返回 nansN{z} 中的一个元素。
-
如果 z 是无穷大,则返回 z.
-
如果 z 是零,则返回 z.
-
如果 z 小于 0 但大于 −1, 则返回负零。
-
否则,返回不小于 z 的最小整数。
4.3.3.14. ffloorN(z)
-
如果 z 是 NaN,则返回 nansN{z} 中的一个元素。
-
如果 z 是无穷大,则返回 z.
-
如果 z 是零,则返回 z.
-
如果 z 大于 0 但小于 1,则返回正零。
-
否则返回不大于 z 的最大整数值。
4.3.3.15. ftruncN(z)
-
如果 z 是 NaN,则返回 nansN{z} 中的一个元素。
-
如果 z 是无穷大,则返回 z.
-
如果 z 是零,则返回 z.
-
如果 z 大于 0 但小于 1,则返回正零。
-
如果 z 小于 0 但大于 −1, 则返回负零。
-
否则返回与 z 符号相同的整数,且该整数的绝对值是小于或等于 z 绝对值的最大整数。
4.3.3.16. fnearestN(z)
-
如果 z 是 NaN,则返回 nansN{z} 中的一个元素。
-
如果 z 是无穷大,则返回 z.
-
如果 z 是零,则返回 z.
-
如果 z 大于 0 但小于或等于 0.5, 则返回正零。
-
如果 z 小于 0 但大于或等于 −0.5, 则返回负零。
-
否则返回最接近 z 的整数值;如果两个值一样接近,则返回偶数。
4.3.3.17. feqN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 0.
-
否则,如果 z1 和 z2 都是零,则返回 1.
-
否则,如果 z1 和 z2 值相同,则返回 1.
-
否则返回 0.
4.3.3.18. fneN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 1.
-
否则如果 z1 和 z2 都是零,则返回 0.
-
否则如果 z1 和 z2 值相同,则返回 0.
-
否则返回 1.
4.3.3.19. fltN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 0.
-
如果 z1 和 z2 值相同,则返回 0.
-
如果 z1 是正无穷大,则返回 0.
-
如果 z1 是负无穷大,则返回 1.
-
如果 z2 是正无穷大,则返回 1.
-
如果 z2 是负无穷大,则返回 0.
-
否则如果 z1 和 z2 都是零,则返回 0.
-
如果 z1 小于 z2, 则返回 1.
-
否则返回 0.
4.3.3.20. fgtN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 0.
-
如果 z1 和 z2 值相同,则返回 0.
-
否则,如果 z1 为正无穷大,则返回 1.
-
否则,如果 z1 为负无穷大,则返回 0.
-
否则,如果 z2 为正无穷大,则返回 0.
-
否则,如果 z2 为负无穷大,则返回 1.
-
否则如果 z1 和 z2 都是零,则返回 0.
-
否则,如果 z1 大于 z2, 则返回 1.
-
否则返回 0.
4.3.3.21. fleN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 0.
-
否则,如果 z1 和 z2 的值相同,则返回 1.
-
如果 z1 是正无穷大,则返回 0.
-
如果 z1 是负无穷大,则返回 1.
-
如果 z2 是正无穷大,则返回 1.
-
如果 z2 是负无穷大,则返回 0.
-
否则,如果 z1 和 z2 都是零,则返回 1.
-
否则,如果 z1 小于或等于 z2, 则返回 1.
-
否则返回 0.
4.3.3.22. fgeN(z1,z2)
-
如果 z1 或 z2 是 NaN,则返回 0.
-
否则,如果 z1 和 z2 的值相同,则返回 1.
-
否则,如果 z1 为正无穷大,则返回 1.
-
否则,如果 z1 为负无穷大,则返回 0.
-
否则,如果 z2 为正无穷大,则返回 0.
-
否则,如果 z2 为负无穷大,则返回 1.
-
否则,如果 z1 和 z2 都是零,则返回 1.
-
否则,如果 z1 小于或等于 z2, 则返回 1.
-
否则返回 0.
4.3.3.23. fpminN(z1,z2)
-
如果 z2 小于 z1 ,则返回 z2.
-
否则返回 z1.
4.3.3.24. fpmaxN(z1,z2)
-
如果 z1 小于 z2,则返回 z2.
-
否则返回 z1.
4.3.4. 转换
4.3.4.1. extenduM,N(i)
-
返回 i.
注意
在抽象语法中,无符号扩展只是重新解释相同的值。
4.3.4.2. extendsM,N(i)
-
令 j 为 带符号解释 的 i,大小为 M.
-
返回 j 相对于大小 N 的二进制补码。
4.3.4.3. wrapM,N(i)
-
返回 i 模 2N.
4.3.4.4. truncuM,N(z)
-
如果 z 是 NaN,则结果未定义。
-
否则,如果 z 是无穷大,则结果未定义。
-
否则,如果 z 是一个数字,并且 trunc(z) 是目标类型范围内的值,则返回该值。
-
否则,结果未定义。
注意
该运算符是 部分 的。它没有为 NaN、无穷大或结果超出范围的值定义。
4.3.4.5. truncsM,N(z)
-
如果 z 是 NaN,则结果未定义。
-
否则,如果 z 是无穷大,则结果未定义。
-
如果 z 是一个数字,并且 trunc(z) 是目标类型范围内的一个值,则返回该值。
-
否则,结果未定义。
注意
该运算符是 部分 的。它没有为 NaN、无穷大或结果超出范围的值定义。
4.3.4.6. trunc_sat_uM,N(z)
4.3.4.7. trunc_sat_sM,N(z)
4.3.4.8. promoteM,N(z)
4.3.4.9. demoteM,N(z)
4.3.4.10. convertuM,N(i)
-
返回 floatN(i).
4.3.4.11. convertsM,N(i)
4.3.4.12. reinterprett1,t2(c)
4.3.4.13. narrowsM,N(i)
4.3.4.14. narrowuM,N(i)
4.4. 指令
WebAssembly 计算是通过执行单个 指令 来完成的。
4.4.1. 数值指令
数值指令是根据通用 数值运算符 来定义的。数值指令与其底层运算符的映射由以下定义表示
对于转换运算符
当底层运算符为部分运算符时,当结果未定义时,相应的指令将陷入异常。当底层运算符为非确定性运算符时,因为它们可能返回多个可能的NaN 值,相应的指令也是非确定性的。
注意
例如,指令 i32.add 作用于操作数 i1,i2 的结果调用了 addi32(i1,i2),它根据上述定义映射到泛型 iadd32(i1,i2)。类似地,i64.trunc_f32_s 作用于 z 调用了 truncf32,i64s(z),它根据上述定义映射到泛型 truncs32,64(z).
4.4.1.1. t.const c
-
将值 t.const c 推入堆栈。
4.4.1.2. t.unop
4.4.1.3. t.binop
4.4.1.4. t.testop
4.4.1.5. t.relop
4.4.1.6. t2.cvtop_t1_sx?
4.4.2. 引用指令
4.4.2.1. ref.null t
-
将值 ref.null t 推入堆栈。
4.4.2.2. ref.is_null
4.4.2.3. ref.func x
4.4.3. 向量指令
按位操作的向量指令被视为相应宽度的整数运算。
大多数其他向量指令都是根据给定的 形状 按车道方式应用数值运算符来定义的。
注意
例如,指令 i32x4.add 应用于操作数 v1,v2 的结果调用了 addi32x4(v1,v2), 它映射到 lanesi32x4−1(addi32(i1,i2)∗), 其中 i1∗ 和 i2∗ 分别是调用 lanesi32x4(v1) 和 lanesi32x4(v2) 所产生的序列。
4.4.3.1. v128.const c
4.4.3.2. v128.vvunop
4.4.3.3. v128.vvbinop
4.4.3.4. v128.vvternop
4.4.3.5. v128.any_true
4.4.3.6. i8x16.swizzle
4.4.3.7. i8x16.shuffle x∗
4.4.3.8. shape.splat
4.4.3.9. t1xN.extract_lane_sx? x
4.4.3.10. shape.replace_lane x
4.4.3.11. shape.vunop
4.4.3.12. shape.vbinop
4.4.3.13. txN.vrelop
4.4.3.14. txN.vishiftop
4.4.3.15. shape.all_true
4.4.3.16. txN.bitmask
4.4.3.17. t2xN.narrow_t1xM_sx
4.4.3.18. t2xN.vcvtop_t1xM_sx
4.4.3.19. t2xN.vcvtop_half_t1xM_sx?
-
断言: 由于 语法, N=M/2.
-
令 i∗ 为计算 lanest1xM(c1) 的结果。
-
如果 half 是 low, 那么
-
令 j∗ 为序列 i∗[0:N].
-
-
否则
-
令 j∗ 为序列 i∗[N:N].
-
-
令 c 为计算 lanest2xN−1(k∗).
其中
4.4.3.20. t2xN.vcvtop_t1xM_sx?_zero
4.4.3.21. i32x4.dot_i16x8_s
4.4.3.22. t2xN.extmul_half_t1xM_sx
-
断言: 由于 语法, N=M/2.
-
令 i1∗ 为计算 lanest1xM(c1) 的结果。
-
令 i2∗ 为计算 lanest1xM(c2) 的结果。
-
如果 half 是 low, 那么
-
否则
-
令 k∗ 为计算 imul∣t2∣(k1∗,k2∗) 的结果。
-
令 c 为计算 lanest2xN−1(k∗).
其中
4.4.3.23. t2xN.extadd_pairwise_t1xM_sx
4.4.4. 参数指令
4.4.4.1. drop
4.4.4.2. select (t∗)?
注意
在 WebAssembly 的未来版本中,select 可能允许每个选择有多个值。
4.4.5. 变量指令
4.4.5.1. local.get x
4.4.5.2. local.set x
4.4.5.3. local.tee x
4.4.5.4. global.get x
-
断言:由于 验证,F.module.globaladdrs[x] 存在。
-
设 a 为 全局地址 F.module.globaladdrs[x].
-
将值 val 推入堆栈。
4.4.5.5. global.set x
-
断言:由于 验证,F.module.globaladdrs[x] 存在。
-
设 a 为 全局地址 F.module.globaladdrs[x].
-
断言:由于 验证,堆栈顶部有一个值。
-
从栈中弹出值val。
注意
验证 确保全局变量实际上被标记为可变的。
4.4.6. 表格指令
4.4.6.1. table.get x
4.4.6.2. table.set x
4.4.6.3. table.size x
-
断言:根据 验证,F.module.tableaddrs[x] 存在。
-
令 a 为 表格地址 F.module.tableaddrs[x].
-
令 sz 为 tab.elem 的长度。
4.4.6.4. table.grow x
要么
-
或者
注意
The table.grow instruction is non-deterministic. It may either succeed, returning the old table size sz, or fail, returning −1. Failure must occur if the referenced table instance has a maximum size defined that would be exceeded. However, failure can occur in other cases as well. In practice, the choice depends on the resources available to the embedder.
4.4.6.5. table.fill x
-
断言:由于 验证,F.module.tableaddrs[x] 存在。
-
令 ta 为 表格地址 F.module.tableaddrs[x].
-
从栈中弹出值val。
-
如果 i+n 大于 tab.elem 的长度,则
-
陷入陷阱。
-
-
如果 0,则
-
返回。
-
-
将值 val 推入堆栈。
-
执行指令 table.set x。
-
将值 val 推入堆栈。
-
执行指令 table.fill x。
4.4.6.6. table.copy x y
-
断言:由于 验证,F.module.tableaddrs[x] 存在。
-
令 tax 为 表地址 F.module.tableaddrs[x].
-
断言:由于 验证,F.module.tableaddrs[y] 存在。
-
令 tay 为 表地址 F.module.tableaddrs[y].
-
如果 s+n 大于 taby.elem 的长度,或 d+n 大于 tabx.elem 的长度,则
-
陷入陷阱。
-
-
如果 n=0,则
返回。
-
如果 d≤s,则
-
否则
-
执行指令 table.copy x y.
4.4.6.7. table.init x y
-
断言:由于 验证,F.module.tableaddrs[x] 存在。
-
令 ta 为 表格地址 F.module.tableaddrs[x].
-
如果 s+n 大于 elem.elem 的长度,或者 d+n 大于 tab.elem 的长度,则
-
陷入陷阱。
-
-
如果 n=0,则
-
返回。
-
-
将值 val 推入堆栈。
-
执行指令 table.set x。
-
断言:由于之前对表格大小的检查,d+1<232.
-
断言:由于之前对段大小的检查,s+1<232.
-
执行指令 table.init x y.
4.4.6.8. elem.drop x
4.4.7. 内存指令
注意
在 load 和 store 指令中,对齐方式 memarg.align 不会影响语义。它指示访问内存的偏移量 ea 应该满足属性 eamod2memarg.align=0. WebAssembly 实现可以使用此提示来优化预期用途。违反该属性的未对齐访问仍然允许,并且必须成功,无论注释如何。但是,在某些硬件上它可能明显更慢。
4.4.7.1. t.load memarg 和 t.loadN_sx memarg
-
如果 N 不属于指令的一部分,那么
-
如果 ea+N/8 大于 mem.data 的长度,那么
-
陷入陷阱。
-
-
如果 N 和 sx 是指令的一部分,那么
-
否则
-
设 c 为常量,使得 bytest(c)=b∗.
-
-
将值 t.const c 推入堆栈。
4.4.7.2. v128.loadMxN_sx memarg
4.4.7.3. v128.loadN_splat memarg
-
如果 ea+N/8 大于 mem.data 的长度,那么
-
陷入陷阱。
-
-
令 L 为整数 128/N.
4.4.7.4. v128.loadN_zero memarg
4.4.7.5. v128.loadN_lane memarg x
-
如果 ea+N/8 大于 mem.data 的长度,那么
-
陷入陷阱。
-
-
令 L 为 128/N.
4.4.7.6. t.store memarg 和 t.storeN memarg
-
从栈顶弹出值 t.const c.
-
如果 N 不属于指令的一部分,那么
-
如果 ea+N/8 大于 mem.data 的长度,那么
-
陷入陷阱。
-
-
如果 N 是指令的一部分,则
-
否则
-
令 b∗ 为字节序列 bytest(c).
-
4.4.7.7. v128.storeN_lane memarg x
-
如果 ea+N/8 大于 mem.data 的长度,那么
-
陷入陷阱。
-
-
令 L 为 128/N.
4.4.7.8. memory.size
4.4.7.9. memory.grow
要么
-
或者
注意
指令 memory.grow 是非确定性的。它可能成功,返回旧的内存大小 sz,也可能失败,返回 −1。如果引用的内存实例定义了最大大小,并且会超过该大小,则失败必须发生。然而,失败也可能在其他情况下发生。在实践中,选择取决于可供嵌入器使用的资源。
4.4.7.10. memory.fill
-
从栈中弹出值val。
-
如果 d+n 大于 mem.data 的长度,则
-
陷入陷阱。
-
-
如果 n=0,则
-
返回。
-
-
将值 val 推入堆栈。
-
断言:由于之前对内存大小的检查,d+1<232.
-
将值 val 推入堆栈。
-
执行指令 memory.fill
4.4.7.11. memory.copy
返回。
-
如果 d≤s,则
-
否则
-
执行指令 memory.copy.
4.4.7.12. memory.init x
-
如果 s+n 大于 data.data 的长度,或者 d+n 大于 mem.data 的长度,则
-
陷入陷阱。
-
-
如果 n=0,则
-
返回。
-
-
令 b 为字节 data.data[s].
-
断言:由于之前对内存大小的检查,d+1<232.
-
断言:由于先前对内存大小的检查,s+1<232.
-
执行指令 memory.init x.
4.4.7.13. data.drop x
4.4.8. 控制指令
4.4.8.1. nop
-
什么也不做。
4.4.8.2. unreachable
-
陷入陷阱。
4.4.8.3. block blocktype instr∗ end
4.4.8.4. loop blocktype instr∗ end
4.4.8.5. if blocktype instr1∗ else instr2∗ end
4.4.8.6. br l
4.4.8.7. br_if l
4.4.8.8. br_table l∗ lN
4.4.8.9. return
4.4.8.10. call x
4.4.8.11. call_indirect x y
-
断言:由于验证,F.module.tableaddrs[x] 存在。
-
令 ta 为 表格地址 F.module.tableaddrs[x].
-
如果 i 不小于 tab.elem 的长度,那么
-
陷入陷阱。
-
-
如果r 是 ref.null t, 那么
-
陷入陷阱。
-
-
如果 ftactual 和 ftexpect 不同,则
-
陷入陷阱。
-
-
调用 地址为 a 的函数实例。
4.4.9. 块
4.4.9.1. 进入带标签 L 的 instr∗
-
将 L 推入堆栈。
-
跳转到指令序列 instr∗ 的开头。
注意
进入指令序列不需要正式的规约规则,因为标签 L 已嵌入到控制指令直接规约到的 管理指令 中。
4.4.9.2. 退出带有标签 L 的 instr∗
当一个块在没有跳转或陷阱中止的情况下结束时,执行以下步骤。
注意
此语义也适用于包含在 loop 指令中的指令序列。因此,循环的执行会从末尾掉落,除非显式执行反向分支。
4.4.10. 函数调用
以下辅助规则定义了通过一个 调用指令 调用 函数实例 并从其中返回的语义。
4.4.10.1. 调用 函数地址 a
4.4.10.2. 从函数返回
当函数执行到末尾时,如果没有发生跳转(例如,return) 或发生陷阱中断,则执行以下步骤。
4.4.10.3. 宿主函数
调用 宿主函数 具有非确定性行为。 它可能以 陷阱 终止,也可能正常返回。 但是,在后一种情况下,它必须根据其 函数类型 在堆栈上消耗和生成正确数量和类型的 WebAssembly 值 。
宿主函数也可以修改 存储 。 然而,所有存储修改必须导致原始存储的 扩展 ,即它们只能修改可变内容,并且不能删除实例。 此外,生成的存储必须是 有效的 ,即其中的所有数据和代码都类型正确。
这里,hf(S;valn) 表示在当前存储 S 中,使用参数 valn 执行宿主函数 hf 的实现定义方式。它产生一组可能的结果,其中每个元素要么是修改后的存储 S′ 和一个 结果 的对,要么是表示发散的特殊值 ⊥。如果至少有一个参数,其结果集不是单一的,则宿主函数是非确定性的。
为了使 WebAssembly 实现能够在存在宿主函数的情况下保持 健全性,每个 宿主函数实例 都必须是 有效的,这意味着它必须遵守适当的前置条件和后置条件:在 有效存储 S 下,给定与指定的参数类型 t1n 匹配的参数 valn, 执行宿主函数必须产生一组非空的可能结果,每个结果要么是发散,要么由一个有效存储 S′ 组成,该存储是 S 的 扩展,以及一个与指定的返回类型 t2m 匹配的结果。所有这些概念在 附录 中进行了精确定义。
4.4.11. 表达式
一个 表达式 是相对于 当前 帧 进行求值的,该帧指向其包含的 模块实例。
值 val 是求值的結果。
4.5. 模块
对于模块,执行语义主要定义了 实例化,它会 分配 模块及其包含的定义的实例,从包含的 元素 和 数据 段初始化 表格 和 内存,如果存在则调用 启动函数。它还包括对导出函数的 调用。
4.5.1. 外部类型
为了将外部值与导入进行比较,这些值由外部类型进行分类。以下辅助类型规则指定了相对于存储 S的这种类型关系,其中引用了实例。
4.5.1.1. func a
4.5.1.2. table a
4.5.1.3. mem a
4.5.1.4. global a
4.5.2. 值类型
为了将参数值与导出的函数的参数类型进行比较,值被分类为值类型。以下辅助类型规则指定了此类型关系,相对于一个可能包含引用地址的存储 S。
4.5.2.1. 数值 t.const c
-
该值在数值类型 t 中有效。
4.5.2.2. 空引用 ref.null t
-
该值在引用类型 t 中有效。
4.5.2.3. 函数引用 ref a
4.5.2.4. 外部引用 ref.extern a
-
该值在引用类型 externref 中有效。
4.5.3. 分配
函数、表格、内存和全局变量的新实例在存储 S 中被分配,如下面辅助函数定义。
4.5.3.1. 函数
4.5.3.2. 宿主函数
-
设 a 为 S 中第一个空闲函数地址。
-
返回 a.
注意
WebAssembly 语义本身永远不会分配宿主函数,但可以由嵌入器分配。
4.5.3.3. 表格
4.5.3.4. Memories
4.5.3.5. 全局变量
-
设 globaltype 为要分配的 全局变量类型,并且 val 为用来初始化全局变量的值。
-
设 a 为 S 中第一个空闲的 全局变量地址。
-
设 globalinst 为 全局变量实例 {type globaltype,value val}.
-
将 globalinst 追加到 globals 的 S 中。
-
返回 a.
4.5.3.6. 元素段
4.5.3.7. 数据段
4.5.3.8. 扩展 表
4.5.3.9. 增长 内存
-
如果 len 大于 216, 则失败。
4.5.3.10. 模块
用于 模块 的分配函数需要一组合适的 外部值,这些外部值被假定为与模块的 导入 向量 匹配;此外,还需要模块的 全局变量 的初始化 值 列表,以及模块的 元素段 的 引用 向量列表。
-
令 module 为要分配的 模块,而 externvalim∗ 为提供模块导入的 外部值 向量,val∗ 为模块的 全局变量 的初始化 值,而 (ref∗)∗ 为模块的 元素段 的 引用 向量。
-
令 globaladdr∗ 为以索引顺序连接的 全局地址 globaladdri。
-
令 funcaddrmod∗ 为从 externvalim∗ 中提取的 函数地址 列表,与 funcaddr∗ 连接。
-
令 tableaddrmod∗ 为从 externvalim∗ 中提取的 表地址 列表,与 tableaddr∗ 连接。
-
令 globaladdrmod∗ 为从 externvalim∗ 中提取的 全局地址 列表,与 globaladdr∗ 连接。
-
对于每个 导出 exporti 在 module.exports 中,执行以下操作
-
如果 exporti 是 函数索引 x 的函数导出,则令 externvali 为 外部值 func (funcaddrmod∗[x]).
-
否则,如果 exporti 是 表格索引 x 的表格导出,则令 externvali 为 外部值 table (tableaddrmod∗[x]).
-
否则,如果 exporti 是 内存索引 x 的内存导出,则令 externvali 为 外部值 mem (memaddrmod∗[x]).
-
否则,如果 exporti 是 全局索引 x 的全局导出,则令 externvali 为 外部值 global (globaladdrmod∗[x]).
-
令 exportinsti 为 导出实例 {name (exporti.name),value externvali}.
-
-
令 exportinst∗ 为 导出实例 exportinsti 按索引顺序的串联。
-
令 moduleinst 为 模块实例 {types (module.types), funcaddrs funcaddrmod∗, tableaddrs tableaddrmod∗, memaddrs memaddrmod∗, globaladdrs globaladdrmod∗, exports exportinst∗}.
-
返回 moduleinst.
其中
这里,符号 allocx∗ 是对多个 分配 对象类型 X 的简写,定义如下
此外,如果省略号 … 是一个序列 An(如全局变量或表格),那么该序列的元素将逐点传递给分配函数。
注意
模块分配的定义与其相关函数的分配相互递归,因为生成的模块实例 moduleinst 被作为参数传递给函数分配器,以形成必要的闭包。在实现中,这种递归可以通过在次要步骤中对其中一个进行修改来轻松地解开。
4.5.4. 实例化
给定一个 存储 S,一个 模块 module 使用一个外部值列表 externvaln 实例化,该列表提供所需的导入,如下所示。
实例化检查模块是否 有效 以及提供的导入是否 匹配 声明的类型,否则可能会 *失败* 并出现错误。实例化也可能导致从初始化一个活动段的表格或内存或从执行启动函数中 陷阱。如何报告这些条件取决于 嵌入器。
-
-
失败。
-
-
断言:module 是 有效的,具有 外部类型 externtypeimm 对其 导入 进行分类。
-
如果 导入 的数量 m 不等于提供的 外部值 的数量 n,那么
-
失败。
-
-
对于每个 外部值 externvali 在 externvaln 和 外部类型 externtypei′ 在 externtypeimn 中,执行以下操作:
-
如果 externvali 在存储 S 中不 有效,对于 外部类型 externtypei,那么
-
失败。
-
-
如果 externtypei 与 externtypei′ 不 匹配,那么
-
失败。
-
-
-
设 moduleinstinit 是一个辅助模块 实例 {globaladdrs globals(externvaln),funcaddrs moduleinst.funcaddrs},它只包含最终模块实例 moduleinst 中的导入全局变量以及导入和分配的函数,定义如下。
-
设 Finit 是一个辅助 帧 {module moduleinstinit,locals ϵ}.
-
将帧 Finit 推送到栈中。
-
令 (ref∗)∗ 为由 module 中的 元素段 确定的 引用 向量列表。它们可以按如下方式计算。
-
从堆栈中弹出帧 Finit。
-
令 moduleinst 为一个新的模块实例,它从 module 在存储 S 中 分配,导入为 externvaln, 全局初始化值为 val∗, 元素段内容为 (ref∗)∗, 令 S′ 为模块分配产生的扩展存储。
-
令 F 为辅助 帧 {module moduleinst,locals ϵ}.
-
将帧 F 推入堆栈。
-
对于 module.elems 中每个 元素段 elemi,其 模式 为 active {table tableidxi,offset einstri∗ end},执行以下操作:
-
对于每个 数据段 datai 在 module.datas 中,其 模式 形式为 active {memory memidxi,offset dinstri∗ end},执行以下操作:
-
断言:由于 验证,帧 F 现在位于堆栈顶部。
-
从堆栈中弹出帧 F。
其中
注意
模块 分配 和 求值 全局 初始化器和 元素段 是相互递归的,因为全局初始化 值 val∗ 和元素段内容 (ref∗)∗ 会被传递给模块分配器,同时依赖于模块实例 moduleinst 和存储 S′ 分配返回。然而,这种递归只是一种规范手段。在实践中,初始化值可以 事先确定,通过分阶段模块分配,首先,模块自身的 函数实例 在存储中预先分配,然后对初始化表达式进行求值,然后分配模块实例的其余部分,最后将新函数实例的 module 字段设置为该模块实例。这是可能的,因为 验证 确保初始化表达式实际上不能调用函数,只能获取它们的引用。
在对存储进行任何可观察到的修改之前,都会检查所有故障条件。存储修改不是原子的;它以单个步骤发生,这些步骤可能与其他线程交织在一起。
4.5.5. 调用
一旦一个 模块 已经 实例化,任何导出的函数都可以通过其 函数地址 funcaddr 在 存储 S 中以及一个适当的列表 val∗ 的 值 参数从外部 *调用*。
如果参数不符合 函数类型,则调用可能 *失败* 并返回错误。调用也可能导致 陷阱。由 嵌入器 定义如何报告这些情况。
注意
如果 嵌入器 API 在执行调用之前本身执行类型检查,无论是静态的还是动态的,那么除了陷阱之外,不会发生其他错误。
执行以下步骤
函数返回后,执行以下步骤。
值 valresm 作为调用的结果返回。
5. 二进制格式
5.1. 约定
WebAssembly 模块 的二进制格式是对其 抽象语法 的密集线性 *编码*。[1]
该格式由一个 *属性语法* 定义,其唯一的终结符是 字节。字节序列是模块的格式良好的编码,当且仅当它由该语法生成。
该语法中的每个产生式都正好有一个综合属性:相应的字节序列编码的抽象语法。因此,属性语法隐式地定义了一个 *解码* 函数(即,二进制格式的解析函数)。
除了少数例外,二进制语法与抽象语法的语法非常相似。
注意
抽象语法中的某些短语在二进制格式中有多种可能的编码。例如,数字可以像具有可选前导零一样进行编码。解码器实现必须支持所有可能的替代方案;编码器实现可以选择任何允许的编码。
包含 WebAssembly 模块的二进制格式文件的推荐扩展名为“.wasm”,推荐的 媒体类型 为“application/wasm”。
可以在此处定义的基本表示之上定义额外的编码层(例如,引入压缩)。但是,这些层超出了当前规范的范围。
5.1.1. 语法
在定义二进制格式的语法规则时,采用以下约定。它们反映了用于 抽象语法 的约定。为了区分二进制语法的符号和抽象语法的符号,采用 typewriter 字体来表示前者。
-
终结符是 字节,用十六进制表示法表示:0x0F.
-
非终结符以打字机字体书写:valtype,instr.
-
Bn 是 n≥0 次 B 的迭代序列。
-
B∗ 是一个可能是空的 B 的迭代序列。(这是一种简写方式,用于 Bn,其中 n 不相关。)
-
B? 是 B 的可选出现。(这是一种简写方式,用于 Bn,其中 n≤1。)
-
x:B 表示与非终结符 B 相同的语言,但同时也为变量 x 绑定了为 B 合成的属性。模式也可以用作变量,例如 7:B.
-
产生式以 sym::=B1⇒A1 ∣ … ∣ Bn⇒An, 其中每个 Ai 是在给定情况下为 sym 合成的属性,通常从 Bi 中绑定的属性变量中合成。
-
一些产生式通过括号中的边际条件进行补充,这些条件限制了产生式的适用性。它们为将产生式组合扩展为许多独立情况提供了一种简写方式。
-
如果相同的元变量或非终结符符号在一个产生式中多次出现(在语法或属性中),那么所有这些出现必须具有相同的实例。(这是一种简写方式,用于需要多个不同变量相等的边际条件。)
5.1.2. 辅助符号
在处理二进制编码时,还使用以下符号
-
ϵ 表示空字节序列。
-
∣∣B∣∣ 是从推导中生成产生式 B 的字节序列的长度。
5.1.3. 向量
5.2. 值
5.2.1. 字节
字节 自己进行编码。
5.2.2. 整数
所有 整数 使用 LEB128 可变长度整数编码进行编码,可以是无符号或有符号变体。
无符号整数 使用 无符号 LEB128 格式进行编码。作为附加约束,对类型为 uN 的值的总字节数不能超过 ceil(N/7) 字节。
带符号整数 使用 有符号 LEB128 格式编码,该格式使用二进制补码表示。作为额外的约束,编码类型为 sN 的值的字节总数不能超过 ceil(N/7) 个字节。
未解释整数 编码为有符号整数。
5.2.3. 浮点数
浮点数 值直接由其 [IEEE-754-2019](第 3.4 节)中的位模式在 小端 字节顺序中进行编码
5.2.4. 名称
名称 被编码为一个包含名称字符序列的 [UNICODE](第 3.9 节)UTF-8 编码的 向量 字节。
辅助 utf8 函数表示此编码,定义如下
注意
与其他一些格式不同,名称字符串不以 0 结尾。
5.3. 类型
5.3.1. 数字类型
数字类型 由单个字节编码。
5.3.2. 向量类型
向量类型 也由单个字节编码。
5.3.3. 引用类型
引用类型 也由单个字节编码。
5.3.4. 值类型
值类型 使用其各自的编码作为 数字类型、向量类型 或 引用类型 进行编码。
注意
值类型可以出现在允许使用类型索引的上下文中,例如在块类型的情况下。因此,类型的二进制格式对应于小负数的带符号 LEB128 编码,以便它们将来可以与(正)类型索引共存。
5.3.5. 结果类型
结果类型通过各自的值类型向量进行编码。
5.3.6. 函数类型
函数类型通过字节 0x60 后面跟着的各自的参数类型和结果类型向量进行编码。
5.3.7. 限制
限制通过一个前导标志进行编码,该标志指示是否存在最大值。
5.3.8. 内存类型
5.3.9. 表类型
5.3.10. 全局类型
5.4. 指令
指令 由操作码进行编码。每个操作码由一个字节表示,后面跟着指令的立即数参数(如果有)。唯一的例外是 结构化控制指令,它由多个操作码组成,用来括起它们的嵌套指令序列。
注意
用于编码指令的字节码范围内的间隙保留供将来扩展。
5.4.1. 控制指令
控制指令 具有不同的编码。对于结构化指令,构成嵌套块的指令序列以 end 和 else 的显式操作码结尾。
块类型 使用特殊的压缩形式进行编码,可以是字节 0x40(表示空类型),单个 值类型,或者作为以正 有符号整数 编码的 类型索引。
5.4.2. 引用指令
引用指令 由单个字节码表示。
5.4.3. 参数化指令
参数化指令 由单个字节码表示,可能后跟类型注释。
5.4.4. 变量指令
5.4.5. 表格指令
表格指令 用单个字节或一个字节前缀后跟一个可变长度的 无符号整数 表示。
5.4.6. 内存指令
每个内存指令变体都使用不同的字节码进行编码。加载和存储指令后面跟着其memarg立即数的编码。
注意
在未来的 WebAssembly 版本中,memory.size、memory.grow、memory.copy 和 memory.fill 指令编码中出现的额外零字节可用于索引其他内存。
5.4.7. 数值指令
所有数值指令变体都由不同的字节码表示。
const 指令后面跟着相应的字面量。
所有其他数字指令都是没有立即数的普通操作码。
所有饱和截断指令都有一个字节的前缀,而实际的操作码则由一个可变长度的 无符号整数 编码。
5.4.8. 向量指令
向量指令 的所有变体都由独立的字节码表示。它们都有一个字节前缀,而实际的操作码由一个可变长度的 无符号整数 编码。
向量加载和存储后是其 memarg 介质的编码。
const 指令后紧跟 16 个立即字节,这些字节将被转换为 i128,字节序为 littleendian。
shuffle 指令后紧跟 16 个 laneidx 立即数的编码。
extract_lane 和 replace_lane 指令后紧跟一个 laneidx 立即数的编码。
所有其他向量指令都是没有立即数的纯操作码。
5.4.9. 表达式
5.5. 模块
模块的二进制编码被组织成节。大多数节对应于一个模块记录的组件,除了函数定义被分成两个节,将它们的类型声明在函数节中与它们在代码节中的主体分离。
注意
这种分离使模块中函数的并行和流式编译成为可能。
5.5.1. 索引
所有索引都使用它们的值进行编码。
5.5.2. 节
每个节包含:
-
一个字节的节标识符,
-
以字节为单位的内容的u32大小,
-
实际的内容,其结构取决于节标识符。
每个节都是可选的;省略的节等同于存在且内容为空的节。
以下带参数的语法规则定义了具有标识符N的节的通用结构,其内容由语法B描述。
对于大多数部分,内容B编码一个向量。 在这些情况下,空结果ϵ被解释为空向量。
注意
除了未知的自定义部分,size对于解码不是必需的,但可以在浏览二进制文件时用于跳过部分。 如果大小与二进制内容B的长度不匹配,则模块格式错误。
使用以下部分 ID
ID |
部分 |
---|---|
0 | |
1 | |
2 | |
3 | |
4 | |
5 | |
6 | |
7 | |
8 | |
9 | |
10 | |
11 | |
12 |
注意
部分 ID 不总是对应于模块编码中的部分顺序。
5.5.3. 自定义部分
自定义部分 的 ID 为 0。 它们旨在用于调试信息或第三方扩展,并且被 WebAssembly 语义忽略。 它们的内容包括一个名称,以进一步标识自定义部分,后面跟着一个用于自定义用途的未解释字节序列。
注意
如果实现解释了自定义部分的数据,则该数据中的错误或部分的放置位置不得使模块失效。
5.5.4. 类型部分
5.5.5. 导入部分
5.5.6. 函数部分
函数节的 ID 为 3。它解码成一个 类型索引 的向量,表示 函数 中的 type 字段,这些函数位于 模块 的 funcs 组件中。相应函数的 locals 和 body 字段在 代码节 中单独编码。
5.5.7. 表格节
5.5.8. 内存节
5.5.9. 全局段
5.5.10. 导出段
5.5.11. 开始部分
5.5.12. 元素部分
元素段 的 id 为 9。它解码为一个 元素段 的向量,这些段表示 elems 组件的一个 模块。
注意
初始整数可以解释为一个位域。位 0 区分被动段或声明段和主动段,位 1 表示主动段存在显式表格索引,否则区分被动段和声明段,位 2 表示使用元素类型和元素 表达式 而不是元素种类和元素索引。
将来版本的 WebAssembly 中可能会添加其他元素种类。
5.5.13. 代码段
代码段 的 id 为 10。它解码为一个代码条目向量,这些条目是 值类型 向量和 表达式 的对。它们表示 locals 和 body 字段的一个 函数 在 funcs 组件的一个 模块。相应的函数的 type 字段在 函数段 中单独编码。
每个代码条目的编码包括
局部变量声明被压缩成一个向量,其条目包含
表示相同值类型的 计数 个局部变量。
在此,code 遍历对 (valtype∗,expr)。元函数 concat((t∗)∗) 连接所有序列 ti∗ 在 (t∗)∗. 任何导致结果序列长度超出 vector 最大尺寸的代码格式错误。
注意
与 sections 类似,代码 size 在解码时不需要,但可以用于在二进制文件中导航时跳过函数。如果尺寸与相应函数代码的长度不匹配,则模块格式错误。
5.5.14. 数据段
5.5.15. 数据计数段
数据计数段 的 ID 为 12。它解码为一个可选的 u32,表示 数据段 在 数据段 中的数量。如果此计数与数据段向量长度不匹配,则模块格式错误。
注意
数据计数区用于简化单遍验证。由于数据区出现在代码区之后,memory.init 和 data.drop 指令在读取数据区之前无法检查数据段索引是否有效。数据计数区出现在代码区之前,因此单遍验证器可以使用此计数,而不是延迟验证。
5.5.16. 模块
一个 模块 的编码以一个包含 4 字节魔数(字符串 ‘\0asm’) 和一个版本字段的序言开始。WebAssembly 二进制格式的当前版本为 1。
序言之后是一系列 区段。自定义区段 可以插入此序列中的任何位置,而其他区段最多只能出现一次,并且必须按照规定的顺序排列。所有区段都可以为空。
由(可能为空的)函数 和 代码 区段产生的向量的长度必须匹配。
同样,可选的数据计数必须与 数据段 向量长度匹配。此外,如果代码区段中出现任何 数据索引,则数据计数必须存在。
其中,对于每个 ti∗,ei 在 coden,
注意
WebAssembly 二进制格式的版本将来可能会增加,如果需要对格式进行向后不兼容的更改。但是,此类更改预计很少发生,即使有也只会在极少数情况下发生。二进制格式旨在向前兼容,以便将来可以进行扩展而无需增加其版本。
6. 文本格式
6.1. 约定
WebAssembly 模块 的文本格式是其 抽象语法 转换为 S 表达式 的渲染。
与 二进制格式 一样,文本格式由一个属性语法定义。文本字符串是模块的格式良好的描述,当且仅当它是根据语法生成的。此语法的每个产生式最多有一个综合属性:相应的字符序列表达的抽象语法。因此,属性语法隐式地定义了一个解析函数。一些产生式还将 上下文 作为继承属性,该属性记录绑定 标识符。
除了少数例外,文本语法的核心与抽象语法的语法密切相关。但是,它还定义了许多缩写,这些缩写是对核心语法的“语法糖”。
包含文本格式 WebAssembly 模块的文件的推荐扩展名为“.wat”。具有此扩展名的文件被假定为使用 UTF-8 编码,如 [UNICODE](第 2.5 节)所述。
6.1.1. 语法
在定义文本格式的语法规则时采用以下约定。它们反映了用于 抽象语法 和 二进制格式 的约定。为了将文本语法的符号与抽象语法的符号区分开来,采用 打字机 字体来表示前者。
-
终结符可以是引号括起来的文字字符串,也可以用 [UNICODE] 标量值表示:‘module’, U+0A.(所有直接写出的字符都明确地来自 Unicode 的 7 位 ASCII 子集。)
-
非终结符以打字机字体书写:valtype,instr.
-
Tn 是 n≥0 次 T 的迭代序列。
-
T∗ 是可能为空的 T 迭代序列。(这是 Tn 的简写形式,在 n 不相关的情况下使用。)
-
T+ 是一个或多个 T 迭代的序列。(这是 Tn 的简写形式,在 n≥1 的情况下使用。)
-
T? 是 T 的可选出现。(这是 Tn 的简写形式,在 n≤1 的情况下使用。)
-
x:T 表示与非终结符 T 相同的语言,但它也将变量 x 绑定到为 T 合成的属性。模式也可以用作变量,例如 (x,y):T.
-
产生式写成 sym::=T1⇒A1 ∣ … ∣ Tn⇒An, 其中每个 Ai 是在给定情况下为 sym 合成的属性,通常来自在 Ti 中绑定的属性变量。
-
一些产生式通过括号中的边际条件进行补充,这些条件限制了产生式的适用性。它们为将产生式组合扩展为许多独立情况提供了一种简写方式。
-
如果同一个元变量或非终结符在产生式中多次出现(在语法或属性中),那么所有这些出现都必须具有相同的实例化。
6.1.2. 缩写
除了与 抽象语法 紧密对应的核心语法之外,文本语法还定义了一些缩写,这些缩写可用于方便性和可读性。
缩写由重写规则定义,这些规则指定了它们扩展到核心语法的形式
在将核心语法规则应用于构造抽象语法之前,假定这些扩展是递归地按出现顺序应用的。
6.1.3. 上下文
文本格式允许使用符号 标识符 来代替 索引。为了将这些标识符解析为具体的索引,一些语法产生式由标识符上下文 I 索引,它作为合成属性,记录了每个 索引空间 中声明的标识符。此外,上下文记录了模块中定义的类型,以便可以为 函数 计算 参数 索引。
将标识符上下文定义为 记录 I 非常方便,其抽象语法如下
对于每个索引空间,这样的上下文包含分配给已定义索引的 标识符 列表。未命名的索引与这些列表中的空条目 (ϵ) 相关联。
如果在没有索引空间包含重复标识符的情况下,则标识符上下文为格式正确。
6.1.3.1. 约定
为了避免不必要的混乱,在写出标识符上下文时会省略空组件。例如,记录 {} 是一个 标识符上下文 的简写形式,其组件全部为空。
6.1.4. 向量
向量 写成普通的序列,但对这些序列的长度有限制。
6.2. 词法格式
6.2.1. 字符
文本格式为源文本分配含义,源文本由字符序列组成。假设字符表示为有效的[UNICODE](第 2.4 节)标量值。
6.2.2. 标记
源文本中的字符流从左到右被划分为标记序列,如下面的语法定义所示。
令牌根据 *最长匹配* 规则从输入字符流中形成。 也就是说,下一个令牌总是由上述词法语法识别的最长可能的字符序列组成。 令牌可以用 空格 分隔,但除了字符串外,它们本身不能包含空格。
*关键字* 令牌是通过在本章的词法生产中以字面形式出现的 终结符 隐式定义的,例如 ‘keyword’, 或在本章中出现的显式定义。
任何不属于其他类别的令牌都被认为是 *保留的*,并且不能出现在源代码中。
6.2.3. White Space
White space is any sequence of literal space characters, formatting characters, or comments. The allowed formatting characters correspond to a subset of the ASCII format effectors, namely, horizontal tabulation (U+09), line feed (U+0A), and carriage return (U+0D).
空白字符只用于分隔tokens,除此之外将被忽略。
6.3. 值
本节中的语法产生式定义了 _词法语法_,因此不允许使用任何 空白。
6.3.1. 整数
所有 整数 可以用十进制或十六进制表示。在两种情况下,数字都可以选择性地用下划线分隔。
整数字面量的允许语法取决于大小和符号。此外,它们的数值必须在相应的类型范围内。
未解释整数 可以写成有符号或无符号形式,并在抽象语法中归一化为无符号形式。
6.3.2. 浮点数
浮点数 值可以用十进制或十六进制表示。
字面量的值不能超出对应 [IEEE-754-2019] 类型的可表示范围(即,数值不能溢出到 ±infinity),但它可能会被 舍入 到最接近的可表示值。
注意
可以通过使用十六进制表示法来防止舍入,该表示法不超过所需类型支持的有效位数。
浮点数也可以写成无穷大或规范 NaN(非数字)的常量。此外,通过提供显式有效载荷值可以表示任意 NaN 值。
6.3.3. 字符串
字符串表示字节序列,可以用来表示文本和二进制数据。它们用引号括起来,可以包含除 ASCII 控制字符、引号 (‘"’) 或反斜杠 (‘\’) 之外的任何字符,除非用转义序列表示。
字符串字面量中的每个字符都表示其 UTF-8 [UNICODE] (第 2.5 节) 编码对应的字节序列,除了十六进制转义序列 ‘\hh’,它们表示相应值的原始字节。
6.3.4. 名称
名称 是表示字面字符序列的字符串。名称字符串必须形成有效的 UTF-8 编码,如 [UNICODE](第 2.5 节)所定义,并被解释为 Unicode 标量值的字符串。
注意
假设源文本本身编码正确,不包含任何十六进制字节转义的字符串始终是有效的名称。
6.3.5. 标识符
索引 可以以数字和符号形式给出。代替索引的符号 *标识符* 以 ‘$’ 开头,后面跟着任何不包含空格、引号、逗号、分号或括号的可打印 ASCII 字符序列。
6.3.5.1. 约定
一些缩写的扩展规则需要插入一个 *新的* 标识符。这可以是任何语法有效的标识符,只要它在给定的源文本中没有出现过。
6.4. 类型
6.4.1. 数字类型
6.4.2. 向量类型
6.4.3. 引用类型
6.4.4. 值类型
6.4.5. 函数类型
注意
函数类型中参数的可选标识符名称仅用于文档目的。它们不能在任何地方被引用。
6.4.5.1. 缩写
多个匿名参数或结果可以合并到单个声明中
6.4.6. 限制
6.4.7. 内存类型
6.4.8. 表类型
6.4.9. 全局类型
6.5. 指令
指令在语法上分为简单指令和结构化指令。
此外,作为语法上的简写,指令可以用 折叠 形式的 S 表达式来编写,以便在视觉上进行分组。
6.5.1. 标签
结构化控制指令 可以用符号化的 标签标识符 进行注释。它们是唯一可以在指令序列中局部绑定的 符号标识符。以下语法通过 组合 上下文和额外的标签条目来处理对 标识符上下文 的相应更新。
注意
在标识符上下文中,新的标签条目被插入标签列表的开头。这实际上将所有现有标签向上移动一位,反映了控制指令是相对索引而不是绝对索引的事实。
如果已经存在具有相同名称的标签,则它会被遮蔽,并且先前标签将无法访问。
6.5.2. 控制指令
结构化控制指令 可以绑定一个可选的符号 标签标识符。相同的标签标识符可以在相应的 end 和 else 伪指令后重复,以指示匹配的分隔符。
它们的 块类型 被指定为 类型使用,类似于 函数 的类型。但是,语法为空或仅包含单个 结果 的类型使用情况不被视为 缩写 用于内联 函数类型,而是直接解析为可选的 值类型。
所有其他控制指令都按原样表示。
注意
对于 call_indirect 的规则中,边条件说明 标识符上下文 I′ 必须仅包含未命名的条目,这强制了在类型注释中出现的任何 param 声明中都不能绑定标识符。
6.5.2.1. 缩写
‘else’ ‘if’ 指令的关键字可以省略,如果后面的指令序列为空。
此外,为了向后兼容性,可以省略到 ‘call_indirect’ 的表格索引,默认为 0.
6.5.3. 引用指令
6.5.4. 参数化指令
6.5.5. 变量指令
6.5.6. 表指令
6.5.6.1. 缩写
为了向后兼容,所有表索引 都可以从表指令中省略,默认值是 0.
6.5.7. 内存指令
内存指令的偏移量和对齐立即数是可选的。偏移量默认为 0,对齐为相应内存访问的存储大小,即其自然对齐。从语法上讲,一个offset或align短语被认为是一个单独的关键字标记,因此不允许在‘=’周围使用空白。
6.5.8. 数值指令
6.5.9. 向量指令
向量内存指令具有可选的偏移量和对齐方式立即数,类似于内存指令。
向量常量指令具有必需的形状 描述符,用于确定如何解析后续的值。
6.5.10. 折叠指令
指令可以写成 S-表达式,通过将它们分组为“折叠”形式。在这个表示法中,指令用圆括号括起来,并可以包含嵌套的折叠指令来表示其操作数。
在 块指令 的情况下,折叠形式省略了 ‘end’ 分隔符。对于 if 指令,两个分支都必须用嵌套的 S-表达式括起来,并以关键字 ‘then’ 和 ‘else’ 开头。
由以下缩写递归定义的所有短语集合构成了辅助句法类 foldedinstr。这种折叠指令可以出现在任何常规指令可以出现的地方。
注意
例如,指令序列
可以折叠成
折叠指令仅仅是语法糖,不暗示额外的语法或基于类型的检查。
6.5.11. 表达式
表达式以指令序列的形式编写。没有显式包含 ‘end’ 关键字,因为它们只出现在方括号的位置。
6.6. 模块
6.6.1. 索引
索引 可以以原始数字形式或作为符号 标识符 给出,当被相应构造绑定时。这些标识符会在合适的 标识符上下文 I 空间中查找。
6.6.2. 类型
类型定义可以绑定符号 类型标识符。
6.6.3. 类型使用
类型使用是对 类型定义 的引用。它可以选择性地通过内联的 参数 和 结果 声明进行增强。这允许绑定符号 标识符 来命名参数的 局部索引。如果给出内联声明,则它们的类型必须与引用的 函数类型 匹配。
typeuse 的合成属性是一个对,它包含使用的 类型索引 和包含可能的参数标识符的局部 标识符上下文。以下辅助函数从参数中提取可选标识符
6.6.3.1. 缩写
一个 typeuse 也可以完全由内联的 参数 和 结果 声明替换。在这种情况下,会自动插入一个 类型索引
其中 x 是当前模块中定义的最小现存 类型索引,其定义为 函数类型 [t1∗]→[t2∗]。如果不存在此类索引,则会插入一个新的 类型定义,其形式为
插入到模块的末尾。
缩写按其出现的顺序扩展,因此先前插入的类型定义会被连续的扩展所重用。
6.6.4. 导入
导入中的描述符可以绑定符号函数、表格、内存或全局 标识符。
6.6.4.1. 缩写
6.6.5. 函数
函数定义可以绑定一个符号化的 函数标识符,以及 局部标识符,分别用于其 参数 和局部变量。
局部 标识符上下文 I′′ 的定义使用以下辅助函数来从局部变量中提取可选标识符
注意
关于 I′′ 的良构性条件确保参数和局部变量不包含重复的标识符。
6.6.5.1. 缩写
多个匿名局部变量可以合并成单个声明。
注意
如果“…”包含额外的导出子句,则后一种缩写可以重复应用。因此,函数声明可以包含任意数量的导出,可能后面跟着一个导入。
6.6.6. 表格
表格定义可以绑定一个符号表格标识符。
6.6.6.1. 缩写
一个元素段可以与表格定义一起内联给出,在这种情况下,它的偏移量为0,并且限制在表格类型中从给定段的长度推断出来。
注意
如果“…”包含额外的导出子句,则后一个缩写可以重复使用。因此,表格声明可以包含任意数量的导出,后面可能紧跟着导入。
6.6.7. 内存
内存定义可以绑定符号 内存标识符。
6.6.7.1. 缩写
一个数据段可以在内存定义中内联给出,在这种情况下,它的偏移量为0,并且限制的内存类型从数据的长度推断,向上取整到页面大小
注意
如果“…” 包含额外的导出子句,则后一种缩写可以重复使用。因此,内存声明可以包含任意数量的导出,后面可能跟着一个导入。
6.6.8. 全局变量
全局定义可以绑定一个符号化的 全局标识符.
6.6.8.1. 缩写
注意
如果“…”包含额外的导出子句,则后一种缩写可以重复应用。因此,全局声明可以包含任意数量的导出,之后可以跟着一个导入。
6.6.9. 导出
导出的语法直接反映了它们的 抽象语法。
6.6.9.1. 缩写
6.6.10. 开始函数
一个开始函数是根据其索引定义的。
注意
在模块中最多只能出现一个启动函数,这可以通过在module语法上设置适当的辅助条件来确保。
6.6.11. 元素段
元素段允许使用可选的表格索引来标识要初始化的表格。
6.6.11.1. 缩写
作为缩写,单个指令可以替代活动元素段的偏移量或作为元素表达式。
此外,元素列表可以写成一系列函数索引。
表格使用可以省略,默认值为0。此外,为了向后兼容 WebAssembly 的早期版本,如果省略了表格使用,则‘func’关键字也可以省略。
作为另一种缩写形式,元素段也可以在 表格 定义中内联指定;请参阅相关部分。
6.6.12. 数据段
数据段允许使用可选的 内存索引 来标识要初始化的内存。数据以 字符串 形式写入,该字符串可以拆分为可能为空的单个字符串字面量的序列。
注意
在当前版本的 WebAssembly 中,唯一有效的内存索引是 0 或解析为相同值的符号 内存标识符。
6.6.12.1. 缩写
作为一种缩写,单个指令可以出现在活动数据段的偏移量位置。
此外,可以省略内存使用,默认值为 0。
作为另一种缩写,数据段也可以与 内存 定义一起内联指定;请参阅相应的章节。
6.6.13. 模块
模块由一系列字段组成,这些字段可以按任何顺序出现。所有定义及其相应的绑定 标识符 作用域涵盖整个模块,包括它们之前的文本。
模块可以选择绑定一个 标识符 来命名模块。该名称仅起文档作用。
对 模块 的组成施加以下限制: m1⊕m2 当且仅当以下条件成立时定义:
初始 标识符上下文 I 的定义使用以下辅助定义,该定义将每个相关定义映射到一个具有一个(可能是空的)标识符的单一上下文
6.6.13.1. 缩写
在源文件中,围绕模块主体的顶级 (module …) 可以省略。
附录 A
A.1 嵌入
WebAssembly 实现通常会嵌入到宿主环境中。嵌入器实现宿主环境与本规范主体定义的 WebAssembly 语义之间的连接。预计嵌入器将以定义明确的方式与语义交互。
本节以嵌入器可以通过其访问 WebAssembly 语义的入口点的形式定义一个合适的接口。该接口旨在完整,这意味着嵌入器不需要直接引用 WebAssembly 规范的其他功能部分。
类型
在嵌入器接口的描述中,来自 抽象语法 和 运行时抽象机 的语法类用作变量的名称,这些变量范围涵盖该类中的所有可能对象。因此,这些语法类也可以解释为类型。
对于数字参数,使用类似于 n:u32 的符号来指定符号名称,以及相应的取值范围。
错误
接口操作失败由辅助语法类指示
除了本节中明确指定的错误条件外,当达到特定的 实现限制 时,实现也可能返回错误。
注意
根据此定义,错误是抽象且不具体的。实现可以将其细化以携带合适的分类和诊断消息。
先决条件和后置条件
某些操作会声明其参数的先决条件或其结果的后置条件。满足先决条件是嵌入器的责任。如果满足,则语义将保证后置条件。
除了每个操作中明确说明的先决条件和后置条件之外,规范还采用了以下约定,用于 运行时对象 (store, moduleinst, externval, 地址)
注意
只要嵌入器将运行时对象视为抽象,并且仅通过此处定义的接口创建和操作它们,所有隐式先决条件都会自动满足。
存储
store_init():store
-
返回空 存储。
模块
module_decode(byte∗):module ∣ error
module_parse(char∗):module ∣ error
module_validate(module):error?
module_instantiate(store,module,externval∗):(store,moduleinst ∣ error)
如果它成功地生成了一个 模块实例 moduleinst,则将 result 设置为 moduleinst.
否则,将 result 设置为 error.
-
返回新的 store 和 result 的组合。
注意
即使在发生错误的情况下,存储也可能会被修改。
module_imports(module):(name,name,externtype)∗
-
先决条件: module 是 有效的,其外部导入类型为 externtype∗,外部导出类型为 externtype′∗.
-
断言: import∗ 的长度等于 externtype∗.
-
对于每个 importi 在 import∗ 中以及相应的 externtypei 在 externtype∗ 中,执行以下操作:
令 resulti 为三元组 (importi.module,importi.name,externtypei).
-
返回所有 resulti 的连接,按索引顺序。
-
后置条件:每个 externtypei 是 有效的.
module_exports(module):(name,externtype)∗
-
先决条件: module 是 有效的,其外部导入类型为 externtype∗,外部导出类型为 externtype′∗.
-
断言:export∗ 的长度等于 externtype′∗ 的长度。
-
对于 exporti 中的每个 export∗ 以及 externtypei′ 中对应的 externtype′∗,进行以下操作:
令 resulti 为一对 (exporti.name,externtypei′).
-
返回所有 resulti 的连接,按索引顺序。
-
后置条件:每个 externtypei′ 都是 有效的。
模块实例
instance_export(moduleinst,name):externval ∣ error
-
断言:由于 模块实例 moduleinst 的 有效性,所有其 导出名称 都是不同的。
-
如果在 exportinsti 中存在一个 moduleinst.exports,使得 name exportinsti.name 等于 name,那么
-
返回 外部值 exportinsti.value.
-
-
否则,返回 error.
函数
func_alloc(store,functype,hostfunc):(store,funcaddr)
func_type(store,funcaddr):functype
func_invoke(store,funcaddr,val∗):(store,val∗ ∣ error)
-
返回新的 store 和 result 的组合。
注意
即使在发生错误的情况下,存储也可能会被修改。
表
table_alloc(store,tabletype,ref):(store,tableaddr)
table_type(store,tableaddr):tabletype
table_read(store,tableaddr,i:u32):ref ∣ error
table_write(store,tableaddr,i:u32,ref):store ∣ error
table_size(store,tableaddr):u32
table_grow(store,tableaddr,n:u32,ref):store ∣ error
内存
mem_alloc(store,memtype):(store,memaddr)
mem_type(store,memaddr):memtype
mem_read(store,memaddr,i:u32):byte ∣ error
mem_write(store,memaddr,i:u32,byte):store ∣ error
mem_size(store,memaddr):u32
mem_grow(store,memaddr,n:u32):store ∣ error
全局变量
global_alloc(store,globaltype,val):(store,globaladdr)
-
前提条件: globaltype 是 有效的.
-
令 globaladdr 为在 store 中 分配全局变量 的结果,使用 全局变量类型 globaltype 和初始化值 val.
-
返回与 globaladdr 配对的新存储。
global_type(store,globaladdr):globaltype
global_read(store,globaladdr):val
global_write(store,globaladdr,val):store ∣ error
A.2 实现限制
实现通常会对 WebAssembly 模块或执行的多个方面施加额外的限制。这些限制可能源于
-
物理资源限制,
-
嵌入器或其环境施加的约束,
-
所选实现策略的限制。
本节列出了允许的限制。如果限制采用数值限制的形式,则不会给出最小要求,也不会假设限制是具体的、固定的数字。但是,预计所有实现都具有“合理”的较大限制,以使常见应用程序能够正常运行。
注意
符合标准的实现不允许省略单个特性。但是,将来可能会指定 WebAssembly 的指定子集。
语法限制
结构
实现可能会对模块的以下维度施加限制
二进制格式
对于以 二进制格式 给出的模块,可能会对以下维度施加额外的限制
文本格式
对于以 文本格式 给出的模块,可能会对以下维度施加额外的限制
验证
实现可以延迟对单个 函数 的 验证,直到它们第一次被 调用。
如果一个函数被发现无效,那么调用以及对同一个函数的每次连续调用都会导致 陷阱。
注意
这是为了允许实现对函数使用解释或即时编译。在执行函数体之前,函数必须完全验证。
执行
在执行 WebAssembly 程序时,可能会对以下维度施加限制
-
已分配的 模块实例 的数量
-
已分配的 函数实例 的数量
-
已分配的 表格实例 的数量
-
已分配的 内存实例 的数量
-
已分配的 全局实例 的数量
-
表格实例 的大小
-
内存实例 的大小
-
堆栈上的 帧 的数量
-
堆栈上的 标签 的数量
-
堆栈上的 值 的数量
如果在执行计算过程中超过了实现的运行时限制,那么它可能会终止该计算,并向调用代码报告嵌入器特定的错误。
以上某些限制可能已在实例化期间得到验证,在这种情况下,实现可能会以与 语法限制 相同的方式报告超出限制。
注意
具体的限制通常不是固定的,但可能取决于细节,相互依赖,随时间变化,或取决于其他实现或嵌入器特定的情况或事件。
A.3 验证算法
WebAssembly 验证 的规范纯粹是声明式的。它描述了 模块 或 指令 序列必须满足的约束才能有效。
本节概述了有效验证代码(即 指令 序列)的算法的框架。(验证的其他方面很容易实现。)
事实上,该算法是在 二进制格式 中出现的操作码的扁平序列上表达的,并且只对其进行单次遍历。因此,它可以直接集成到解码器中。
该算法是用类型化伪代码表达的,其语义旨在不言自明。
数据结构
类型可以表示为枚举。
type val_type = I32 | I64 | F32 | F64 | V128 | Funcref | Externref
func is_num(t : val_type | Unknown) : bool =
return t = I32 || t = I64 || t = F32 || t = F64 || t = Unknown
func is_vec(t : val_type | Unknown) : bool =
return t = V128 || t = Unknown
func is_ref(t : val_type | Unknown) : bool =
return t = Funcref || t = Externref || t = Unknown
该算法使用两个独立的堆栈:值堆栈和控制堆栈。前者跟踪堆栈上操作数值的 类型,后者围绕 结构化控制指令 及其相关的 块。
type val_stack = stack(val_type | Unknown)
type ctrl_stack = stack(ctrl_frame)
type ctrl_frame = {
opcode : opcode
start_types : list(val_type)
end_types : list(val_type)
height : nat
unreachable : bool
}
对于每个值,值堆栈记录其 值类型,或者当类型未知时记录 Unknown
。
对于每个进入的块,控制堆栈记录一个控制帧,其中包含源操作码、块开始和结束时操作数堆栈顶部的类型(用于检查其结果以及分支)、块开始时操作数堆栈的高度(用于检查操作数是否未达到当前块的底部)、以及记录块的剩余部分是否不可到达的标志(用于处理分支后的 堆栈多态 类型)。
为了展示算法,操作数堆栈和控制堆栈只是作为全局变量维护的
var vals : val_stackvar ctrls : ctrl_stack
但是,这些变量不是由主检查函数直接操作的,而是通过一组辅助函数操作的
func push_val(type : val_type | Unknown) = vals.push(type)
func pop_val() : val_type | Unknown =
if (vals.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown
error_if(vals.size() = ctrls[0].height)
return vals.pop()
func pop_val(expect : val_type | Unknown) : val_type | Unknown =
let actual = pop_val()
error_if(actual =/= expect && actual =/= Unknown && expect =/= Unknown)
return actual
func push_vals(types : list(val_type)) = foreach (t in types) push_val(t)
func pop_vals(types : list(val_type)) : list(val_type) =
var popped := []
foreach (t in reverse(types)) popped.prepend(pop_val(t))
return popped
推送一个操作数值只是将相应的类型推送到值堆栈。
弹出操作数值会检查值堆栈是否未达到当前块的底部,然后删除一个类型。但首先,会处理一个特殊情况,即块不包含任何已知值,但已被标记为不可到达。这可能在无条件分支后发生,当堆栈以 多态 的方式进行类型化时。在这种情况下,将返回未知类型。
另一个弹出操作数值的函数接受一个预期类型,将实际操作数类型与之进行检查。如果其中一个类型是 Unknown,那么类型可能会不同。该函数返回从堆栈中弹出的实际类型。
最后,还有一些累积函数用于推送或弹出多个操作数类型。
注意
符号 stack[i]
表示从顶部索引堆栈,例如,ctrls[0]
访问最后推送的元素。
控制堆栈也通过辅助函数进行操作
func push_ctrl(opcode : opcode, in : list(val_type), out : list(val_type)) = let frame = ctrl_frame(opcode, in, out, vals.size(), false)
ctrls.push(frame)
push_vals(in)
func pop_ctrl() : ctrl_frame =
error_if(ctrls.is_empty())
let frame = ctrls[0]
pop_vals(frame.end_types)
error_if(vals.size() =/= frame.height)
ctrls.pop()
return frame
func label_types(frame : ctrl_frame) : list(val_types) =
return (if frame.opcode == loop then frame.start_types else frame.end_types)
func unreachable() =
vals.resize(ctrls[0].height)
ctrls[0].unreachable := true
推送控制帧会获取标签和结果值的类型。它分配一个新的帧记录来记录它们以及操作数堆栈的当前高度,并标记该块为可到达。
弹出帧首先检查控制堆栈是否为空。然后,它会验证操作数堆栈是否包含在退出块结束时预期的正确类型的值,并将它们从操作数堆栈中弹出。之后,它会检查堆栈是否缩回其初始高度。
与控制帧关联的 标签 的类型是帧开始或结束时堆栈的类型,由它起源的操作码决定。
最后,可以将当前帧标记为不可到达。在这种情况下,所有现有的操作数类型都会从值堆栈中清除,以便在 pop_val
中的 堆栈多态 逻辑生效。由于每个函数都有一个隐式最外层标签,对应于一个隐式块帧,因此验证算法的一个不变式是在验证指令时控制堆栈上始终至少存在一个帧,因此,ctrls[0] 始终定义。
操作码序列的验证
以下函数展示了对操作堆栈的几个代表性指令的验证。其他指令以类似的方式进行检查。
func validate(opcode) =switch (opcode)
case (i32.add)
pop_val(I32)
pop_val(I32)
push_val(I32)
case (drop)
pop_val()
case (select)
pop_val(I32)
let t1 = pop_val()
let t2 = pop_val()
error_if(not ((is_num(t1) && is_num(t2)) || (is_vec(t1) && is_vec(t2))))
error_if(t1 =/= t2 && t1 =/= Unknown && t2 =/= Unknown)
push_val(if (t1 = Unknown) t2 else t1)
case (select t)
pop_val(I32)
pop_val(t)
pop_val(t)
push_val(t)
case (unreachable)
unreachable()
case (block t1*->t2*)
pop_vals([t1*])
push_ctrl(block, [t1*], [t2*])
case (loop t1*->t2*)
pop_vals([t1*])
push_ctrl(loop, [t1*], [t2*])
case (if t1*->t2*)
pop_val(I32)
pop_vals([t1*])
push_ctrl(if, [t1*], [t2*])
case (end)
let frame = pop_ctrl()
push_vals(frame.end_types)
case (else)
let frame = pop_ctrl()
error_if(frame.opcode =/= if)
push_ctrl(else, frame.start_types, frame.end_types)
case (br n)
error_if(ctrls.size() < n)
pop_vals(label_types(ctrls[n]))
unreachable()
case (br_if n)
error_if(ctrls.size() < n)
pop_val(I32)
pop_vals(label_types(ctrls[n]))
push_vals(label_types(ctrls[n]))
case (br_table n* m)
pop_val(I32)
error_if(ctrls.size() < m)
let arity = label_types(ctrls[m]).size()
foreach (n in n*)
error_if(ctrls.size() < n)
error_if(label_types(ctrls[n]).size() =/= arity)
push_vals(pop_vals(label_types(ctrls[n])))
pop_vals(label_types(ctrls[m]))
unreachable()
注意
在当前 WebAssembly 指令集中,Unknown
类型的操作数永远不会在堆栈上被复制。如果该语言扩展了类似 dup
的堆栈指令,这种情况将会改变。在这样的扩展下,上述算法需要通过用适当的 *类型变量* 替换 Unknown
类型来进行细化,以确保所有使用都是一致的。
A.4 自定义节
本附录定义了 WebAssembly 的 二进制格式 中的专用 自定义节。这些节不会影响或改变 WebAssembly 语义,并且像任何自定义节一样,它们可以被实现忽略。但是,它们提供有用的元数据,实现可以使用这些元数据来改善用户体验或获取编译提示。
目前,只定义了一个专用自定义节,即 名称节。
名称节
名称节 是一个 自定义节,其名称字符串本身为 ‘name’. 名称节在模块中应该只出现一次,并且应该出现在 数据节 之后。
本节的目的是将可打印的名称附加到模块中的定义,例如,调试器或模块的某些部分需要以 文本形式 呈现时可以使用这些名称。
子节
名称节的 数据 由一系列 *子节* 组成。每个子节包含:
-
一个字节的子节 *标识符*,
-
以字节为单位的内容的u32大小,
-
实际的 *内容*,其结构取决于子节标识符。
使用以下子节标识符:
ID |
子节 |
---|---|
0 | |
1 | |
2 |
每个子节最多只能出现一次,并且按标识符递增的顺序排列。
名称映射
名称映射 将 名称 映射到给定 索引空间 中的 索引。它由一个 向量 组成,其中包含按索引值递增顺序排列的索引/名称对。每个索引必须是唯一的,但分配的名称不需要唯一。
间接名称映射将名称分配给二维的索引空间,其中次级索引按主索引进行分组。 它包含按升序索引值的向量形式的主索引/名称映射对,其中每个名称映射又将次级索引映射到名称。 每个主索引必须是唯一的,同样每个次级索引对于单个名称映射也是唯一的。
模块名称
模块名称小节的 ID 为 0。 它仅仅包含单个分配给模块本身的名称。
函数名称
函数名称小节的 ID 为 1。 它包含将函数名称分配给函数索引的名称映射。
局部名称
局部名称小节的 ID 为 2。 它包含将局部名称分配给按函数索引分组的局部索引的间接名称映射。
A.5 健壮性
WebAssembly 的类型系统是健壮的,这意味着它在 WebAssembly 语义方面既是类型安全的,又是内存安全的。 例如
-
在运行时,验证期间声明和推导的所有类型都将被遵守;例如,每个局部或全局变量将只包含类型正确的取值,每个指令只应用于预期类型的操作数,以及每个函数调用始终计算为正确类型的结果(如果它不会陷入或发散)。
-
除了由程序明确定义的内存位置外,不会读取或写入任何内存位置,即作为局部变量、全局变量、表格中的元素,或线性内存中的位置。
健全性也有助于确保其他属性,最值得注意的是函数和模块作用域的封装:任何局部变量都无法在其自身函数之外访问,任何模块组件都无法在其自身模块之外访问,除非它们被明确地导出或导入。
定义 WebAssembly 验证的类型规则仅涵盖 WebAssembly 程序的静态组件。为了准确地陈述和证明健全性,类型规则必须扩展到抽象运行时的动态组件,即存储、配置和管理指令。[1]
结果
结果 val∗
结果 trap
存储有效性
以下键入规则指定了运行时 存储 S 何时为有效。有效存储必须包含相对于 S 本身有效的 函数、表格、内存、全局 和 模块 实例。
为此,每种实例都由相应的 函数、表格、内存 或 全局 类型分类。模块实例由模块上下文分类,它们是将常规 上下文 重新用作模块类型,用于描述模块定义的 索引空间。
存储 S
-
每个 全局实例 globalinsti 在 S.globals 中必须与某个 全局类型 globaltypei 有效。
-
那么该存储就是有效的。
函数实例 {type functype,module moduleinst,code func}
宿主函数实例 {type functype,hostcode hf}
注意
这条规则表明,如果满足关于存储和参数的适当先决条件,那么执行宿主函数必须满足关于存储和结果的适当后置条件。这些后置条件与在 执行规则 中调用宿主函数的后置条件相匹配。
任何函数被调用的存储都被假定为当前存储的扩展。这样,函数本身就能够对未来存储做出足够的假设。
表实例 {type (limits t),elem ref∗}
内存实例 {type limits,data b∗}
全局实例 {type (mut t),value val}
元素实例 {type t,elem ref∗}
数据实例 {data b∗}
-
该数据实例是有效的。
导出实例 {name name,value externval}
-
该 外部值 externval 必须是 有效 的,并且其 外部类型 为 externtype.
-
然后,该导出实例将成为有效的导出实例。
模块实例 moduleinst
-
每个 函数类型 functypei 在 moduleinst.types 中必须是 有效的。
-
对于每个 函数地址 funcaddri 在 moduleinst.funcaddrs, 外部值 func funcaddri 必须是 有效的, 并具有某种 外部类型 func functypei′.
-
对于每个 表格地址 tableaddri 在 moduleinst.tableaddrs, 外部值 table tableaddri 必须是 有效的, 并具有某种 外部类型 table tabletypei.
-
对于每个 内存地址 memaddri 在 moduleinst.memaddrs, 外部值 mem memaddri 必须是 有效的, 并具有某种 外部类型 mem memtypei.
-
对于每个全局地址 globaladdri in moduleinst.globaladdrs, 外部值 global globaladdri 必须与某个外部类型 global globaltypei 有效。
-
对于每个元素地址 elemaddri in moduleinst.elemaddrs, 元素实例 S.elems[elemaddri] 必须与某个引用类型 reftypei 有效。
-
对于每个数据地址 dataaddri in moduleinst.dataaddrs, 数据实例 S.datas[dataaddri] 必须有效。
-
每个导出实例 exportinsti in moduleinst.exports 必须有效。
-
对于每个导出实例 exportinsti in moduleinst.exports, 名称 exportinsti.name 必须与moduleinst.exports 中出现的任何其他名称不同。
-
令 globaltype∗ 为所有 globaltypei 按顺序连接的结果。
-
令 m 为 moduleinst.funcaddrs 的长度。
-
令 n 为 moduleinst.dataaddrs 的长度。
-
令 x∗ 为从 0 到 m−1 的 函数索引 序列。
-
那么,模块实例在 上下文 {types functype∗, funcs functype′∗, tables tabletype∗, mems memtype∗, globals globaltype∗, elems reftype∗, datas okn, refs x∗} 中是有效的。
配置有效性
为了将 WebAssembly 的 类型系统 与其 执行语义 联系起来,必须将 指令的类型规则 扩展到 配置 S;T, 它将 存储 与执行 线程 相关联。
配置和线程按其结果类型进行分类。除了存储S外,线程还根据返回类型resulttype?进行类型化,该类型控制是否以及用哪种类型允许return指令。除了管理frame指令中的指令序列之外,此类型不存在(ϵ)。
最后,帧通过帧上下文进行分类,帧上下文扩展了帧关联的模块上下文的模块实例,包括帧包含的局部变量。
配置 S;T
线程 F;instr∗
-
设resulttype?为当前允许的返回类型。
-
设C′与C相同,但将return设置为resulttype?.
-
那么,该线程使用结果类型[t∗]是有效的。
Frames {locals val∗,module moduleinst}
-
模块实例 moduleinst 必须是 有效的,且具有某个 模块上下文 C.
-
令 t∗ 为所有 ti 的按顺序连接。
-
那么该帧是有效的,且具有 帧上下文 C′.
管理指令
对管理指令的类型规则如下所示。除了上下文 C之外,这些指令的类型还根据给定的存储 S定义。为此,所有之前的类型判断C⊢prop被推广为包含存储,如 S;C⊢prop,通过隐式地将S添加到所有规则中 - S从未被预先存在的规则修改,但它在下面给出的管理指令的额外规则中被访问。
trap
ref.extern externaddr
ref funcaddr
invoke funcaddr
labeln{instr0∗} instr∗ end
framen{F} instr∗ end
存储扩展
程序可以修改 存储 及其包含的实例。任何此类修改必须遵守某些不变性,例如不删除分配的实例或更改不可变定义。尽管这些不变性是 WebAssembly 指令 和 模块 的执行语义所固有的,但 宿主函数 并不会自动遵守它们。因此,必须将所需的变量声明为对 调用 宿主函数的显式约束。只有当 嵌入器 确保这些约束时,健壮性才成立。
必要的约束由存储扩展的概念来编码:当以下规则成立时,存储状态 S′ 扩展状态 S, 写作 S⪯S′.
注意
扩展并不意味着新存储有效,有效性是单独定义的 以上.
存储 S
-
S.funcs 的长度不得缩短。
-
S.tables 的长度不得缩短。
-
S.mems 的长度不得缩短。
-
S.globals 的长度不得缩短。
-
S.elems 的长度不得缩短。
-
S.datas 的长度不得缩短。
-
对于原始 globalinsti 中的每个 全局实例 S.globals, 新的全局实例必须是旧全局实例的 扩展。
函数实例 funcinst
-
函数实例必须保持不变。
表实例 tableinst
内存实例 meminst
全局实例 globalinst
-
的全局类型 globalinst.type 必须保持不变。
-
设 mut t 为 globalinst.type 的结构。
-
如果 const 为 const ,那么值 globalinst.value 必须保持不变。
元素实例 eleminst
数据实例 datainst
定理
根据 有效配置 的定义,标准的健全性定理成立。 [2] [3]
定理(保持性)。 如果一个 配置 S;T 是 有效的,其 结果类型 为 [t∗](即,⊢S;T:[t∗]),并且经过一系列步骤变为 S′;T′(即,S;T↪S′;T′),那么 S′;T′ 也是一个有效的配置,并且具有相同的结果类型(即,⊢S′;T′:[t∗])。此外,S′ 是 S 的 扩展(即,⊢S⪯S′)。
一个终止的 线程 是其 指令 序列为一个 结果 的线程。一个终止配置是其线程终止的配置。
定理(进展性)。 如果一个 配置 S;T 是 有效的(即,⊢S;T:[t∗] 对于一些 结果类型 [t∗]),那么它要么是终止的,要么可以经过一步变为某个配置 S′;T′(即,S;T↪S′;T′)。
从保持性和进展性可以直接得出 WebAssembly 类型系统的健全性。
推论(健全性)。如果一个 配置 S;T 是 有效的(即,⊢S;T:[t∗] 对于某个 结果类型 [t∗]),那么它要么会发散,要么会在有限步内到达一个终端配置 S′;T′(即,S;T↪∗S′;T′)是有效的,并具有相同的结果类型(即,⊢S′;T′:[t∗]),并且 S′ 是 S 的 扩展(即,⊢S⪯S′)。
换句话说,有效配置中的每个线程要么永远运行,要么陷入陷阱,要么以预期类型的结果终止。因此,给定一个 有效存储,由 实例化 或 调用 有效模块定义的计算不会“崩溃”,也不会以本规范中未涵盖的方式出现其他(错误)行为。
形式化和定理来自以下文章:Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. Bringing the Web up to Speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.
PLDI 2017 论文形式化和健全性证明的机器验证版本在以下文章中进行了描述:Conrad Watt. Mechanising and Verifying the WebAssembly Specification. Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2018). ACM 2018.
来自官方规范的语义的机器验证形式化和健全性证明在以下文章中进行了描述:Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner. Two Mechanisations of WebAssembly 1.0. Proceedings of the 24th International Symposium on Formal Methods (FM 2021). Springer 2021.
变更历史记录
自从 WebAssembly 规范最初发布 1.0 版以来,已经整合了许多扩展建议。以下部分概述了发生了哪些变化。
版本 2.0
符号扩展指令
添加了用于在整数表示中执行符号扩展的新数值指令 [1]。
非陷阱浮点数到整数转换
添加了新的转换指令,这些指令在将浮点数转换为整数时避免陷阱 [2]。
多值
将块和函数的结果类型推广以允许使用多值;此外,引入了具有块参数的能力 [3]。
引用类型
表格指令
新增直接访问和修改表格的指令 [4].
多个表格
新增了每个模块使用多个表格的功能 [4].
批量内存和表格指令
-
新增二进制格式中的 数据计数段
-
活动数据段和元素段边界不再在编译时检查,而是可能导致陷阱
向量指令
新增向量类型和指令,可并行处理多个数值(也称为 _SIMD_,单指令多数据) [6]
-
新增 内存指令:v128.load,v128.loadNxM_sx,v128.loadN_zero,v128.loadN_splat,v128.loadN_lane,v128.store,v128.storeN_lane
-
新增一元 向量指令: v128.not, iNxM.abs, iNxM.neg, i8x16.popcnt, fNxM.abs, fNxM.neg, fNxM.sqrt, fNxM.ceil, fNxM.floor, fNxM.trunc, fNxM.nearest
-
New binary vector instructions: v128.and, v128.andnot, v128.or, v128.xor, iNxM.add, iNxM.sub, iNxM.mul, iNxM.add_sat_sx, iNxM.sub_sat_sx, iNxM.min_sx, iNxM.max_sx, iNxM.shl, iNxM.shr_sx, fNxM.add, iNxM.extmul_half_iN′xM′_sx, i16x8.q15mulr_sat_s, i32x4.dot_i16x8_s, i16x8.extadd_pairwise_i8x16_sx, i32x4.extadd_pairwise_i16x8_sx, i8x16.avgr_u, i16x8.avgr_u, fNxM.sub, fNxM.mul, fNxM.div, fNxM.min, fNxM.max, fNxM.pmin, fNxM.pmax
-
新增三元 向量指令: v128.bitselect
-
新增测试 向量指令: v128.any_true, iNxM.all_true
-
新的关系型 向量指令:iNxM.eq, iNxM.ne, iNxM.lt_sx, iNxM.gt_sx, iNxM.le_sx, iNxM.ge_sx, fNxM.eq, fNxM.ne, fNxM.lt, fNxM.gt, fNxM.le, fNxM.ge
-
新的转换 向量指令:i32x4.trunc_sat_f32x4_sx, i32x4.trunc_sat_f64x2_sx_zero, f32x4.convert_i32x4_sx, f32x4.demote_f64x2_zero, f64x2.convert_low_i32x4_sx, f64x2.promote_low_f32x4
-
新的通道访问 向量指令:iNxM.extract_lane_sx?, iNxM.replace_lane, fNxM.extract_lane, fNxM.replace_lane
-
新的通道分割/合并 向量指令:iNxM.extend_half_iN′xM′_sx, i8x16.narrow_i16x8_sx, i16x8.narrow_i32x4_sx
-
新的字节重排序 向量指令: i8x16.shuffle, i8x16.swizzle
-
新的注入/投影 向量指令: iNxM.splat, fNxM.splat, iNxM.bitmask
https://github.com/WebAssembly/spec/tree/main/proposals/sign-extension-ops/
https://github.com/WebAssembly/spec/tree/main/proposals/nontrapping-float-to-int-conversion/
https://github.com/WebAssembly/spec/tree/main/proposals/multi-value/
https://github.com/WebAssembly/spec/tree/main/proposals/reference-types/
https://github.com/WebAssembly/spec/tree/main/proposals/bulk-memory-operations/
https://github.com/WebAssembly/spec/tree/main/proposals/simd/
A.6 类型索引
类别 |
构造函数 |
二进制操作码 |
---|---|---|
x | ||
0x7F (-1,作为 s7) | ||
0x7E (-2,作为 s7) | ||
0x7D (-3,作为 s7) | ||
0x7C (-4,作为 s7) | ||
0x7B (-5,作为 s7) | ||
(保留) |
0x7A .. 0x71 | |
0x70 (-16,作为 s7) | ||
0x6F (-17,作为 s7) | ||
(保留) |
0x6E .. 0x61 | |
0x60 (-32,作为 s7) | ||
(保留) |
0x5F .. 0x41 | |
[ϵ] |
0x40 (-64,作为 s7) | |
(无) | ||
(无) | ||
(无) |
A.7 指令索引
指令 |
二进制操作码 |
类型 |
验证 |
执行 |
---|---|---|---|---|
0x00 |
[t1∗]→[t2∗] | |||
0x01 |
[]→[] | |||
block bt |
0x02 |
[t1∗]→[t2∗] | ||
loop bt |
0x03 |
[t1∗]→[t2∗] | ||
if bt |
0x04 | |||
0x05 | ||||
(保留) |
0x06 | |||
(保留) |
0x07 | |||
(保留) |
0x08 | |||
(保留) |
0x09 | |||
(保留) |
0x0A | |||
0x0B | ||||
br l |
0x0C |
[t1∗ t∗]→[t2∗] | ||
br_if l |
0x0D | |||
br_table l∗ l |
0x0E | |||
0x0F |
[t1∗ t∗]→[t2∗] | |||
call x |
0x10 |
[t1∗]→[t2∗] | ||
call_indirect x y |
0x11 | |||
(保留) |
0x12 | |||
(保留) |
0x13 | |||
(保留) |
0x14 | |||
(保留) |
0x15 | |||
(保留) |
0x16 | |||
(保留) |
0x17 | |||
(保留) |
0x18 | |||
(保留) |
0x19 | |||
0x1A |
[t]→[] | |||
0x1B | ||||
select t |
0x1C | |||
(保留) |
0x1D | |||
(保留) |
0x1E | |||
(保留) |
0x1F | |||
0x20 |
[]→[t] | |||
0x21 |
[t]→[] | |||
0x22 |
[t]→[t] | |||
0x23 |
[]→[t] | |||
0x24 |
[t]→[] | |||
0x25 | ||||
0x26 | ||||
(保留) |
0x27 | |||
0x28 | ||||
0x29 | ||||
0x2A | ||||
0x2B | ||||
0x2C | ||||
0x2D | ||||
0x2E | ||||
0x2F | ||||
0x30 | ||||
0x31 | ||||
0x32 | ||||
0x33 | ||||
0x34 | ||||
0x35 | ||||
0x36 | ||||
0x37 | ||||
0x38 | ||||
0x39 | ||||
0x3A | ||||
0x3B | ||||
0x3C | ||||
0x3D | ||||
0x3E | ||||
0x3F | ||||
0x40 | ||||
0x41 | ||||
0x42 | ||||
0x43 | ||||
0x44 | ||||
0x45 | ||||
0x46 | ||||
0x47 | ||||
0x48 | ||||
0x49 | ||||
0x4A | ||||
0x4B | ||||
0x4C | ||||
0x4D | ||||
0x4E | ||||
0x4F | ||||
0x50 | ||||
0x51 | ||||
0x52 | ||||
0x53 | ||||
0x54 | ||||
0x55 | ||||
0x56 | ||||
0x57 | ||||
0x58 | ||||
0x59 | ||||
0x5A | ||||
0x5B | ||||
0x5C | ||||
0x5D | ||||
0x5E | ||||
0x5F | ||||
0x60 | ||||
0x61 | ||||
0x62 | ||||
0x63 | ||||
0x64 | ||||
0x65 | ||||
0x66 | ||||
0x67 | ||||
0x68 | ||||
0x69 | ||||
0x6A | ||||
0x6B | ||||
0x6C | ||||
0x6D | ||||
0x6E | ||||
0x6F | ||||
0x70 | ||||
0x71 | ||||
0x72 | ||||
0x73 | ||||
0x74 | ||||
0x75 | ||||
0x76 | ||||
0x77 | ||||
0x78 | ||||
0x79 | ||||
0x7A | ||||
0x7B | ||||
0x7C | ||||
0x7D | ||||
0x7E | ||||
0x7F | ||||
0x80 | ||||
0x81 | ||||
0x82 | ||||
0x83 | ||||
0x84 | ||||
0x85 | ||||
0x86 | ||||
0x87 | ||||
0x88 | ||||
0x89 | ||||
0x8A | ||||
0x8B | ||||
0x8C | ||||
0x8D | ||||
0x8E | ||||
0x8F | ||||
0x90 | ||||
0x91 | ||||
0x92 | ||||
0x93 | ||||
0x94 | ||||
0x95 | ||||
0x96 | ||||
0x97 | ||||
0x98 | ||||
0x99 | ||||
0x9A | ||||
0x9B | ||||
0x9C | ||||
0x9D | ||||
0x9E | ||||
0x9F | ||||
0xA0 | ||||
0xA1 | ||||
0xA2 | ||||
0xA3 | ||||
0xA4 | ||||
0xA5 | ||||
0xA6 | ||||
0xA7 | ||||
0xA8 | ||||
0xA9 | ||||
0xAA | ||||
0xAB | ||||
0xAC | ||||
0xAD | ||||
0xAE | ||||
0xAF | ||||
0xB0 | ||||
0xB1 | ||||
0xB2 | ||||
0xB3 | ||||
0xB4 | ||||
0xB5 | ||||
0xB6 | ||||
0xB7 | ||||
0xB8 | ||||
0xB9 | ||||
0xBA | ||||
0xBB | ||||
0xBC | ||||
0xBD | ||||
0xBE | ||||
0xBF | ||||
0xC0 | ||||
0xC1 | ||||
0xC2 | ||||
0xC3 | ||||
0xC4 | ||||
(保留) |
0xC5 | |||
(保留) |
0xC6 | |||
(保留) |
0xC7 | |||
(保留) |
0xC8 | |||
(保留) |
0xC9 | |||
(保留) |
0xCA | |||
(保留) |
0xCB | |||
(保留) |
0xCC | |||
(保留) |
0xCD | |||
(保留) |
0xCE | |||
(保留) |
0xCF | |||
ref.null t |
0xD0 |
[]→[t] | ||
0xD1 | ||||
ref.func x |
0xD2 | |||
(保留) |
0xD3 | |||
(保留) |
0xD4 | |||
(保留) |
0xD5 | |||
(保留) |
0xD6 | |||
(保留) |
0xD7 | |||
(保留) |
0xD8 | |||
(保留) |
0xD9 | |||
(保留) |
0xDA | |||
(保留) |
0xDB | |||
(保留) |
0xDC | |||
(保留) |
0xDD | |||
(保留) |
0xDE | |||
(保留) |
0xDF | |||
(保留) |
0xE0 | |||
(保留) |
0xE1 | |||
(保留) |
0xE2 | |||
(保留) |
0xE3 | |||
(保留) |
0xE4 | |||
(保留) |
0xE5 | |||
(保留) |
0xE6 | |||
(保留) |
0xE7 | |||
(保留) |
0xE8 | |||
(保留) |
0xE9 | |||
(保留) |
0xEA | |||
(保留) |
0xEB | |||
(保留) |
0xEC | |||
(保留) |
0xED | |||
(保留) |
0xEE | |||
(保留) |
0xEF | |||
(保留) |
0xF0 | |||
(保留) |
0xF1 | |||
(保留) |
0xF2 | |||
(保留) |
0xF3 | |||
(保留) |
0xF4 | |||
(保留) |
| |||
(保留) |
0xF6 | |||
(保留) |
0xF7 | |||
(保留) |
0xF8 | |||
(保留) |
0xF9 | |||
(保留) |
0xFA | |||
(保留) |
0xFB | |||
0xFC 0x00 | ||||
0xFC 0x01 | ||||
0xFC 0x02 | ||||
0xFC 0x03 | ||||
0xFC 0x04 | ||||
0xFC 0x05 | ||||
0xFC 0x06 | ||||
0xFC 0x07 | ||||
0xFC 0x08 | ||||
0xFC 0x09 |
[]→[] | |||
0xFC 0x0A | ||||
0xFC 0x0B | ||||
table.init x y |
0xFC 0x0C | |||
0xFC 0x0D |
[]→[] | |||
table.copy x y |
0xFC 0x0E | |||
0xFC 0x0F | ||||
0xFC 0x10 | ||||
0xFD 0x00 | ||||
0xFD 0x01 | ||||
0xFD 0x02 | ||||
0xFD 0x03 | ||||
0xFD 0x04 | ||||
0xFD 0x05 | ||||
0xFD 0x06 | ||||
0xFD 0x07 | ||||
0xFD 0x08 | ||||
0xFD 0x09 | ||||
0xFD 0x0A | ||||
0xFD 0x0B | ||||
0xFD 0x0C | ||||
0xFD 0x0D | ||||
0xFD 0x0E | ||||
0xFD 0x0F | ||||
0xFD 0x10 | ||||
0xFD 0x11 | ||||
0xFD 0x12 | ||||
0xFD 0x13 | ||||
0xFD 0x14 | ||||
0xFD 0x15 | ||||
0xFD 0x16 | ||||
0xFD 0x17 | ||||
0xFD 0x18 | ||||
0xFD 0x19 | ||||
0xFD 0x1A | ||||
0xFD 0x1B | ||||
0xFD 0x1C | ||||
0xFD 0x1D | ||||
0xFD 0x1E | ||||
0xFD 0x1F | ||||
0xFD 0x20 | ||||
0xFD 0x21 | ||||
0xFD 0x22 | ||||
0xFD 0x23 | ||||
0xFD 0x24 | ||||
0xFD 0x25 | ||||
0xFD 0x26 | ||||
0xFD 0x27 | ||||
0xFD 0x28 | ||||
0xFD 0x29 | ||||
0xFD 0x2A | ||||
0xFD 0x2B | ||||
0xFD 0x2C | ||||
0xFD 0x2D | ||||
0xFD 0x2E | ||||
0xFD 0x2F | ||||
0xFD 0x30 | ||||
0xFD 0x31 | ||||
0xFD 0x32 | ||||
0xFD 0x33 | ||||
0xFD 0x34 | ||||
0xFD 0x35 | ||||
0xFD 0x36 | ||||
0xFD 0x37 | ||||
0xFD 0x38 | ||||
0xFD 0x39 | ||||
0xFD 0x3A | ||||
0xFD 0x3B | ||||
0xFD 0x3C | ||||
0xFD 0x3D | ||||
0xFD 0x3E | ||||
0xFD 0x3F | ||||
0xFD 0x40 | ||||
0xFD 0x41 | ||||
0xFD 0x42 | ||||
0xFD 0x43 | ||||
0xFD 0x44 | ||||
0xFD 0x45 | ||||
0xFD 0x46 | ||||
0xFD 0x47 | ||||
0xFD 0x48 | ||||
0xFD 0x49 | ||||
0xFD 0x4A | ||||
0xFD 0x4B | ||||
0xFD 0x4C | ||||
0xFD 0x4D | ||||
0xFD 0x4E | ||||
0xFD 0x4F | ||||
0xFD 0x50 | ||||
0xFD 0x51 | ||||
0xFD 0x52 | ||||
0xFD 0x53 | ||||
0xFD 0x54 | ||||
0xFD 0x55 | ||||
0xFD 0x56 | ||||
0xFD 0x57 | ||||
0xFD 0x58 | ||||
0xFD 0x59 | ||||
0xFD 0x5A | ||||
0xFD 0x5B | ||||
0xFD 0x5C | ||||
0xFD 0x5D | ||||
0xFD 0x5E | ||||
0xFD 0x5F | ||||
0xFD 0x60 | ||||
0xFD 0x61 | ||||
0xFD 0x62 | ||||
0xFD 0x63 | ||||
0xFD 0x64 | ||||
0xFD 0x65 | ||||
0xFD 0x66 | ||||
0xFD 0x67 | ||||
0xFD 0x68 | ||||
0xFD 0x69 | ||||
0xFD 0x6A | ||||
0xFD 0x6B | ||||
0xFD 0x6C | ||||
0xFD 0x6D | ||||
0xFD 0x6E | ||||
0xFD 0x6F | ||||
0xFD 0x70 | ||||
0xFD 0x71 | ||||
0xFD 0x72 | ||||
0xFD 0x73 | ||||
0xFD 0x74 | ||||
0xFD 0x75 | ||||
0xFD 0x76 | ||||
0xFD 0x77 | ||||
0xFD 0x78 | ||||
0xFD 0x79 | ||||
0xFD 0x7A | ||||
0xFD 0x7B | ||||
i16x8.extadd_pairwise_i8x16_s |
0xFD 0x7C | |||
i16x8.extadd_pairwise_i8x16_u |
0xFD 0x7D | |||
i32x4.extadd_pairwise_i16x8_s |
0xFD 0x7E | |||
i32x4.extadd_pairwise_i16x8_u |
0xFD 0x7F | |||
0xFD 0x80 0x01 | ||||
0xFD 0x81 0x01 | ||||
0xFD 0x82 0x01 | ||||
0xFD 0x83 0x01 | ||||
0xFD 0x84 0x01 | ||||
0xFD 0x85 0x01 | ||||
0xFD 0x86 0x01 | ||||
0xFD 0x87 0x01 | ||||
0xFD 0x88 0x01 | ||||
0xFD 0x89 0x01 | ||||
0xFD 0x8A 0x01 | ||||
0xFD 0x8B 0x01 | ||||
0xFD 0x8C 0x01 | ||||
0xFD 0x8D 0x01 | ||||
0xFD 0x8E 0x01 | ||||
0xFD 0x8F 0x01 | ||||
0xFD 0x90 0x01 | ||||
0xFD 0x91 0x01 | ||||
0xFD 0x92 0x01 | ||||
0xFD 0x93 0x01 | ||||
0xFD 0x94 0x01 | ||||
0xFD 0x95 0x01 | ||||
0xFD 0x96 0x01 | ||||
0xFD 0x97 0x01 | ||||
0xFD 0x98 0x01 | ||||
0xFD 0x99 0x01 | ||||
0xFD 0x9B 0x01 | ||||
0xFD 0x9C 0x01 | ||||
0xFD 0x9D 0x01 | ||||
0xFD 0x9E 0x01 | ||||
0xFD 0x9F 0x01 | ||||
0xFD 0xA0 0x01 | ||||
0xFD 0xA1 0x01 | ||||
0xFD 0xA3 0x01 | ||||
0xFD 0xA4 0x01 | ||||
0xFD 0xA7 0x01 | ||||
0xFD 0xA8 0x01 | ||||
0xFD 0xA9 0x01 | ||||
0xFD 0xAA 0x01 | ||||
0xFD 0xAB 0x01 | ||||
0xFD 0xAC 0x01 | ||||
0xFD 0xAD 0x01 | ||||
0xFD 0xAE 0x01 | ||||
0xFD 0xB1 0x01 | ||||
0xFD 0xB5 0x01 | ||||
0xFD 0xB6 0x01 | ||||
0x | ||||
0xFD 0xB8 0x01 | ||||
0xFD 0xB9 0x01 | ||||
0xFD 0xBA 0x01 | ||||
0xFD 0xBC 0x01 | ||||
0xFD 0xBD 0x01 | ||||
0xFD 0xBE 0x01 | ||||
0xFD 0xBF 0x01 | ||||
0xFD 0xC0 0x01 | ||||
0xFD 0xC1 0x01 | ||||
0xFD 0xC3 0x01 | ||||
0xFD 0xC4 0x01 | ||||
0xFD 0xC7 0x01 | ||||
0xFD 0xC8 0x01 | ||||
0xFD 0xC9 0x01 | ||||
0xFD 0xCA 0x01 | ||||
0xFD 0xCB 0x01 | ||||
0xFD 0xCC 0x01 | ||||
0xFD 0xCD 0x01 | ||||
0xFD 0xCE 0x01 | ||||
0xFD 0xD1 0x01 | ||||
0xFD 0xD5 0x01 | ||||
0xFD 0xD6 0x01 | ||||
0xFD 0xD7 0x01 | ||||
0xFD 0xD8 0x01 | ||||
0xFD 0xD9 0x01 | ||||
0xFD 0xDA 0x01 | ||||
0xFD 0xDB 0x01 | ||||
0xFD 0xDC 0x01 | ||||
0xFD 0xDD 0x01 | ||||
0xFD 0xDE 0x01 | ||||
0xFD 0xDF 0x01 | ||||
0xFD 0xE0 0x01 | ||||
0xFD 0xE1 0x01 | ||||
0xFD 0xE3 0x01 | ||||
0xFD 0xE4 0x01 | ||||
0xFD 0xE5 0x01 | ||||
0xFD 0xE6 0x01 | ||||
0xFD 0xE7 0x01 | ||||
0xFD 0xE8 0x01 | ||||
0xFD 0xE9 0x01 | ||||
0xFD 0xEA 0x01 | ||||
0xFD 0xEB 0x01 | ||||
0xFD 0xEC 0x01 | ||||
0xFD 0xED 0x01 | ||||
0xFD 0xEF 0x01 | ||||
0xFD 0xF0 0x01 | ||||
0xFD 0xF1 0x01 | ||||
0xFD 0xF2 0x01 | ||||
0xFD 0xF3 0x01 | ||||
0xFD 0xF4 0x01 | ||||
0xFD 0xF5 0x01 | ||||
0xFD 0xF6 0x01 | ||||
0xFD 0xF7 0x01 | ||||
0xFD 0xF8 0x01 | ||||
0xFD 0xF9 0x01 | ||||
0xFD 0xFA 0x01 | ||||
0xFD 0xFB 0x01 | ||||
0xFD 0xFC 0x01 | ||||
0xFD 0xFD 0x01 | ||||
0xFD 0xFE 0x01 | ||||
0xFD 0xFF 0x01 |
注意
表中给出了多字节操作码的最短编码。但是,第一个字节后面的内容实际上是使用可变长度编码的u32,因此有多种可能的表示形式。
A.8 语义规则索引
静态结构的类型
结构 |
判断 |
---|---|
运行时结构类型
结构 |
判断 |
---|---|
S⊢exportinstok | |
S⊢moduleinst:C | |
常量性
结构 |
判断 |
---|---|
匹配
结构 |
判断 |
---|---|
存储扩展
结构 |
判断 |
---|---|
执行
结构 |
判断 |
---|---|
一致性
文档约定
一致性要求通过描述性断言和 RFC 2119 术语的组合来表达。本规范规范性部分中的关键词“MUST”、“MUST NOT”、“REQUIRED”、“SHALL”、“SHALL NOT”、“SHOULD”、“SHOULD NOT”、“RECOMMENDED”、“MAY”和“OPTIONAL”应按照 RFC 2119 中的描述进行解释。然而,为了易读性,这些词语在本规范中不全部使用大写字母。
本规范的所有文本均为规范性文本,除非明确标记为非规范性文本、示例或注释。[RFC2119]
本规范中的示例以“例如”开头,或与规范性文本分开设置,使用class="example"
,如下所示
信息性注释以“注释”开头,并与规范性文本分开设置,使用class="note"
,如下所示
注意,这是一条提示性说明。
符合标准的算法
算法中以命令式形式表述的要求(例如“去除任何前导空格”或“返回 false 并中止这些步骤”)应根据用于引入算法的关键词(“必须”,“应该”,“可以”等)的含义来解释。
以算法或具体步骤形式表述的符合性要求可以通过任何方式实现,只要最终结果等效即可。特别是,本规范中定义的算法旨在易于理解,并非旨在提高性能。鼓励实现者进行优化。
参考
规范性参考
- [IEEE-754-2019]
- IEEE 浮点数算术标准. 2008年8月29日. URL: http://ieeexplore.ieee.org/servlet/opac?punumber=4610933
- [RFC2119]
- S. Bradner. RFC 中用于指示要求级别的关键词. 1997年3月. 最佳实践. URL: https://datatracker.ietf.org/doc/html/rfc2119
- [UNICODE]
- Unicode 标准. URL: https://www.unicode.org/versions/latest/
6.2.4. 注释
一个注释可以是行注释,以双分号 ‘;;’ 开始并延伸到行尾,也可以是块注释,用分隔符 ‘(;’…‘;)’ 包裹起来。块注释可以嵌套。
这里,伪标记 eof 表示输入的结束。针对 blockchar 产生的规则中的 _前瞻_ 限制,消除了语法歧义,使得只有正确的方括号形式的块注释分隔符才被允许。
注意
任何格式化和控制字符都可以在注释中使用。