Page 189 - 《软件学报》2025年第8期

3612 软件学报 2025 年第 36 卷第 8 期

此后, 据 MIR 内容及 LLVM IR 规范进行相应的逻辑转换, 生成 LLVM IR 代码, 再使用 LLVM 生成汇编代码, 最
后进行编译链接生成二进制代码.

词法分析, 语法分析 脱糖 类型推断, 类型检查 优化, 借用检查 优化
宏展开, 名称解析 trait 解析

源程序 AST HIR MIR LLVM IR 汇编代码

图 8 Rust 编译过程

值得一提的是, Rust 语言的表面 (surface) 语法富含大量的语法糖, 而对于这些语法, Rust 语言社区尚未给出
一套正式的操作语义定义. 相比之下, MIR 显著简化了语言的复杂性. MIR 拥有一组精简的操作集, 通过去糖处理
简化掉了 Rust 表面层的许多复杂特性, 例如循环和模式匹配语句, 且函数体以控制流图的形式清晰呈现. 同时,
MIR 中仍然保留了 Rust 所有权和借用概念的核心, 这些概念在类型系统中占据着重要位置. 此外, MIR 还保留了
泛型定义, 使得语言的通用性得以延续. 因此, 与复杂的表面 Rust 语法相比, MIR 提供了一个更为简洁和易于操作
的环境, 同时保留了语言的关键特性. 同时, MIR 提供了丰富的应用程序接口 (API), 这些 API 允许开发者访问、
提取和操作 Rust 程序的 MIR 表示. MIR 的这些特性使其不仅在编译过程中扮演着关键角色, 而且还是进行深入
程序分析和逻辑推理的理想选择. 如今, MIR 已经成为形式化语义深入研究和精准高效验证工具开发的对象. 很
多验证工具与 Rust 编译器的紧密集成, 在 Rust 编译器完成类型检查之后提取 MIR 及类型和借用检查信息, 再进
行进一步的分析推理.

3 针对 Rust 形式语义的研究工作

类型系统作为 Rust 语言的基石, 对程序的正确性、安全性和效率起着至关重要的作用. 大多数对 Rust 的形
式化语义研究工作捕捉了 Rust 类型系统的核心, 描述 Rust 类型推断和借用检查的过程, 并给出类型系统的可靠
性证明, 表明遵循 Rust 所有权、借用和生命周期规则的程序是内存和线程安全的. 还有一些工作没有借助类型系
统, 而是主要建模了 Rust 以内存管理为核心的操作语义来描述 Rust 的形式规范, 包括所有权系统、借用检查、
生命周期规则等. 对 Rust 的形式化语义的研究工作提供了一种精准清晰的语义框架以便开发人员更深入地学习
和探索这一新兴编程范式的机制和特性, 同时也为后续开发 Rust 程序验证工具提供了坚实的理论基础. 本节首先
对类型系统的概念进行精炼的概述, 并特别聚焦于 Rust 语言的类型系统, 此后分别介绍基于 Rust 类型系统的语
义研究工作和基于纯操作语义的 Rust 语义研究工作. 表 1 总结了不同形式语义模型研究工作的差别. 其中, “正确
性保证”表示该工作是否使用了机械化的证明 (如借助 Coq 证明助手 [18] 证明) 确保语义模型正确性, “内存模型”表
示该工作是否精准地刻画了 Rust 的内存模型.

表 1 Rust 形式语义模型研究工作总结对比

支持语言特性
研究工作 正确保证 类型系统 数据结构 内存模型 生命周期 验证性质
Unsafe Closure 并发 Trait
RustBelt [13] ● ● MIR ○ 生命周期逻辑 并发、内存安全 ● ○ ● ○
[19]
RustHornBelt ● ● MIR ○ 生命周期逻辑 并发、内存安全 ● ○ ● ○
[15]
RefinedRust ● ● MIR ● 生命周期逻辑 功能正确性 ● ○ ○ ○
[20]
Oxide ○ ● Rust ○ Polonius 功能正确性 ○ ● ○ ○
[21]
Flux ○ ● MIR ● NLL 类型安全 ○ ● ○ ○
[22]
FR ○ ● Rust ○ 词法 类型安全, 功能正确性 ○ ○ ○ ○
[23]
Patina ○ ● Rust ○ 词法 类型安全 ○ ○ ○ ○
[24]
StackedBorrows ○ ○ Rust ● 栈表示 编译优化, UB ● ○ ○ ○
[25]
KRust ○ ○ Rust ○ 词法 功能正确性 ○ ○ ○ ○
[26]
RustSEM ○ ○ Rust ○ NLL 并发、内存安全 ● ● ● ●