On Borrow-Checking Analysis Precision in Rust
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.
https://vbn.aau.dk/ws/files/512993395/On_Borrow_Checking_Analysis_Precision_in_Rust_Falke_Carlsen.pdf
https://vbn.aau.dk/ws/files/511261353/w_smile.png