On Borrow-Checking Analysis Precision in Rust
Author
Carlsen, Falke Bjernemose Øtker
Term
4. term
Education
Publication year
2023
Pages
36
Abstract
Denne afhandling undersøger, hvor præcist Rusts borrow checkere afgør, hvilke programmer der er sikre. Borrow checkeren (låne-kontrollen) er en central del af Rust, der håndhæver hukommelsessikkerhed ved at spore referencer (borrows). Vi fokuserer på den nuværende metode, Non-Lexical Lifetimes (NLL), og den planlagte efterfølger, Polonius. Vores motivation er et eksempelprogram, get_or_insert.rs, som NLL afviser, selv om det bruger mønstre, mange udviklere ville forvente virker. Vi analyserer adfærden i den nuværende og fremtidige checker og foreslår en alternativ borrow-checking-analyse, der kører på Rusts Mid-level Intermediate Representation (MIR). Vores metode bygger på klassisk compiler liveness-analyse, som afgør, hvornår variabler stadig er i brug, og koder Rusts låne-regler som overlappende låneudtryk. Vi har implementeret et proof-of-concept i Python. I vores små tests accepterer det to tilfælde, som NLL i dag afviser, og afviser korrekt et trivielt ugyldigt program. Vores evaluering har dog vigtige begrænsninger: oversættelsen af de NLL-afviste Rust-programmer til MIR er ikke formelt begrundet, og vi giver ingen korrekthedsbevis for vores analyse.
This thesis examines how precisely Rust's borrow checkers decide which programs are safe. The borrow checker is a core part of Rust that enforces memory safety by tracking references (borrows). We focus on the current approach, Non-Lexical Lifetimes (NLL), and the planned successor, Polonius. Our motivation is an example program, get_or_insert.rs, which NLL rejects even though it uses patterns many programmers would expect to work. We analyze the behavior of the current and future checkers and propose an alternative borrow-checking analysis that runs on Rust's Mid-level Intermediate Representation (MIR). Our method builds on classic compiler liveness analysis, which identifies when variables are still in use, and encodes Rust's borrowing rules as overlapping borrow expressions. We implemented a proof of concept in Python. In our small tests, it accepts two cases that NLL currently rejects and correctly rejects a trivially invalid program. However, our evaluation has important limitations: the translation of the NLL-rejected Rust programs into MIR is not formally justified, and we do not provide a proof of correctness for our analysis.
[This summary has been rewritten with the help of AI based on the project's original abstract]
Keywords
Documents