On Borrow-Checking Analysis Precision in Rust - PhDData

Access database of worldwide thesis




On Borrow-Checking Analysis Precision in Rust

The thesis was published by Carlsen, Falke Bjernemose Øtker, in January 2023, Aalborg University.

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.



Read the last PhD tips