能力图：Rust所有权与借用保障机制的通用模型

《Proceedings of the ACM on Programming Languages》：Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees

Rust的类型系统为验证和分析工具提供了丰富的别名和可变 guarantees，但现有模型存在语言支持不足或精度问题。本文提出Place Capability Graphs模型，通过直接计算Rust编译器的分析结果，有效支持复杂借用、组合类型和循环结构，并在实际项目中验证了97%以上主流Rust crate的功能覆盖，并成功改进Flowistry和Prusti工具。

　　

摘要

由于Rust的类型系统在控制别名和可变性方面提供了丰富的保障，因此它成为了验证和程序分析工具的理想目标。然而，完全理解、提取和利用这些保障是非常微妙且具有挑战性的：现有的Rust类型检查模型要么支持一种与实际Rust代码脱节的简化语言，要么在精确建模Rust的借用操作、存储这些操作的复合类型、函数签名以及循环等方面存在严重限制。

在本文中，我们提出了“位置能力图”（Place Capability Graphs）：这是一种新的Rust类型检查结果模型，它克服了上述限制，并且可以直接从Rust编译器自身的程序化表示和分析中计算得出。我们证明了该模型能够覆盖最流行的公共Rust库中97%以上的函数，并通过开发Flowistry和Prusti工具的新原型版本，展示了其作为通用验证和程序分析工具基础的适用性。