21. Borrow Checker: Architecture & Axioms
The borrow checker operates as a highly specialized phase in the compiler pipeline. It relies on a hybrid model: it extracts a fact schema heavily inspired by Rust’s Polonius architecture, computes liveness via a fast hand-rolled dataflow pass, and then uses a declarative SMT (Z3) solver to resolve complex borrow conflicts (a departure from Polonius’s Datalog-based approach).
The Pipeline
- Parse: Source code $\rightarrow$ AST.
- CFG Extraction: Traverse the AST to build basic blocks and extract a specific set of “Base Facts”.
- Liveness Pass: Run a standard backward-liveness fixpoint algorithm to compute active ranges for all loans.
- SMT Verification (Z3): Feed the CFG facts and computed liveness into Z3 as axiomatic assertions. Z3 evaluates the model for conflicts.
- Diagnostics: Translate SAT results into errors.
Base Fact Extraction
The CFG traversal extracts mechanical facts that act as the raw input relations for the solver.
| Fact | Meaning |
|---|---|
loan_issued_at(L, N) | Loan L is created at node N (ref/mut ref expression) |
loan_killed_at(L, N) | The place targeted by L is mutated, moved, or explicitly dropped at N |
var_used_at(Var, N) | Variable Var is read or written at N (drives liveness) |
cfg_edge(N, N') | Control-flow edge between nodes |
place_of(L, P) | The memory place a loan targets (e.g., p.x) |
loan_kind(L, K) | The kind of loan: Shared, ReservedMut, or ActiveMut |
activated_at(L, N) | The node where a ReservedMut loan becomes ActiveMut (two-phase activation) |
ancestor_of(L1, L2) | Reborrow relationship (e.g., L2 was derived from L1) |
overlap(P1, P2) | Static structural overlap predicate between two places |
Liveness & Active Ranges
Computing liveness using unconstrained SMT quantifiers is computationally abusive. Instead, the compiler pre-computes the active range of every loan.
The CFG pass uses a standard backward-liveness worklist algorithm driven by the var_used_at and loan_killed_at facts. The output of this pass is a set of ground facts: ActiveLoan(L, N), marking every exact node where a loan is alive.
These ground facts are directly asserted into the Z3 solver, completely relieving it of the burden of discovering graph reachability.
Z3 Conflict Resolution & PointsTo
Z3 is used strictly for evaluating complex logical overlap, ancestor/reborrow rules, and two-phase borrow activation.
Crucially, to accurately catch overlapping mutable borrow conflicts, the compiler asserts the PointsTo relation across the entire active range of the loan, not just at its creation node:
# The compiler emits this ground truth for Z3:
for L in loans:
for n in active_range(L): # Every node where ActiveLoan(L, n) holds
assert PointsTo(L, place(L), n)The solver evaluates the conflict axiom by checking overlap at each active node. Instead of an existential query searching for a violation, the compiler asserts the safety rule as a universal constraint:
∀ L1, L2, N, P1, P2:
PointsTo(L1, P1, N) ∧ PointsTo(L2, P2, N) ∧
overlap(P1, P2) ∧
ActiveLoan(L1, N) ∧ ActiveLoan(L2, N) ∧
(kind(L1) == ActiveMut ∨ kind(L2) == ActiveMut) ∧
L1 ≠ L2
⇒ (AncestorOf(L1, L2) ∨ AncestorOf(L2, L1))If the SMT solver returns SAT, it means the constraints hold for all active nodes and the program is Safe. If it returns UNSAT, a real, physical conflict occurred because two unrelated mutable loans overlapped at the same active node, violating the universal axiom. The solver’s UNSAT core (or a subsequent negated query) is then used to extract the exact conflicting loans for the diagnostic engine.