Place Capability Graphs: Rust 所有权和借用保证的通用模型
编程语言
2025-08-27 v5
摘要
Rust 类型系统因其对控制别名和可变性的丰富保证而成为验证和程序分析工具的吸引目标。然而，完全理解、提取和利用这些保证并不容易：现有的 Rust 类型检查模型要么支持与实际 Rust 代码相距甚远的较小理想化语言，要么在精确建模 Rust 借用、存储它们的复合类型、函数签名和循环方面存在严重限制。本文提出了一种名为 Place Capability Graphs 的 Rust 类型检查新模型，克服了这些限制，并且可以直接从 Rust 编译器自己的程序化表示和分析中计算得出。我们演示了该模型支持最流行的公共 crate 中超过 97% 的 Rust 函数，并展示了其作为通用-purpose 验证和程序分析工具的适用性，通过开发新的原型版本 Flowistry 和 Prusti 工具。
引用
@article{arxiv.2503.21691,
title = {Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees},
author = {Zachary Grannan and Aurel Bílý and Jonáš Fiala and Jasper Geer and Markus de Medeiros and Peter Müller and Alexander J. Summers},
journal= {arXiv preprint arXiv:2503.21691},
year = {2025}
}