Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915462713966592 |
|---|---|
| author | Grannan, Zachary Bílý, Aurel Fiala, Jonáš Geer, Jasper de Medeiros, Markus Müller, Peter Summers, Alexander J. |
| author_facet | Grannan, Zachary Bílý, Aurel Fiala, Jonáš Geer, Jasper de Medeiros, Markus Müller, Peter Summers, Alexander J. |
| contents | Rust's novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully understanding, extracting and exploiting these guarantees is subtle and challenging: existing models for Rust's type checking either support a smaller idealised language disconnected from real-world Rust code, or come with severe limitations in terms of precise modelling of Rust borrows, composite types storing them, function signatures and loops.
In this paper, we present a novel model of Rust's type-checking called Place Capability Graphs, which lifts these limitations, and which can be directly calculated from the Rust compiler's own programmatic representations and analyses. We demonstrate that our model supports over 97% of Rust functions in the most popular public crates, and show its suitability as a general-purpose basis for verification and program analysis tools by developing promising new prototype versions of the existing Flowistry and Prusti tools. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_21691 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees Grannan, Zachary Bílý, Aurel Fiala, Jonáš Geer, Jasper de Medeiros, Markus Müller, Peter Summers, Alexander J. Programming Languages Rust's novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully understanding, extracting and exploiting these guarantees is subtle and challenging: existing models for Rust's type checking either support a smaller idealised language disconnected from real-world Rust code, or come with severe limitations in terms of precise modelling of Rust borrows, composite types storing them, function signatures and loops. In this paper, we present a novel model of Rust's type-checking called Place Capability Graphs, which lifts these limitations, and which can be directly calculated from the Rust compiler's own programmatic representations and analyses. We demonstrate that our model supports over 97% of Rust functions in the most popular public crates, and show its suitability as a general-purpose basis for verification and program analysis tools by developing promising new prototype versions of the existing Flowistry and Prusti tools. |
| title | Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2503.21691 |