WebAssembly核心标准:WebAssembly Core Specification
细枝末节略,无关内容略。
简介
本文档介绍了WebAssembly核心标准的1.0版。WebAssembly是一种安全,可移植的低级代码格式,旨在有效执行和紧凑表达。
相关文档:核心WebAssembly规范,WebAssembly JS接口和WebAssembly Web API。
1. 引言
1.1. 引言
WebAssembly(缩写为Wasm)是一种安全,可移植的低级代码格式,旨在高效执行和紧凑表达。
它的主要目标是在Web上启用高性能应用程序,但是它没有做任何特定于Web的假设或提供特定于Web的功能,因此它也可以在其他环境中使用。
WebAssembly是W3C组织开发的开放标准。
本文档介绍了核心WebAssembly标准的1.0版。其未来将被替换为添加具有其他功能的新增量发行版。
1.1.1. 设计目标
WebAssembly的设计目标如下:
- 快速,安全和可移植的语义:
快速:利用几乎所有现代硬件共有的功能,以接近本机的代码性能执行。
安全:代码经过验证并在内存安全的[2]沙盒环境中执行,可防止数据损坏或安全漏洞。
定义明确:以易于非正式地和正式地进行推理的方式,全面而精确地定义有效的程序及其行为。
与硬件无关:可以在所有现代体系结构,台式机或移动设备以及嵌入式系统上进行编译。
与语言无关:不青睐任何特定的语言,编程模型或对象模型。
与平台无关:可以嵌入在浏览器中,作为独立VM运行或集成在其他环境中。
开放:程序可以通过简单通用的方式与其环境进行互操作。
- 高效便携的表示形式:
紧凑:具有比典型文本或本机代码格式小的传输速度快的二进制格式。
模块化:程序可以分成较小的部分,可以分别传输,缓存和使用。
高效:可以通过一次快速遍历进行解码,验证和编译,等同于即时(JIT)或提前(AOT)编译。
可流式传输:允许在看到所有数据之前尽快开始解码,验证和编译。
可并行化:允许将解码,验证和编译分为许多独立的并行任务。
可移植性:没有任何现代硬件无法广泛支持的架构假设。
WebAssembly代码还旨在易于检查和调试,尤其是在Web浏览器之类的环境中,但是此类功能超出了本规范的范围。
[1]“WebAssembly”的缩写,而不是首字母缩写,因此未使用大写字母。
[2]没有任何程序可以破坏WebAssembly的内存模型。当然,它不能保证编译为WebAssembly的不安全语言不会破坏其自身的内存布局,例如WebAssembly的线性内存中。
1.1.2. 作用域
WebAssembly的核心是一套虚拟指令集体系结构(虚拟ISA)。
因此,其具有许多用例,且可以嵌入许多不同的环境中。
为了涵盖它们的多样性并实现最大程度的重用,WebAssembly规范被拆分并分层为多个文档。
本文档与WebAssembly的核心ISA层有关。
它定义了指令集,二进制编码,验证和执行语义以及文本表示形式。
但是,它没有定义WebAssembly程序如何与它们在其中执行的特定环境交互,也没有定义如何从这样的环境中调用它们。
取而代之的是,此规范得到了其他文档的补充,这些文档定义了到特定嵌入环境(例如Web)的接口。
这些都将定义适合给定环境的WebAssembly应用程序编程接口(API)。
1.2. 安全性考量
WebAssembly不提供对执行代码的计算环境的环境访问。
与环境的任何交互(例如I/O,对资源的访问或操作系统调用)只能通过调用嵌入器提供的功能并将其导入WebAssembly模块中来执行。
嵌入程序可以通过控制或限制其可用于导入的功能来建立适用于相应环境的安全策略。
这些注意事项是嵌入程序的责任,也是特定环境的API定义的内容。
由于WebAssembly旨在转换为直接在主机硬件上运行的机器代码,因此可能会在硬件级别受到旁通道攻击。
在这是一个潜在的脆弱的环境中,嵌入程序可能必须设置适当的缓解措施以隔离WebAssembly计算。
1.2.1. 依赖
WebAssembly依赖于两个现有标准:
- [IEEE-754-2019],用于表示浮点数据和相应数字运算的语义。
- [UNICODE],用于表示导入/导出名称和文本格式。
但是,为了使本规范变得独立,将上述标准的相关方面定义并正式化为本规范的一部分,例如二进制表示和浮点值的取整,以及Unicode的值范围和UTF-8编码字符。
注意!
前述标准是所有各个定义的权威来源。本规范中给出的形式化旨在与这些定义匹配。所描述的语法或语义上的任何差异均应视为错误。
1.3. 概览
1.3.1 概念
WebAssembly编码一种低级的,类似于程序集的编程语言。该语言围绕以下概念构建。
值Values
WebAssembly仅提供四种基本值类型。这些是整数和IEEE-754-2019数字,分别为32位和64位宽度。32位整数还用作布尔值和内存地址。可以使用这些类型的常规操作,包括它们之间转换的完整矩阵。有符号和无符号整数类型之间没有区别。取而代之的是,整数会被相应的操作解释为无符号或有两个补码表示形式的符号。
指令Instructions
WebAssembly的计算模型基于堆栈计算机 。代码由按顺序执行的指令序列组成。指令在隐式操作数堆栈[1]上操作值,并分为两个主要类别。简单的指令对数据执行基本操作。它们从操作数堆栈中弹出参数,并将结果压回该操作数堆栈。控制指令会改变控制流程。控制流是结构化的,这意味着它可以用嵌套好的结构(例如块,循环和条件)来表示。分支只能针对此类构造。
陷阱Traps
w在某些情况下,某些指令可能会产生陷阱,该陷阱会立即中止执行。陷阱不能由WebAssembly代码处理,但是会报告给外部环境,通常可以在外部环境中捕获它们。
功能Functions
代码被组织成单独的功能。每个函数都将值序列作为参数,并返回值序列作为结果。 [2]函数可以互相调用,包括递归调用,从而导致无法直接访问的隐式调用堆栈。函数还可以声明可用作虚拟寄存器的可变局部变量。
表Tables
表是特定元素类型的不透明值的数组。它允许程序通过动态索引操作数间接选择这些值。当前,唯一可用的元素类型是无类型的函数引用。因此,程序可以通过向表中的动态索引间接调用函数。例如,这允许通过表索引模拟功能指针。
线性内存Linear Memory
线性内存是连续,可变的原始字节数组。这样的存储器以初始大小创建,但是可以动态增长。程序可以在任何字节地址(包括未对齐)将线性存储器中的值加载/存储在线性存储器中或将其存储在其中。整数加载和存储可以指定小于各自值类型的大小的存储大小。如果访问不在当前内存大小的范围内,则会发生陷阱。
模块Modules
WebAssembly二进制文件采用模块的形式,该模块包含函数,表和线性内存的定义以及可变或不可变的全局变量。也可以导入定义,指定模块/名称对和合适的类型。每个定义可以选择以一个或多个名称导出。除定义外,模块还可以为其内存或表定义初始化数据,该初始化数据采用复制到给定偏移量的段的形式。他们还可以定义自动执行的启动功能。
嵌入器Embedder
WebAssembly实现通常将嵌入到主机环境中。此环境定义了如何启动模块加载,如何提供导入(包括主机端定义)以及如何访问导出。但是,任何特定嵌入的细节都超出了本规范的范围,而是由互补的,特定于环境的API定义提供。
[1]实际上,实现无需维护实际的操作数堆栈。取而代之的是,堆栈可以看作是一组由指令隐式引用的匿名寄存器。类型系统可确保始终静态地了解堆栈高度,从而确保所有引用的寄存器。
[2]在当前版本的WebAssembly中,最多只有一个结果值。
1.3.2. 语义解析
从概念上讲,WebAssembly的语义分为三个阶段。对于语言的每个部分,规范都会对其进行指定。
解码Decoding
WebAssembly模块以二进制格式分发。解码过程将格式化并将其转换为模块的内部表示形式。在本规范中,此表示是通过抽象语法建模的,但是实际的实现可以改为直接编译为机器代码。
验证Validation
被解码的模块必须有效。验证检查许多格式正确的条件,以确保模块有意义且安全。特别是,它对功能及其内部的指令序列进行类型检查,以确保例如一致地使用操作数堆栈。
执行Execution
最后,一个有效的模块可以被执行。执行可以进一步分为两个阶段:
实例化Instantiation。模块实例是模块的动态表示,带有其自己的状态和执行堆栈。实例化将执行模块主体本身,并为其定义所有导入。它将初始化全局变量,内存和表,并调用模块的启动函数(如果已定义)。它返回模块导出的实例。
调用Invocation。一旦实例化,就可以通过在模块实例上调用导出的函数来启动进一步的WebAssembly计算。给定必需的参数,该函数将执行相应的函数并返回其结果。
实例化和调用是在嵌入环境中的操作。
2. 架构
2.1. 规定
WebAssembly是一种编程语言,具有多种具体表示形式(其二进制格式和文本格式)。 两者都映射到一个共同的结构。为简明起见,以抽象语法的形式描述了此结构。本规范的所有部分均根据此抽象语法定义。
2.1.1. 语法符号
在定义抽象语法的语法规则时采用以下约定。
- 结束符号(原子)以sans-serif字体编写。
- 非结束符以斜体字体表示:。
- 是A的个迭代的序列。
- 是A的可能是空的迭代序列。(这是n无关的的简写。)
- 是A的非空迭代序列。(这是的简写,其中n≥1。)
- 是A的可选出现。(这是的简写,其中n≤1。)
- 产生式被写成。
- 大型产生式可能会分为多个定义,可以用第一个以显式椭圆结束,并以椭圆以开头来表示。
- 一些产品在括号中加上附加条件“”,这为将产品组合扩展为许多单独的案例提供了捷径。
2.1.2. 辅助符号
在处理语法结构时,还使用以下表示法:
- 表示空序列。
- 表示序列s的长度。
- 表示序列s的第i个元素,从0开始。
- 表示序列s的子序列。
- 表示与s相同的序列,除了第i个元素被A代替。
- 表示与s相同的序列,不同之处在于子序列被An取代。
- 表示通过将中的所有序列串联而形成的平坦序列。
此外,采用以下约定:
-
符号(其中x是非终结符号)被视为跨x的各个序列(类似于,,)的元变量。
-
当给定一个序列时,则假定在中写入的序列中x的出现与xn呈逐点对应关系(对于,,同样)。这隐式表达了在序列上映射语法结构的形式。
以下形式的生产被解释为分别将一组固定的字段映射到“值” Ai的记录:
使用以下表示法来处理此类记录:
-
表示r的字段filed的内容。
-
表示与r相同的记录,除了字段组件的内容被A代替。
-
通过逐点追加每个序列来表示具有相同序列字段的两个记录的组合:
- 分别表示记录序列的组成;如果序列为空,则结果记录的所有字段均为空。
序列和记录的更新符号递归地概括为“路径” 所访问的嵌套组件:
- 是的缩写。
- 是的缩写。
其中缩写为
2.1.3. 向量
向量是形式为(或)的有界序列,其中A可以是值或复杂的构造。一个向量最多可包含(即MaxUint256)个元素。
2.2. 值
WebAssembly程序对原始数值进行操作。
此外,在程序的定义中,值的不可变序列出现以表示更复杂的数据,例如文本字符串或其他向量。
2.2.1. Bytes
值的最简单形式是未解释的原始字节。
在抽象语法中,它们表示为十六进制文字。
2.2.1.1. 惯例
-
元变量的范围为字节。
-
字节有时被解释为自然数。
2.2.2. 整数
具有不同值范围的不同类别的整数通过其位宽以及是无符号还是有符号来区分。
后者定义了未解释的整数,其有符号性解释会根据上下文而变化。
在抽象语法中,它们表示为无符号值。
但是,某些运算会根据二进制补码解释将其转换为带符号。
注意
在本规范中出现的主要整数类型是u32,u64,s32,s64,i8,i16,i32,i64。但是,例如在浮点数的定义中,其他大小也可以作为辅助结构。
2.2.2.1. 惯例
- 元变量的范围是整数。
- 如上面的语法所示,数字可以用简单的算术表示。
为了区分之类的算术与之类的序列,用括号将后者区分。
2.2.3. 浮点数
浮点数据表示32或64位值,它们对应于[IEEE-754-2019]标准(第3.3节)的相应二进制格式。
每个值都有一个符号和大小。 幅值可以表示为形式为的正态数,其中是指数,m是其最高位为1的有效数,或者以次正规数来表示 指数固定为最小可能值,且为0; 在次法线中的是零正值和负值。 由于有效位数是二进制值,因此法线以的形式表示,其中是的位宽; 对于次普通人也是如此。
可能的大小还包括特殊值(无穷大)和nan(即NaN,非数字)。NaN值具有一个有效载荷,该载荷描述了基础二进制表示形式中的尾数位。 信号和安静的NaN之间没有区别。
\displaylines{fNmag ::=(1+uM\cdot 2^{-M})\cdot 2^e ((if\ −2^{E−1} + 2 \leq e \leq 2^{E−1}−1))\\ |\ (0+uM\cdot 2^{-M})\cdot 2^e (if\ e=-2^{E-1}+2)\\ \infty\\ nan(n)\ (if 1\leq n\lt 2^M)}
当 M=signif(N) 且 E=expon(N) 则
\displaylines{signif(32) = 23 \\ expon(32) =8 \\ signif(64)=52\\ expon(64)=11}
一个*规范的(canonical)*NaN是浮点数值,其中是有效载荷,其最高有效位为1而所有其他均为0:
一个*算术(arithmetic)*NaN是的浮点值,因此最高有效位为1,其他所有位均为任意。
注意
在抽象语法中,子范数以有效数字的前导0区分。 次正态的指数与正态数的最小可能指数具有相同的值。 仅在二进制表示中,次正态的指数与任何正态数的指数的编码方式不同。
2.2.3.1. 惯例
- 元变量z取自从上下文清晰可辨的浮点值。
2.2.4. 名称Names
名称是字符序列,是[UNICODE](第2.4节)定义的标量值。
\displaylines{name::= char^* \ (if\ |utf8(char^*)|<2^{32})\\ char ::= U+00|\ldots|U+D7FF|U+E000|...U+10FFFF}
由于二进制格式的限制,名称的长度受其UTF-8编码的长度限制。
2.2.4.1. 惯例
- 字符(Unicode标量值)有时与n <1114112的自然数互换使用。
2.3 类型Types
WebAssembly中的各种实体按类型分类。
在验证,实例化以及可能的执行期间检查类型。
2.3.1 值(Value)类型
值类型对WebAssembly代码可以计算的单个值以及变量接受的值进行分类。
i32和i64类型分别将32位和64位整数分类。
整数不是固有地带符号或无符号的,它们的解释由单个操作确定。
f32和f64类型分别将32位和64位浮点数分类。
它们分别对应于[IEEE-754-2019]标准(第3.3节)定义的相应二进制浮点表示形式,也称为单精度和双精度。
2.3.3.1. 惯例
- 元变量t可以从清晰的上下文中范围内的值类型。
- 符号表示值类型的位宽。即,和。
2.3.2. 结果(Result)类型
结果类型对执行指令或块的结果进行分类,该指令或块是用括号写入的一系列值。
注意
在当前版本的WebAssembly中,结果最多允许一个值。但是,这可能会泛化为将来版本中的值序列。
2.3.3 函数(Function)类型
函数类型对函数的签名进行分类,将参数向量映射到结果向量,如下所示。
注意
在当前版本的WebAssembly中,有效函数类型的结果类型向量的长度最多为1。此限制在将来的版本中可能会消除。
2.3.4. 限制
限制对与内存类型和表类型关联的可调整大小的存储的大小范围进行分类。
如果没有给出最大值,则相应的存储可以增长到任何大小。
2.3.5. 内存(Memories)类型
存储器类型将线性存储器及其大小范围分类。
这些限制限制了内存的最小和最大可选大小。 限制以页面大小为单位给出。
2.3.6. 表格类型
表类型根据大小范围内的元素类型的元素对表进行分类。
\displaylines{tabletype ::= limits elemtype\\ elemtype::=funcref}
像内存一样,表格的最小和最大大小限制也受到限制。
限制以条目数给出。
元素类型funcref是所有函数类型的无限并集。
因此,该类型的表包含对异构类型函数的引用。
注意
在WebAssembly的未来版本中,可能会引入其他元素类型。
2.3.7. 全局变量类型
全局变量类型对全局变量进行分类,这些全局变量具有一个值,并且可以是可变的或不可变的。
\displaylines{globaltype ::= mut valtype\\mut ::= const | var} #### 2.3.8. 外部类型 外部类型使用各自的类型对导入和外部值进行分类。 $$ externtype :: = func functype| table tabletype | mem memtype | global globaltype
2.3.8.1 惯例
为外部类型的序列定义了以下辅助符号。
它以保留顺序的方式筛选出特定种类的条目:
\displaylines{funcs(externtype^*)=[functype|(func functype) \in externtype^*] \\ tables(externtype^*)=[tabletype | (table tabletype)\in externtype^*] \\ mems(externtype^*)=[memtype | (mem memtype)\in externtype^*] \\ globals(externtype^*)=[globaltype | (global globaltype)\in externtype^*]}
2.4. 指令Instructions
WebAssembly代码由指令序列组成。 它的计算模型基于堆栈机,其中指令在隐式操作数堆栈上操纵值,使用(弹出)自变量值并生成或返回(推入)结果值。
注意
在当前版本的WebAssembly中,单个指令最多可以推入一个结果值。在将来的版本中可能会取消此限制。
除了来自堆栈的动态操作数之外,某些指令还具有静态中间参数,通常是索引或类型注释,它们是指令本身的一部分。
某些指令的结构在于将嵌套的指令序列括起来。
以下各节将指令分为许多不同的类别。
2.4.1. 数值指令
数值指令提供对特定类型数值的基本操作。
这些操作与硬件中可用的各个操作紧密匹配。
\displaylines{instr ::= \mathrm{i} nn.\mathrm{const}\ inn | \mathrm{i}nn.\mathrm{const}\ fnn \\ | \mathrm{i}nn.iunop | \mathrm{f}nn.funop \\ | \mathrm{i}nn.ibinop | \mathrm{f}nn.fbinop \\ | \mathrm{i}nn.itestop \\ | \mathrm{i}nn.irelop | \mathrm{f}nn.frelop \\ | \mathrm{i32.wrap\_i64} | \mathrm{i64.extend\_i32\_}sx | \mathrm{i}nn.\mathrm{trunc\_f}mm\_sx \\ | \mathrm{f32.demote\_f64} | \mathrm{f64.promote\_f32} | \mathrm{f}nn.\mathrm{convert\_i}mm\_sx \\ | \mathrm{i}nn.\mathrm{reinterpret\_f}nn | \mathrm{i}nn.\mathrm{reinterpret\_i}nn \\ | \ldots}
\displaylines{ibinop ::= \mathrm{add | sub | mul | div\_}sx \mathrm{|rem\_}sx \\ | \mathrm{and | or | xor | shl | shr\_}sx \mathrm{| rtol | rtor} }
数字指令按值类型划分。 对于每种类型,可以区分几个子类别:
- 常量:返回静态常量。
- 一元运算符:使用一个操作数并产生相应类型的一个结果。
- 二进制运算符:使用两个操作数并产生一个相应类型的结果。
- 测试:消耗一个相应类型的操作数,并产生一个布尔整数结果。
- 比较:消耗两个各自类型的操作数,并产生一个布尔整数结果。
- 转换:使用一种类型的值并产生另一种类型的结果(转换的源类型是“_”之后的类型)。
一些整数指令有两种形式,其中带符号注释sx区分是将操作数解释为无符号整数还是带符号整数。
对于其他整数指令,对有符号的解释使用二进制补码意味着无论有符号性如何,它们的行为都相同。
2.4.1.1. 惯例
有时,根据以下语法速记将操作分组在一起很方便:
2.4.2. 参数指令
该组中的指令可以对任何值类型的操作数进行运算。
\displaylines{ instr ::= \ldots \\ | \mathrm{drop} \\ | \mathrm{select} }
drop运算符只是丢掉单个操作数。
select运算符根据其第三个操作数是否为零来选择执行其前两个操作数之一。
2.4.3. 变量指令
变量指令涉及对局部或全局变量的访问。
\displaylines{ instr ::= \ldots \\ | \mathrm{local.get}\ localidx \\ | \mathrm{local.set}\ localidx \\ | \mathrm{local.tee}\ localidx \\ | \mathrm{global.get}\ globalidx \\ | \mathrm{global.set}\ globalidx}
这些指令分别获取或设置变量的值。
local.tee指令类似于local.set,但会返回其参数。
2.4.4. 内存指令
该组指令与线性内存有关。
内存可以通过使用不同值类型的加载(load)和存储(store)指令来访问。
它们都使用一个内存中间值memarg,该值包含一个地址偏移量(offset)和一个预期的编排方式(表示为2的幂的指数)。
整数的加载和存储可以选择指定小于各自值类型的位宽度的存储大小。
在一些加载情况下,则需要符号扩展模式来选择适当的行为。
静态地址偏移量被添加到动态地址操作数,从而产生33位长度的有效地址,该地址是从零开始的索引,可从该索引访问内存。
所有值以Little-Endian读取和写入。
如果任何已访问的内存字节超出了内存当前大小所隐含的地址范围,就会产生陷阱(Trap)。
注意
WebAssembly的未来版本可能会提供具有64位地址范围的内存指令。
(这也是为啥现在叫wasm32)
memory.size指令返回当前的内存大小。
memory.grow指令将内存增加给定的增量,并返回先前的大小;如果无法分配足够的内存,则返回-1。
两条指令均以页面大小为单位。
注意
在当前版本的WebAssembly中,所有内存指令都隐式地(默认)对内存索引0进行操作。此限制在将来的版本中可能会取消。
2.4.5. 控制指令
该组中的指令会影响控制流程。
\displaylines{ instr ::= \ldots \\ | \mathrm{nop} \\ | \mathrm{unreachable} \\ | \mathrm{block}\ resulttype\ instr^*\ \mathrm{end} \\ | \mathrm{loop }\ resulttype\ instr^*\ \mathrm{end} \\ | \mathrm{if}\ resulttype\ instr^*\ \mathrm{else}\ instr^*\ \mathrm{end} \\ | \mathrm{br}\ labelidx \\ | \mathrm{br\_if}\ labelidx \\ | \mathrm{br\_table}\ vec(labelidx)\ labelidx \\ | \mathrm{return} \\ | \mathrm{call}\ funcidx \\ | \mathrm{call\_indirect}\ typeidx}
nop指令不执行任何操作。
unreachable指令触发无条件的陷阱。
block,loop以及if指令是结构化指令。
它们将嵌套的指令序列(称为块)括起来,以指令末尾或伪指令终止或分隔。
正如语法规定的那样,必须将它们嵌套好。
结构化指令可以产生一个如注释结果类型描述的值。
每个结构化控制指令都会引入一个隐式标签。
标签(Label)是分支指令通过标签索引引用的目标。
与其他索引空间不同,标签的索引是相对于嵌套深度的,也就是说,标签0指的是包围引用分支指令的最内部结构化控制指令,而递增的索引则引用更远的索引。
因此,只能从关联的结构化控制指令中引用标签。
这也意味着分支只能指向外部,“脱离”它们所针对的控制构造的块。
具体效果取决于该控制结构:
在block或if情况下,向前跳转直到匹配到end后恢复执行。
在loop循环情况下,向后跳到loop开始。
注意
这将强制执行结构化的控制流程。
直观地讲,在大多数类似于C的语言中,针对块的if分支的行为类似于break语句,而针对循环的分支的行为类似于continue语句。
分支(Branch)指令有以下几种形式:
br:执行无条件分支
br_if:执行条件分支
br_table:通过操作数索引到标签向量的间接操作来执行该间接操作,该标签向量是指令的直接执行对象,如果操作数超出范围,则指向默认目标。
return:无条件分支到最外层代码块的快捷方式,该块隐式地是当前函数的主体。
采取分支将操作数堆栈展开到输入目标结构化控制指令的高度。
但是,以非空结果类型为目标的控制指令作为目标的前向分支首先消耗匹配的操作数,并在展开后将它们推回操作数堆栈中,以作为终止的结构化指令的结果。
call指令调用另一个函数,从堆栈中使用必要的参数并返回调用的结果值。
call_indirect指令通过将操作数索引到表中来间接调用函数。
由于表(table)可能包含异构类型funcref的函数元素,因此将根据指令的立即数对被调用方进行动态检查,以检查该函数类型(function type),如果调用不匹配,则调用将使用陷阱(trap)中止。
注意
在当前版本的WebAssembly中,call_indirect默认对表索引(tableidx)0操作。在将来的版本中可能会取消此限制。
2.4.6. 表达式Expression
函数(function)主体,全局变量(globals)的初始化值以及元素(element)或数据(data)段的偏移量都作为表达式给出。表达式是由结束(end)标记终止的指令(instruction)序列。
在某些地方,验证器将表达式限制为常量,从而限制了被允许的指令集。
2.5 模块 Modules
WebAssembly程序被组织成模块,这些模块是部署,加载和编译的单元。
一个模块包含了类型(types),函数(functions),表(tables),内存(memories)和全局变量(globals)的定义。
此外,它可以声明导入(imports)和导出(exports),并以数据(data)和元素(element)段或启动函数的形式提供初始化逻辑。
\displaylines{ module ::= \{ types\ vec(functype), funcs\ vec(func), \\ tables\ vec(table), \\ mems vec(mem), \\ globals\ vec(elem), \\ data\ vec(data), \\ start\ start^?, \\ imports\ vec(import), exports\ vec(export) \}}
每个向量,甚至整个模块,都可能是空的。
2.5.1. 索引
定义被以从0开始的索引引用。
每个定义类都有其自己专属的索引空间,如以下类所示。
\displaylines{ typeidx ::= u32\\ funcidx ::= u32\\ tableidx ::= u32\\ memidx ::= u32\\ globalidx ::= u32\\ localidx ::= u32\\ labelidx ::= u32}
函数(functions),表(tables),内存(memories)和全局变量(globals)的索引空间包括在同一模块中声明的相应导入(imports)中。
这些导入(imports)的索引在同一索引空间中优先于其他定义的索引。
局部变量(locals)的索引空间只能在函数内部访问,并且包括以此为参数的函数。这种函数位于局部变量之前。
标签(label)索引引用指令序列内的结构化控制指令。
2.5.1.1. 惯例
- 元变量l覆盖标签索引。
- 元变量x,y覆盖其他任何索引空间中的索引。
2.5.2. 类型
模块的类型组件定义了一个功能类型(function types)的向量。
所有功能类型必须在此组件中定义模块中使用。
它们由类型索引引用。
注意
WebAssembly的未来版本可能会添加类型定义的其他形式。
2.5.3. 函数
模块的funcs组件定义具有以下结构的函数向量:
函数(function)的类型通过引用模块中定义的类型来声明其签名。
该函数的参数通过函数主体中从0的局部索引进行引用; 他们是可变的。
局部变量(locals)声明一个可变局部变量及其类型的向量。
这些变量是通过函数体内的局部索引来引用的。
第一个局部变量的索引是最小索引,其不引用任何参数。
主体(body)是一个指令序列,在终止时必须产生一个与函数类型的结果类型(result type)匹配的堆栈。
函数通过函数索引被引用,由最小索引开始,不引用任何函数导入(function import)。
2.5.4. 表
模块的表组件定义了由表类型描述的一个表向量:
表是特定表元素类型的不透明值的向量。
表类型的限制中的最小的大小指定了该表的初始大小。
而如果存在最大则其大小限制该表稍后可以增长至的大小。
可以通过元素段(element segment)初始化表。
通过表索引引用表,从最小索引开始,不需要引用一个表导入(table import)。
大多数构造都隐式引用表索引0。
注意
在当前版本的WebAssembly中,最多可以在一个模块中定义或导入一个表,并且所有构造都隐式引用表0。此限制在将来的版本中可能会取消。
2.5.5. 内存
模块的内存(mems)组件定义了一个线性存储器(或简称为存储器)的向量,如其存储器类型所述:
内存是未被解释的原始字节的向量。
内存类型的限制中的最小(Min)大小指定该内存的初始大小,而最大内存大小(Max,如果存在)则限制了以后可以增长的大小。
两者均以页面大小为单位。
可以通过数据段(data segment)初始化内存。
内存被内存索引引用,从最小索引开始,不引用内存导入(memory import)。
大多数构造都隐式引用内存索引0。
注意
在当前版本的WebAssembly中,最多可以在一个模块中定义或导入一个内存,并且所有构造都隐式引用此内存0。此限制在将来的版本中可能会取消。
(换句话说现在的mems根本就是个单元素数组,里面就一个memory)
2.5.6. 全局变量Globals
模块的全局变量组件定义了一个全局变量的向量(或简称为globals):
每个全局变量都存储给定全局变量类型(global type)的单个值。
它的类型还指定了全局变量是不可变的还是可变的。
此外,每个全局变量都使用常量初始化表达式(expr)给出的初始化值进行初始化。
全局变量通过全局索引引用,从最小的索引开始,不引用全局导入。
2.5.7. 元素段 Element Segments
表的初始内容未初始化。
模块的elem组件定义元素段的向量,这些向量以给定的偏移量从元素的静态向量初始化表的子范围。
偏移量(offset)由一个常量表达式给出。
注意
在当前版本的WebAssembly中,模块中最多允许一个表。因此,唯一有效的tableidx为0。
2.5.8. 数据段 Data Segments
内存的初始内容为一堆零值字节。
模块的数据组件定义数据段的向量,这些数据段以给定的偏移量和静态字节向量来初始化内存范围。
偏移量(offset)由一个常量表达式给出。
注意
在当前版本的WebAssembly中,一个模块中最多允许有一个内存。 因此,唯一有效的memidx为0。
2.5.9. 启动函数 Start Function
模块的启动(start)组件声明一个启动函数的函数索引,该函数在初始化表和内存后在实例化模块时自动调用。
注意
启动功能用于初始化模块的状态。在初始化完成之前,无法访问模块及其导出(exports)。
2.5.10. 导出 exports
模块的导出组件定义了一组导出。一旦实例化该模块,主机环境就可以访问它们。
\displaylines{ exportdesc ::= \mathrm{func}\ funcidx\\ | \mathrm{table}\ tableidx\\ | \mathrm{mem}\ memidx\\ | \mathrm{global}\ globalidx}
每个导出都用唯一的名称标记。
可导出的定义是函数,表,内存和全局变量,它们通过相应的描述符进行引用。
2.5.10.1. 惯例
为导出序列定义了以下辅助符号,以保留顺序的方式过滤出特定种类的索引:
- func(export^*)=\[ funcidx | \mathrm(func)\ funcidx \in (export.\mathrm{desc}) \]
- tables(export^*)=\[ tableidx | \mathrm(table)\ tableidx \in (export.\mathrm{desc}) \]
- mems(export^*)=\[ memidx | \mathrm(mem)\ memidx \in (export.\mathrm{desc}) \]
- globals(export^*)=\[ globalidx | \mathrm(global)\ globalidx \in (export.\mathrm{desc}) \]
2.5.11. 导入 imports
模块的导入组件定义了实例化所需的一组导入。
\displaylines{ importdesc ::= \mathrm{func}\ typeidx\\ | \mathrm{table}\ tabletype\\ | \mathrm{mem}\ memtype\\ | \mathrm{global}\ globaltype}
每个导入都由两级名称空间标记,该名称空间由模块名称和该模块内实体的名称组成。
可导入的定义为函数,表,内存和全局变量。
每个导入都由一个描述符指定,该描述符的类型与实例化期间提供的定义必须匹配。
每次导入都会在相应的索引空间(index space)中定义一个索引。
在每个索引空间中,导入索引都位于模块本身包含的任何定义的第一个索引之前。
注意
与导出名称不同,导入名称不一定是唯一的。
可以多次导入同一“模块名::名称”。
这样的导入甚至可能具有不同的类型描述,包括不同种类的实体。
仍然可以实例化具有此类导入的模块,具体取决于嵌入程序如何允许解析和提供导入的细节。
但是,不需要嵌入程序来支持此类重载,并且WebAssembly模块本身无法实现重载名称。
3. 验证
3.1. 惯例
验证将检查WebAssembly模块的格式是否正确,因为只能有效的模块能够被实例化。
有效性是由类型系统根据模块及其内容的抽象语法定义的。
对于每个抽象语法,都有一个键入规则,用于指定适用于它的约束。
所有规则均以两种等效形式给出:
- 用行文,以直观的形式描述含义。
- 用公式表示法,以数学形式描述规则。[1]
注意
行文和公式规则是等效的,因此阅读本规范不需要理解公式符号。
公式提供了更简洁的符号描述,该符号广泛用于编程语言的语义中,并易于进行数学证明。
在这两种情况下,规则都是以声明方式制定的。也就是说,它们仅制定约束条件,而没有定义算法。
附录中提供了根据本规范的用于类型检查指令序列的健全完整算法的框架。
3.1.1. 上下文
单个定义的有效性被制定为与上下文相关,该上下文收集有关周围模块和范围内定义的相关信息:
- 类型:当前模块中定义的类型列表。
- 函数:在当前模块中声明的功能列表,以其功能类型表示。
- 表:在当前模块中声明的表格列表,以表格类型表示。
- 内存:在当前模块中声明的内存列表,以其内存类型表示。
- 全局变量:在当前模块中声明的全局变量列表,以其全局类型表示。
- 局部变量:在当前函数中声明的本地列表(包括参数),以其值类型表示。
- 标签:从当前位置可访问的标签堆栈,以其结果类型表示。
- 返回值:当前函数的返回类型,表示为可选结果类型,当不允许返回时(如独立表达式),该结果类型不存在。
换句话说,上下文包含每个索引空间的一系列适当类型,描述该空间中的每个定义条目。
局部变量,标签和返回类型仅用于验证函数体中的指令,而在其他地方保留为空。
标签栈是上下文中随指令序列的验证而变化的唯一部分。
更具体地说,上下文被定义为具有抽象语法的记录(records),:
\displaylines{C::=\mathrm{types}\ functype^*,\\ \mathrm{funcs}\ functype^*,\\ \mathrm{tables}\ tabletype^*,\\ \mathrm{mems}\ memtype^*,\\ \mathrm{globals}\ globaltype^*,\\ \mathrm{locals}\ valtype^*,\\ \mathrm{labels}\ resulttype^*,\\ \mathrm{return}\ resulttype^?}
除了使用编写的现场访问外,还采用以下表示法来处理上下文:
- 拼写上下文时,将省略空白字段。
- 表示与相同的上下文,但元素附加在其组件序列之前。
注意
我们使用诸如之类的索引符号在上下文中的相应索引空间中查找索引。
上下文扩展符号主要用于局部扩展相对索引空间,例如标签索引。
因此,将符号定义为附加在各个序列的前面,引入新的相对索引0并移动现有的相对索引。
3.1.2. 行文符号
验证由程式化规则为抽象语法的每个相关部分指定。 这些规则不仅说明定义短语何时有效的约束,而且还使用类型对短语进行分类。 在说明这些规则时采用了以下约定。
- 当且仅当满足相应规则表示的所有约束时,短语A才被称为“对于T型有效”。 T的形式取决于A是什么。
注意
例如,如果是一个函数,则也是一个函数类型。
如果是全局类型,则也是全局类型; 如此类推。
-
规则隐式假定给定上下文。
-
在某些地方,此上下文在本地扩展到带有其他条目的上下文。措词“在上下文中,…声明…”用于表示以下声明必须在扩展上下文中包含的假设下适用。
3.1.3. 正式符号
注意
本节简要说明了正式指定键入规则的表示法。
对于感兴趣的读者,可以在相应的书中找到更全面的介绍。 [2]
短语具有各自类型的命题被写为。
但是,总的来说,键入取决于上下文。
为明确表示这一点,完整的形式为判断,它表示在C的假设下成立。
正式的符号规则使用一种标准的方法来指定类型系统,将它们呈现为推理规则。
每个规则具有以下一般形式:
这样的规则被认为是一个大含义:如果所有前提都成立,那么结论成立。
有些规则没有前提;它们是其结论无条件成立的公理。
结论始终是判断,并且抽象语法的每个相关构造A都有一个相应的规则。
注意
例如,可以将i32.add指令的输入规则作为一个公理给出:
该指令对于[i32, i32]→[i32]类型始终有效(假设它使用两个i32值并产生一个i32),而与任何其他条件无关。
像local.get这样的指令可以按如下方式键入:
在此,前提要求上下文中存在直接本地索引x。
该指令产生其各自类型t的值(并且不消耗任何值)。
如果C.locals[x]不存在,则前提不成立,并且指令类型错误。最后,结构化指令需要一个递归规则,其中前提本身就是键入判断:
一个block指令仅在其主体中的指令序列有效时才有效。
此外,结果类型必须与区块的注解匹配。
如果是这样,则块指令与主体具有相同的类型。
在内部,可以使用相同类型的其他标签,这可以通过使用前提的其他标签信息扩展上下文C来表示。
[1]语义来自以下文章:Andreas Haas,Andreas Rossberg,Derek Schuff,Ben Titzer,Dan Gohman,Luke Wagner,Alon Zakai,JF Bastien,Michael Holman。 《通过WebAssembly加速Web》。 第38届ACM SIGPLAN编程语言设计和实现会议(PLDI 2017)的会议记录。 ACM 2017年。
[2]例如:Benjamin Pierce。 《类型和编程语言》。 麻省理工学院出版社2002
3.2. 类型
大多数类型都是普遍有效的。
但是,限制适用于函数类型以及表类型和内存类型的限制,必须在验证期间进行检查。
3.2.1. 限制Limits
界限必须具有在给定范围内的有意义的界限。
3.2.1.1.
- n的值不能大于k。
- 如果最大值不为空,则:
- 它的值不能大于k。
- 它的值不能小于n。
- 然后该限制在范围k内有效。
3.2.2. 函数类型
函数类型不能指定一个以上的结果。
3.2.2.1.
- 参数m不得大于1。
- 则函数类型有效。
注意
在将来的WebAssembly版本中,可能消除对返回值至多一个的限制。
3.2.3. 表类型
3.2.3.1. 元素类型:限制
- 限制limits必须在范围内有效
- 则表类型有效。
3.2.4. 内存类型
3.2.4.1. 限制
- 限制limits必须在范围内有效
- 则内存类型有效。
3.2.5. 全局类型
3.2.5.1. 可变值类型
- 全局类型有效
3.2.6. 外部类型
3.2.6.1. 函数类型 func
- func的函数类型functype必须有效。
- 则外部类型有效。
3.2.6.2. 表类型 table
- 差不多同上,仅类型区别,类型有效则有效
3.2.6.3. 内存类型 mem
- 差不多同上,仅类型区别,类型有效则有效
3.2.6.4. 全局类型 global
- 差不多同上,仅类型区别,类型有效则有效
3.3. 指令
指令按函数类型[t]→[t]进行分类,这些函数类型描述了指令如何操纵操作数堆栈。 这些类型描述了必需的输入堆栈,其中弹出了一条指令的类型为t的参数值,以及提供的输出堆栈,其返回的结果为类型t的结果。