On Borrow-Checking Analysis Precision in Rust
Term
4. term
Education
Publication year
2023
Submitted on
2023-01-20
Pages
36
Abstract
We investigate the precision of existing borrow-checking analyses; the current Non-Lexical Lifetimes (NLL) and future Polonius. This is motivated by the exemplary program 'get_or_insert.rs', which is rejected by NLL, as it employs seemingly ordinary patterns that users might expect to function. We aim to understand the current and future borrow-checkers of Rust and propose our own borrow-checking analysis on Rusts Mid-level Intermediate Representation, based on the classic compiler liveness analysis and encoding Rusts borrowing rules into overlapping borrow-expression. With our proposed analysis follows a proof-of-concept implementation in Python which passes two accept cases currently rejected by NLL and rejects a trivially invalid program. Out results are rebutted by unproven translation of NLL-rejected Rust programs into MIR and lack of correctness proof for our analysis.
Keywords
Documents