KRust:Rust形式化可执行语义*

王 丰，张 俊

1.中国科学院 上海微系统与信息技术研究所，上海 200050

2.上海科技大学 信息科学与技术学院，上海 201210

3.中国科学院大学，北京 100049

1 引言

Rust是近年来兴起的系统级编程语言，由火狐浏览器的开发商Mozilla[1]研发和维护。Rust 旨在不牺牲性能的情况下，实现内存安全和对内存的精细化控制。Rust 目前已经被应用到大型系统级软件的开发中，例如操作系统、设备驱动、游戏引擎和网络浏览器等。和Rust不同，C/C++虽然提供了对内存的精细化控制，但是由于没有垃圾回收机制，需要程序员自己手动释放申请的动态内存，这将会导致大量的内存安全问题，例如野指针等等。Java等语言提供了垃圾回收功能，但是程序员对内存的控制方面不如C/C++高效。另一方面，垃圾回收运行的时候会影响整个程序的运行，对程序的性能会产生影响。

Rust 有三个主要特性：所有权、借用和生命周期。这些特性使得Rust和主流系统级的编程语言有着本质的不同。在Rust 中，资源的所有权是一个变量绑定。当一个变量离开它的作用域的时候，Rust会自动释放这个变量所绑定的资源。资源的所有权可以被转移。这个特性保证了对任意一个资源，只有唯一的一个所有者。Rust提供了借用机制，可以让一个资源被多个变量共享。借用机制的实现需要使用引用类型。在Rust中，有两种引用类型：可变引用和不可变引用。可变引用可以用来修改资源，而不可变引用只能用来读取资源，不能用来修改。Rust的借用机制有两条规则：一个资源如果有多个引用，那么这些引用都必须是不可变引用；可变引用最多只能有一个。Rust 的生命周期机制用来规避不安全的借用。任何的借用都必须比资源所有者有更小的作用域。这个机制消除了很多内存问题，例如“野指针”和“释放后使用”等。

形式化语义是构建程序分析和验证工具，例如模型检查等，和协助开发安全可靠的编译器的基础。目前来说，Rust 的形式化语义还没有被充分研究，也没有一个完备的语义，对程序分析和验证工具的开发造成了很大的困难。在这篇文章中，提出了针对Rust 语言的形式化可执行操作语义KRust。KRust 是第一个刻画Rust 的形式化可执行操作语义。“可执行”表示KRust 可以根据语义，直接运行Rust 程序。目前，实现的语义规则涉及了Rust 的核心特性：所有权、借用和生命周期。使用了K 框架[2](以下简称K)来开发。K是专门用来刻画编程语言语义的工具。使用K 定义的形式化语义有很多好处。首先，K 能自动生成一个解释器，因此用K 实现的语义是可执行的。另外，K提供了模型检查和符号执行等形式化工具，因此定义好语义规则后，可以直接使用K提供的工具对Rust程序进行形式化分析。

2 Rust特性介绍

2.1 所有权

所有权是Rust 最重要的特性，确保了程序中的资源有且仅有一个所有者。

在上面的程序中，第2行定义了一个字符串类型的变量s。此时，s拥有了一个字符串“Hello”。在程序的第3行，s被赋值给了新的变量v。Rust的所有权机制导致了s将失去原有字符串的所有权，v成为了字符串“Hello”的所有者。此后，不能再通过s访问原来的字符串，因此第4行输出s内容的语句会报错。

2.2 借用

Rust 提供了借用机制，通过使用引用类型（&和&mut），可以临时把资源的所有权借用给其他变量。

在上面的例子中，第2行和第5行分别使用了mut 关键词定义了一个可变的变量。在第3行，变量a被借用给了x，但这个借用是不可变借用，因此第4行尝试通过x来修改a的值会报错。第6行的借用是可变借用，可以通过y来修改b的值。

2.3 生命周期

Rust 的借用机制赋予了变量对一个资源临时的读写权限，而生命周期机制是用来检查借用是否有效的手段。

上面的程序首先定义了一个可变变量x。第3行到第6行中间的代码块中定义了一个变量y，初始值为2，然后把对y的可变借用赋值给了x。x是在代码块之前定义的，x的生命周期一直到程序的最后一行，而y的生命周期在第6行就结束了。如果x想要借用y的值，Rust 的生命周期机制则会要求x的生命周期必须包含于y的生命周期。而此时x的生命周期是包含y的，因此第5行的借用和第7行的赋值都无效，并报错。如果没有生命周期机制，x在第6行之后就是一个“空指针”，造成内存安全问题。

3 KRust:使用K定义的Rust形式化语义

3.1 K框架

K是一个可执行的语义框架，提供了程序状态空间和语义规则的表示方法，可以方便用来定义一门语言的操作语义。K可以自动生成解释器，来执行真实的代码。除此以外，K 提供了很多静态分析工具，比如模型检查、符号执行和定理证明等。目前，已经有很多语言使用K 定义了形式化语义，例如C[3-4]、Python[5]、PHP[6]、Java[7]和JavaScript[8]等。

语义规则是基于程序状态来描述，实现语义规则首先需要刻画程序状态。K 提供了“结构”的概念来描述程序状态，其中包含了自定义的标签和映射关系。为了方便阅读，本文中语义规则的书写没有完全遵循K 的语法。图1是一个简单的语义规则的示例，其规则用来查找一个变量对应的值。规则中涉及到了三个标签。第一个标签k 用来存储需要被执行的程序语句。第二个标签env 存储的是映射关系集合，记录变量名和地址之间的对应关系。第三个标签store 也是映射关系的集合，和env 不同，store记录的是地址和值之间的映射关系。这个规则表示的意思是，X会被替换为V，当且仅当env标签中存在从X到L的映射，并且store中存在从L到V的映射。

Fig.1 Rule for lookup图1 变量替换规则

3.2 KRust结构

图2展示了KRust 用来描述Rust 程序状态所使用的15个标签。T标签是K提供的顶层标签，用来包含其他自定义的标签。k 里面记录的是所有的程序语句。env 记录变量到地址的映射的集合。control和fstack 用来实现函数调用，fstack 包含的是一个列表，列表里每个元素包含的是一个局部的env 标签、程序语句和返回值类型。genv 是全局的映射关系。typeEnv记录的是变量对应的类型。变量对应的值存储在store 标签中。mutType 用来记录一个变量是否是可变的。nextLoc 用来为新申明的变量分配地址，其中仅包含一个整型值，表示下一个可用的地址。borrow 记录对象是否被其他变量引用了，以及是被可变引用了，还是被不可变引用了。ref 记录一个变量引用的另一个变量的地址，引用的类型是可变引用还是不可变引用记录在了refType中。moved记录对象是否被清理了。mType 记录成员函数的类型。methods保存了Trait中定义的函数接口（Rust的Trait类似于Java 的接口概念）。enumElements 记录了枚举类型中的元素。

Fig.2 Configuration of KRust图2 KRust结构

3.3 语义规则

KRust 目前已经实现了405条语义，包括了变量的声明和赋值、变量之间的借用、解引用、函数（包括结构体中成员函数）的定义及调用、结构体、Trait 和模式匹配等。KRust 语义中包含的类型有基本数据类型、引用类型、结构体类型、枚举类型、静态数组和动态数组等。KRust也实现了基本的控制流语义，包括分支判断和循环操作等。KRust 实现了Rust 最重要的3个特性，即所有权、借用和生命周期。由于篇幅所限，下面仅列举了5条语义规则，全部语义详见KRust源代码(https://bitbucket.org/jerrywang304/krustcode)。在这些语义规则中，“↦”表示存在一对映射。“⇒”用来新增加一对映射。“ ⊥”表示未定义的值。“A↦(B⇒C)”表示将原来的映射对“A↦B”替换为“A↦C”。一条程序语句被K执行成功之后，会被替换为K中的特殊符号“·”，然后再继续执行下一条。

3.3.1 变量声明

图3给出的是变量声明语义规则。在定义一个不可变且有显式类型的变量后，首先需要给变量分配一个地址L，并且在env标签中增加从X到L的映射关系。X并没有初始化值，因此store 标签中的值为“⊥”。typeEnv中记录了X的类型为T。mutType中，0代表不可变。moved中，0表示没有被清理，因为此时只是定义X。nextLoc中保存的是下一个可用的地址，L已经被使用了，则下一个可用地址为L+1。在其他标签中，由于X还未被使用，值都为“⊥”。

Fig.3 Rule for declaration图3 变量声明规则

3.3.2 借用和生命周期

图4给出的是可变借用语义规则。如需要把一个变量Y借用给另一个变量X，需要满足X存活的时间比Y长的条件。L1＞L2限制了X必须在Y之后被定义，即X的生命周期是包含于Y的。moved标签中两个映射对必须存在，确保X和Y此时没有被清理。另外，在把Y的可变引用赋值给X之前，Y必须满足没有被其他变量所引用，无论是可变引用还是不可变引用。因此，在borrow 标签中，Y的地址L2对应的值之前必须是“⊥”，然后需要改成1。在borrow标签中，1表示已经被可变引用，0表示已经被不可变引用。

Fig.4 Rule for mutable borrowing图4 可变借用规则

3.3.3 结构体和所有权转移

在图5定义的语义规则中，S是一个已经定义的结构体。X被声明为可变变量，并且初值为一个结构体实例，此时X的类型被更新为S。F1是语义规则中定义的辅助函数，用来存储结构体中的字段。TIDs表示的是函数参数的类型。在这条规则中，store 标签中的映射对确保了S的确是一个结构体，否则这条语义不会被执行。Vs中存储的是结构体实例中字段具体的值。F2是另一个自定义的辅助函数，用来完成具体的赋值工作，即把Vs赋值给X中的字段，此后可以通过X来获取这个结构体实例中的值。

Fig.5 Rule for declaration of struct instance图5 结构体实例声明规则

图6定义了结构体变量所有权转移的规则。X和Y都是S类型，即结构体变量。把Y赋值给X后，X变为Y对应的结构体实例的拥有者。F3辅助函数会将Y中的字段的值，赋值给X中对应的字段的值。然后F4辅助函数会将moved 标签中Y对应的值由0改为1，即清理掉Y的结构体实例。

Fig.6 Rule for ownership move of struct图6 结构体所有权转移规则

3.3.4 结构体成员函数实现

图7这条语义将impl 中的成员函数依次进行处理。env 和store 中的映射对用来确保S是一个结构体。针对每个成员函数，这条语义会把其转化为全局函数，函数名改为“S∷X”，并且更新形参列表，然后递归进行处理。由于成员函数的第一个参数为self，将会占有调用次函数的变量的所有权，因此在mType标签中，将函数名对应的值赋值为自定义的标识符“take”，在此成员函数调用的时候会被使用，用来转移调用者的所有权。

Fig.7 Rule for struct methods图7 结构体成员函数规则

4 测试和应用

4.1 一致性测试

和先前文献中的工作一样[3-8]，KRust也使用了测试集来测试语义实现的和Rust 编译器是否一致，即给定相同的代码，比较KRust和Rust官方编译器编译执行后的输出结果。采用的测试集包括了Rust编译器官方测试集和针对每个语义规则写的Rust 代码。Rust 官方提供了针对编译器的测试集。官方测试集中的大量代码有调用库函数，调用外部C 程序代码，没有主函数，只针对Rust 某个版本和只适用于特定操作系统等问题，不完全适合用来做语义对比测试。从官方测试集中选取了157个合适的测试样例。在这些代码中，KRust和Rust编译器表现出了一致的行为。由于这157个测试样例没有涵盖KRust支持的全部语法和语义，在实验过程中使用了另外34个真实有效的Rust 代码。在这部分测试代码中，KRust 没有表现出和Rust 编译器完全相同的行为。在测试结构体成员函数的语义规则中，实验发现了Rust编译器的bug。

在上面的例子中，第1行定义了一个结构体，第2行至第6行为结构体实现了一个成员函数。这个成员函数的参数是self，不是引用，一旦被调用会导致结构体实例的所有权转移。第8行定义了一个结构体实例。第9行将结构体实例所有权进行转移。第10行的调用会导致q被清理掉。但是依然可以在第11行使用q尝试修改结构体实例。编译器没有在第11行做出警告和报错。根据Rust官方文档的介绍，q对应的结构体实例此时已经被清理，不能再被访问。KRust不会成功执行第11行的代码，因为它违反了KRust中定义好的语义规则，而Rust编译器没有在第11行发出任何警告或者报错信息。把这个问题报给了Rust社区。Rust编译器已经对这个问题进行了更新，最新版本(1.33.0)对这类操作会给出警告，未来Rust编译器更加完善后，会直接给出报错信息。

4.2 应用

K 提供的形式化工具，可以用来进行模型检查、可达性分析、符号执行和验证等。

4.2.1调试器

K自带的调试工具可以方便用来查看程序状态。

假设上面的程序名为sample.rs，可以使用如下命令来调试查看每一条语义规则执行后的程序状态。

1.krun sample.rs--debugger

在第4行代码第一次被执行后，调试器会显示出如下的程序状态。

4.2.2 验证工具

下面是一个具体的验证算法复杂度的例子。

上面的Rust代码使用了辗转相减法来计算最大公约数。K提供了一个配置文件，用来做验证。为了证明算法的复杂度为O(max(a,b))，需要在配置文件中添加以下内容。

time 标签中保存的是一个整数，函数每调用一次，这个数加1。T1和T2分别代表了函数调用前后time标签里的值，T2-T1代表了函数执行的次数。K的验证工具输出为“true”，证明了T2-T1 ≤maxInt(X,Y)，即复杂度为O(max(a,b))。

5 相关工作

K已经成功地被用来定义了多种语言的语义，例如C[3-4]、Java 1.4[7]、JavaScript[8]、PHP[6]、Python3.3[5]、Verilog[9]和Scheme[10]。Rust 和这些语言有着本质的不同，不能简单模仿这些工作，需要重新定义程序状态和语义规则。Rust 的出现吸引了很多研究者的关注，目前已经有一些关于Rust 测试和语义等方面的工作。Reed 也发表了Rust 语义相关的工作，主要针对的是Rust的借用检查器（borrow checker）。但是这份语义支持的Rust 的语法过于陈旧，并且没有被实现，更不能被执行[11]。Jung等人使用Coq定义了新的语言λRust和这门语言的语义[12]。这份工作主要研究的是Rust 的所有权机制。λRust和Rust 的中间表示（mid-level intermediate representation，MIR）非常相似，但不是真实Rust语言。并且，λRust定义了比Rust语言本身还多的语义。Dewey等人针对Rust的类型检查开发了一款模糊测试工具，并且发现了Rust 编译器的问题[13]，这项研究也说明了在开发安全可靠的编译器的过程中是需要形式化语义的。目前已有研究人员针对Rust开发了程序分析工具[14-15]，但是这两个工作都把Rust转到其他的编程语言，例如C语言，然后应用针对这个语言的程序分析工具进行分析。但是，把编程语言转换的过程很容易出现不一致的情况，会丢失语言的特性，也很难保证转换的正确性。KRust描述的就是Rust的语义，没有做任何转变。

6 结束语

本文给出了第一个针对Rust语言的形式化可执行语义KRust。KRust目前涵盖了Rust中所有的基本类型和基本运算；复合数据类型，例如结构体、数组和动态数组，以及枚举类型；基本的控制流和分支判断；函数，包括成员函数的定义和调用；Trait；模式匹配等。KRust 实现的语义规则涵盖了Rust 最重要的三个特性，即所有权、借用和生命周期。为了测试KRust的语义和Rust语义的一致性，使用了真实有效的Rust 代码作为测试集，其中包括了Rust 官方编译器测试样例。同时，通过一致性对比测试，发现了Rust编译器的问题。另外，还介绍了KRust在Rust程序分析和验证上的潜在应用。本文主要的工作是实现Rust 核心语义，未来工作包括实现更多的语义规则，使KRust 更加完备，以及把KRust 应用到开发Rust程序分析工具中。