Rewriting Rust’s Borrow Checker in SQL

Many beginners are intimidated by Rust’s borrow checker. It’s a unique tool that prevents unsafe reference access and gives Rust strict compile-time safety. At first, the errors it outputs can seem obscure and unintuitive. However, most people don’t realize that the central mechanism can be implemented with a couple of SQL queries!

The History of Borrow Checking

The golden rule is that you can either have one mutable reference or any number of immutable references. But how does Rust know whether you’re borrowing correctly?

There have been three major approaches to borrow checking in Rust: Lexical Lifetimes, Non-Lexical Lifetimes (NLL), and Polonius.

In early versions of Rust, references were considered alive until they went out of scope. The borrow checker could therefore look at the range of lines where a reference was in scope and ensure that the golden rule was followed. This is called a lexical lifetime because it uses the lexical scope of the variable to determine when the borrow ends.

However, this approach is overly conservative. What if I have a reference in scope but only use it twice? Should its borrow persist for the entire scope?

Non-Lexical Lifetimes (NLL) take a more intelligent approach by determining when a reference is used for the last time. Instead of tying a borrow to the enclosing scope, NLL ends the borrow after its final use. This makes borrow checking much more granular and allows the compiler to accept many more valid programs.

However, NLL is still conservative in some cases because it can’t precisely reason about every possible control-flow path. Here is an example of a program that NLL rejects even though it is safe. As humans, it’s clear that either the if branch executes and returns, or the code afterwards executes—but never both.

1use std::collections::HashMap;2use std::hash::Hash;3
4fn get_or_insert_default<'a, K, V>(5    map: &'a mut HashMap<K, V>,6    key: K,7) -> &'a mut V8where9    K: Hash + Eq + Copy,10    V: Default,11{12    if let Some(value) = map.get_mut(&key) {13        return value;14    }15
16    map.insert(key, V::default());17    map.get_mut(&key).unwrap()18}

Polonius

More recently, the Rust community has been developing a new borrow checker called Polonius.

The original Polonius model expressed borrow checking as Datalog rules evaluated using Datafrog. Datafrog is a logic engine that derives facts from a set of core premises.

Rustc first lowers the source into MIR (Mid-level Intermediate Representation), where the function is represented as basic blocks connected by control-flow edges. The borrow checker then extracts facts from that MIR. From these facts, it repeatedly derives new facts until it reaches a fixed point, at which no additional information can be inferred.

Because facts are structured statements and recursive derivations are just joins between structured statements, you can think of this control-flow analysis as a set of recursive joins—similar to those in a SQL database. We’ll be implementing a toy borrow checker inspired by this style of analysis.

Implementing Borrow Checking in SQL

We can start by defining some core primitives. We can represent every fact about a program as a row in a table. Relations are sets of facts generated from a program. Rules are inference statements used to derive facts from other facts.

A Toy Example

Consider an implication(source, target) relation. We will write the fact implication(A, B) as A => B. A rule can be: If A => B and B => C, then A => C for all A, B, C. Thus, through recursively applying this rule, we can trivially prove that A => D for the following pseudocode.

1A => B2B => C3C => D

One way to express this in SQL would be to use a self-join on an implication table with the following query:

1SELECT first.source, second.target2FROM implication AS first3JOIN implication AS second4  ON first.target = second.source;

We can take these results and insert them back into the implication table, which stores all the facts we know about a program. We can loop this until we can no longer derive facts. The code for inserting in this example is shown below:

1INSERT INTO implication (source, target)2SELECT first.source, second.target3FROM implication AS first4JOIN implication AS second5  ON first.target = second.source6ON CONFLICT DO NOTHING;

As mysterious as a borrow checker may seem, its behavior can be attributed to this loop.

A More Concrete Example

Consider the short block of Rust code with a clearly illegal reference access:

1fn main() {2    let mut value = 0;3    let borrowed = &value;4    value = 1;5    println!("{borrowed}");6}

We can define cfg_edge(source, target) as a relation that says control may move directly from one MIR point to another. In this example the graph is a straight line, but branches produce multiple outgoing edges.

We can also define loan_live_at as a relation that says that if a reference (we will call it a loan) is live at P1 and cfg_edge(P1, P2), then the loan may also be live at P2 (depending on what is required at P2).

Now we can check variable liveness—how long a variable lives in a program. These are propagated backward. We read the println!(...) statement and infer that borrowed must have existed at every preceding point until we reach its definition.

On the line where the loan is issued for borrowed (we’ll refer to the loan as bw0), we can say that the loan must also be live for that same lifetime. While the shared loan is live, the borrowed value cannot be mutated through a competing access path. Therefore, assigning to value produces a loan_invalidated_at fact. Finally, we can define a rule that if a loan is both alive and invalidated, then there is an unsafe access and prove that this access is unsafe.

Let’s say we swapped the assignment and the final use. The program below would be valid because L3 is the final use of borrowed, so backward liveness does not make it live at L4. The mutation therefore occurs after the loan has ended.

1fn main() {2    let mut value = 0;3    let borrowed = &value;4    println!("{borrowed}");5    value = 1;6}

Expressing the Basic Rules

We can express some basic rules in SQL from these explorations.

Rule 1: A used variable is live

If a variable is used at a point, then it must be live when execution reaches that point.

1IF var_used_at(V, P)2=>3var_live_on_entry(V, P)

This can be expressed in SQL as:

1INSERT INTO var_live_on_entry (variable, point)2SELECT variable, point3FROM var_used_at4ON CONFLICT DO NOTHING;

Rule 2: Propagate liveness backward

If a variable is live at P2, and control moves from P1 to P2, then the variable must also be live at P1. However, propagation stops if the variable is defined at P1.

1IF var_live_on_entry(V, P2)2AND cfg_edge(P1, P2)3AND NOT var_defined_at(V, P1)4=>5var_live_on_entry(V, P1)

This can be expressed in SQL as:

1INSERT INTO var_live_on_entry (variable, point)2SELECT live.variable, edge.source3FROM var_live_on_entry AS live4JOIN cfg_edge AS edge5  ON edge.target = live.point6WHERE NOT EXISTS (7    SELECT 18    FROM var_defined_at AS defined9    WHERE defined.variable = live.variable10      AND defined.point = edge.source11)12ON CONFLICT DO NOTHING;

Rule 3: Introduce loan_required_at as a toy bridge

Note: loan_required_at is made up for this post to keep the rule compact. A real checker derives the equivalent “still needed here” information from liveness plus origin/loan relationships, rather than treating it as an input fact.

Rule 4: Propagate a required loan forward

If a loan is live at one point, control can move to another point, and the loan is still required there, then it is live at the next point.

1IF loan_live_at(L, P1)2AND cfg_edge(P1, P2)3AND loan_required_at(L, P2)4=>5loan_live_at(L, P2)

This can be expressed in SQL as:

1INSERT INTO loan_live_at (loan, point)2SELECT live.loan, edge.target3FROM loan_live_at AS live4JOIN cfg_edge AS edge5  ON edge.source = live.point6JOIN loan_required_at AS required7  ON required.loan = live.loan8 AND required.point = edge.target9ON CONFLICT DO NOTHING;

Rule 5: Detect an invalidated live loan

If a loan is live and invalidated at the same point, then the program contains an unsafe access.

1IF loan_live_at(L, P)2AND loan_invalidated_at(P, L)3=>4error(L, P)

This can be expressed in SQL as:

1INSERT INTO errors (loan, point)2SELECT live.loan, live.point3FROM loan_live_at AS live4JOIN loan_invalidated_at AS invalidated5  ON invalidated.loan = live.loan6 AND invalidated.point = live.point7ON CONFLICT DO NOTHING;

These rules are not a complete representation of the borrow checker, but they demonstrate the analysis it performs.

Implementation

A simple implementation is included in this repository for you to follow along with. Rust’s borrow checker does not run on the source code directly, but rather on the mid-level intermediate representation. At this level, all conditionals are decomposed into “basic blocks,” which are sets of continuous instructions ending in a branch, jump, or return. Variable names are replaced with placeholders, and the representation uses cryptic internal names for primitives that are outside the scope of this blog.

The important thing to know is that we can get a list of the facts (rows in our relations) by running the following command:

1rustup run nightly rustc \2    -Z nll-facts \3    -Z nll-facts-dir=fixtures/borrow_conflict \4    -Z dump-mir=nll \5    -Z dump-mir-dir=fixtures/borrow_conflict/mir \6    fixtures/source/borrow_conflict.rs

Note that the default Rust compiler does not support this and you must be running the nightly toolchain. This command produces two outputs. -Z nll-facts emits the relation files that Laertes loads into PostgreSQL. -Z dump-mir emits a human-readable MIR representation that helps us understand where those facts came from. Example outputs are in /fixtures/.

We can start by defining structs for rules and relations.

1#[derive(Debug, Clone, PartialEq, Eq)]2pub struct Relation {3    pub name: &'static str,4    // Generic to allow us to represent5    // Edge(source, target)6    // LoanIssuedAt(origin, loan, point)7    // LoanKilledAt(loan, point)8    pub columns: &'static [&'static str],9}10
11#[derive(Debug, Clone, PartialEq, Eq)]12pub struct Rule {13    pub name: &'static str,14    pub target: &'static str,15    pub select: &'static str,16}

We can write all of our rules in SQL. These can be found in the /src/rules/ directory.

Then we can write a core loop to apply these rules to facts output by the MIR dump. If we are left with errors in the errors table, then we have violated a borrow-checking rule. This loop applies rules, derives facts, ignores duplicate facts, and stops when no additional facts can be derived.

1pub fn run_to_fixed_point(2    client: &mut Client,3    rules: &[Rule],4) -> Result<Evaluation> {5    let mut rounds = 0;6    let mut facts_derived = 0;7
8    loop {9        let mut facts_derived_this_round = 0;10
11        for rule in rules {12            facts_derived_this_round += rule.apply(client)?;13        }14
15        if facts_derived_this_round == 0 {16            return Ok(Evaluation {17                rounds,18                facts_derived,19            });20        }21
22        rounds += 1;23        facts_derived += facts_derived_this_round;24    }25}

These are the core pieces needed to implement a borrow checker. I would encourage you to read the source code for yourself and see how things are threaded together.

Conclusion

Rust’s borrow checker often feels opaque, but it is much simpler at its core. Datalog uses a much more efficient implementation of this strategy (semi-naive evaluation), but the core principle is the same. Large programs can generate many facts and recursive joins, and PostgreSQL is not the right execution engine for a production compiler.

Nevertheless, it’s an effective way to break down the borrow checker into simple rules to reason through when writing code.