An alias-based formulation of the borrow checker · baby stepsEver since the Rust All Hands, I&rsquo;ve been experimenting with an<br>alternative formulation of the Rust borrow checker. The goal is to<br>find a formulation that overcomes some shortcomings of the current<br>proposal while hopefully also being faster to compute. I have<br>implemented a prototype for this analysis. It passes the full NLL test<br>suite and also handles a few cases – such as #47680 – that the<br>current NLL analysis cannot handle. However, the performance has a<br>long way to go (it is currently slower than existing analysis). That<br>said, I haven&rsquo;t even begun to optimize yet, and I know I am doing some<br>naive and inefficient things that can definitely be done better; so I<br>am still optimistic we&rsquo;ll be able to make big strides there.<br>Also, it was pointed out to me that yesterday, April 26, is the sixth<br>&ldquo;birthday&rdquo; of the borrow check – it&rsquo;s fun to look at my commit from<br>that time, gives a good picture of what Rust was like then.12<br>End-users don&rsquo;t have to care<br>The first thing to note is that this proposal makes no difference<br>from the point of view of an end-user of Rust . That is, the borrow<br>checker ought to work the same as it would have under the NLL<br>proposal, more or less.<br>However, there are some subtle shifts in this proposal in terms of how<br>the compiler thinks about your program, and that could potentially<br>affect future language features.<br>Our first example<br>The analysis works on MIR, but I&rsquo;m going to explain it in terms of<br>simple Rust examples. Here is the first example, which I will call<br>example A. The example should not compile, as you can see:<br>fn main() {<br>let mut x: i32 = 22;<br>let mut v: Veci32> = vec![];<br>let r: &mut Veci32> = &mut v;<br>let p: &i32 = &x; // 1. `x` is borrowed here to create `p`<br>r.push(p); // 2. `p` is stored into `v`, but through `r`<br>x += 1; // take(v); // 3. the reference to `x` is later used here

fn takeT>(p: T) { .. }

Regions are sets of loans<br>The biggest shift in this new approach is that when you have a type<br>like &'a i32, the meaning of 'a changes:<br>In the system described in the NLL RFC, 'a – called a lifetime –<br>ultimately corresponded to some portion of the source program or<br>control-flow graph.<br>Under this proposal, 'a – which I will be calling a region3 –<br>instead corresponds to a set of loans – that is, a set of<br>borrow expressions, like &x or &mut v in Example A. The idea is<br>that if a reference r has type &'a i32 then invalidating the terms<br>of any of the loans in 'a would invalidate r.<br>Invalidating the terms of a loan means to perform an illegal<br>access of the path borrowed by the loan. So for example if you have a<br>mutable loan like r = &mut v, then you can only access the value v<br>through the reference r. Accessing v directly in any way – read,<br>write, or move – would invalidate the loan. For a shared loan like p = &x, reading through x (or p) is allowed, but writing or<br>mutating x would invalidate the terms of the loan (and writing<br>through p is also not possible).<br>The subtyping rules for references work a bit differently now that a<br>region is a set of loans and not program points. Whereas with points,<br>you can approximate a reference by shortening the lifetime, with sets<br>of loans you can approximate by enlarging the set. In other words:<br>'a ⊆ 'b<br>&'a u32 In Rust syntax, 'a ⊆ 'b corresponds to the notation 'a: 'b, and<br>that is what I will use for the rest of the post. We have<br>traditionally called this an outlives relationship, but I am going<br>to call it a subset relationship instead, as befits the new meaning<br>of regions4.<br>To gain a better intuition for the idea of regions as sets of loans, consider<br>this program:<br>let x = vec![1, 2];

let p: &'a i32 = if random() {<br>&x[0] // Loan L0<br>} else {<br>&x[1] // Loan L1<br>};

Here, the region 'a would correspond to the set {L0, L1}, since it<br>may refer to data produced by the loan L0, but it may also refer to<br>data from the loan L1.<br>Datalog<br>Throughout this post, I&rsquo;m going to be defining the analysis by using<br>Datalog rules. Datalog is – in some sense – a subset of Prolog<br>designed for efficient execution. It basically corresponds to rules<br>like this (using the syntax from the Souffle project):<br>.decl cfg_edge(P:point, Q:point)<br>.input cfg_edge

.decl reachable(P:point, Q:point)<br>reachable(P, Q) :- cfg_edge(P, Q).<br>reachable(P, R) :- reachable(P, Q), cfg_edge(Q, R).<br>As you can see here, Datalog programs define relations between things;<br>here those relations are declared with .decl5. Some relations<br>are inputs , declared with .input, which means that their values<br>are given up-front by the user (these are also called facts). In this<br>program, that is cfg_edge. Other relations, like reachable, are<br>defined via rules which synthesize new things from those facts. As in<br>Prolog, upper-case identifiers are variables, and whenever a variable<br>appears twice, it must have the same value.<br>Note that, because it is a subset, Datalog avoids a lot of Prolog&rsquo;s<br>more...