Modelling Rust’s Reference Ownership Analysis Declaratively in Datalog

Abstract: Rust is a modern systems programming language that offers improved memory safety over traditional languages like C or C++ as well as automatic memory managementwithout introducing garbage collection. In particular, it guarantees that well-typedprograms are free from data-races caused by memory-aliasing, use-after-frees, and accesses to deinitialised or uninitialised memory. At the heart of Rust's memory safety guarantees lies a system of memory ownership, verified statically in the compiler by aprocess called the borrow check. However, the current implementation of theborrow check is not expressive enough to prove several desirable programs safe,despite being so. This report introduces an improved borrow check called Polonius,which increases the resolution of the analysis to reason at the program statement level, and enables a more expressive formulation of the borrow check itself through the use of a domain-specific language, Datalog. To the best of our knowledge, Polonius is the first use of Datalog for type verification in the compiler of aproduction language. Specifically, this thesis extends Polonius with initialisation and liveness computationsfor variables, and constitutes the first complete description of Polonius in text. Finally,it describes an exploratory study of input data for Polonius generated by analysingcirca 12~000 popular Git repositories found on GitHub and the Crates.io Rustpackage index. Some central findings from the study are that deallocations are uncommon relative to other variable uses, and that a weaker (and therefore faster)analysis than Polonius is often sufficient to prove a program correct. Indeed, many functions (circa 64%) do not create any references at all, and therefore do not involve the reference-analysis part of the borrow check.