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

张卓若 等: 面向 Rust 语言的形式化验证方法研究综述 3607

量的可行域和作用域, 默认从声明变量开始有效直到变量所在域结束.
基于上述所有权规则, Rust 针对不同数据类型实现了相应的内存管理策略. 具体来说, 栈基础数据类型 (整型、
浮点型等) 赋值时自动进行值拷贝 (copy), 因此原变量保持有效. 而堆分配类型 (如 String、Vec<T>) 默认使用移
动 (move) 语义. 如图 1 所示, 赋值操作会转移所有权并使原变量失效. 如需确保堆分配变量在赋值操作后保持双
重有效性, 需显式执行堆数据的深拷贝 (clone). 智能指针 Box<T> 针对其指向的分配在堆上的 T 类型数据实现内
存的独占式管理, 当 Box<T> 的所有权被移动或其作用域结束时, 会自动调用析构函数释放堆上分配的内存, 有效
防止内存泄漏. 此外, 当变量作为参数传入函数时, 它遵循与移动操作相同的原则, 即所有权转移到函数中. 相应
地, 如果一个变量作为函数的返回值, 其所有权会随着返回语句从函数中移动出来, 转移到调用者的作用域.

1 let x = String::from("hello"); // x 是 String 类型所有者
2 let y = x; // x 的所有权被转移给了 y
3 // println!("{}", x); // 编译错误: x 不再有效
4 println!("{}", y); // 正常: y 是 String 的新所有者
图 1 Rust 中的所有权机制

2.1.2 借用检查
所有权系统为 Rust 提供了内存管理的基础, 但有时我们需要引用一个值而不转移所有权. Rust 通过借用
(borrowing) 机制实现了这一点. 在 Rust 中, 借用有两种类型: 不可变借用 (immutable borrow) 和可变借用 (mutable
borrow). 借用机制允许一个值在同一时间被多个地方使用, 但同时只能有一个可变借用或者多个不可变借用, 且
所有借用必须在其创建的作用域结束之前有效, 以此保证了数据的一致性, 防止了数据竞争和悬挂指针. 该程序属
性由 Rust 的借用检查器 (borrow checker) 保证, 不满足该属性的程序会被拒绝通过编译. 如图 2, r1 和 r2 是 String
对象的不可变借用者, r3 是 String 对象的可变借用者, 当第 6 行试图同时使用 r1, r2 和 r3 时, 编译器会报错, 因为
在同一时间不允许既有不可变借用又有可变借用.

1 let mut s = String::from("Hello");
2 let r1 = &s; //不可变借用
3 let r2 = &s; // 另一个不可变借用
4 println!("{} and {}", r1, r2); // 同时使用两个不可变借用
5 let r3 = &mut s; //词法生命周期下报错: 同时存在不可变借用和可变借用; 非词法不报错
6 //println!("{},{} and {}", r1, r2, r3); //(词法和非词法下均)报错: 同时存在不可变借用和可变借用
7 println!("{}", r3);
图 2 Rust 中的借用规则例 1

Rust 借用检查器在以下条件同时成立时, 会判定程序中的某个语句违反了借用检查规则: (1) 该语句访问了某
个内存对象. Rust 中将内存对象表示为路径 (path) P 的形式, 如局部变量 a, 访问字段 a.b, 解引用操作*a.b; (2) 访问
路径 P 违反了由某个借用表达式产生的借用 L (loan); (3) 借用 L 此时是活跃 (live) 的, 意味着 L 未来将被用以访
问其借用的内存对象.
例如, 在图 3 中所示的悬垂指针问题中, 涉及的事件序列如下: 在第 5 行, 字符串变量 s 退出其作用域, 编译器
自动插入的 drop 函数随之释放了与之关联的内存对象, 这一过程相当于对路径 s 执行了一次写操作. 在第 4 行,
一个借用表达式创建了一个借用 L0, 该借用是对 s 的不可变借用. 根据 Rust 的借用规则, 写入 s 与借用 L0 是冲突
的, 因为在不可变借用的有效期内, 不允许对借用的内存对象进行修改. 到了第 7 行, 由于 L0 被使用, 这表明在第
5 行执行 drop(s) 时, L0 仍然是活跃的. 因此, 借用检查器发现了这一借用违规, 并报告了错误.
给定一个程序, 能够确定哪些语句将访问内存对象, 以及这些访问操作与借用规则之间的冲突. 关键问题在于
准确推断各个借用的活跃区域, 即 Rust 语言中所谓的生命周期. Rust 通常能够通过借用检查器自动推断生命周