The borrow checker

References (&T, &mut T) let a function read or change a value without copying it and without owning it. They are only safe if nothing frees, moves or changes the value behind a reference while it is in use. Larva's borrow checker proves that for every function, before any code is generated. It works on Larva IR, not on a source language: whatever language wrote the program, the same checker runs over the same control-flow graph.

For the language side (what &x and &mut x mean in Antril, and examples), see References and the borrow checker.

The code is Larva.IR/Analysis/BorrowChecker, with MoveAnalysis, LoanAnalysis, Liveness, Dataflow, Location and BorrowError.

What it proves

The checker follows the model of Rust's non-lexical-lifetime borrow checker, adapted to Larva's types. For each function it proves five things:

It adds two rules for objects, which can be reached through many handles at once:

• Outside an unsafe function, a gc handle gives read-only access, except to the fields of a class (a struct marked Mutable), which may be assigned by value.
• No field of a class may be borrowed, shared or exclusive: another handle could change it at any time. The one exception is a shared borrow passed straight into the call that ends its block (how generic code boxes a field of type T); it lives only for that call, like a read.

unsafe functions may write through any gc handle and dereference raw pointers; the other rules still apply to them.

Where it runs

 frontend --HIR--> lowering --IR--> type check --> region check --> borrow check --> object --> link ...
                                                                    (per function, in parallel)

The checker runs after the type checker and (in arena modes) the region checker, on IR that is known to be well typed. Generic functions are checked once, before they are instantiated. Each function is checked on its own: a call is trusted to do what its signature says. BorrowChecker.Check(module) checks all the functions of a module on as many threads as there are processors and returns the errors in function order.

Checking IR rather than source has a cost and a gain. The cost: the checker sees temporaries and lowered constructs (a foreach loop's hidden index, a constructor's object header), so lowering passes must produce code it accepts. The design document records such cases: generic parameters lowered with a new constraint, Unborrowed, so the checker no longer assumed a T could carry a borrow; method calls on a value evaluating their arguments before borrowing this. The gain: one checker for every language, and it checks exactly the code that will run.

The analyses

The checker walks every reachable block once, carrying two states forward through its statements:

                Dataflow.Forward (fixed point over the CFG)
               /                                          \
   MoveAnalysis: places that may be               LoanAnalysis: which loans each
   uninitialized, and why/where                   local's value may carry
               \                                          /
                 checks at each statement and terminator
                 (active loans = loans held by locals live at this point: Liveness)

Points

A point in a function is a Location: block and index, printed bb3[1]. A block's terminator sits at index Statements.Length. Every message names points this way, and every check runs at a point.

Initialization and moves: MoveAnalysis

MoveAnalysis is a forward dataflow analysis whose state, MoveState, is the set of places that may be uninitialized, each with its origin (UninitOrigin: never initialized, moved, storage dead, dropped, and the location where that happened).

• At entry every local except the arguments is uninitialized.
• A write initializes its place. Writing a field of an uninitialized struct splits the entry into its sibling fields, so a struct can be initialized field by field.
• A move of a non-Copy value out of a place reachable without * or [i] marks it moved. Moving a Copy value is a read.
• StorageDead and drop mark their place dead or dropped.
• At a join the states are united: a place uninitialized on any path is uninitialized after.
• On an exception edge, a call's arguments are gone but its destination was not written.

The state is built for speed: whole locals live in an array, places with projections in a small map per local, and both are copied only when one copy changes. The lowering reuses the same analysis (with a "must" variant that intersects at joins) to decide where reference-counted handles are released, and whether a drop needs a flag.

Loans: LoanAnalysis

Every &place or &mut place statement creates a Loan: an id, its location, the borrowed place and whether it is mutable. LoanAnalysis tracks, for each local, which loans its current value may carry (LoanState.Held):

• r = &mut c gives r the new loan. A reborrow through a reference (&(*r).0) also keeps the original loans alive.
• Copying or moving a value that contains references passes its loans along; intrinsics never do (they return numbers or raw pointers).
• A call's result may carry the loans of its reference arguments, when the result's types could point into what those loans borrowed. Types decide: a &[u16] cannot point into a struct of numbers.
• A whole-local write replaces the loans it held; a partial write adds to them. StorageDead forgets them.

Liveness: when a loan ends

Liveness is a backward analysis: a local is live at a point if its current value may still be read. A loan is active at a point only when some local that holds it is live there. That is what makes lifetimes non-lexical: a reference stops borrowing after its last use, not at the end of its scope.

Counter c;
&mut Counter r = &mut c;
r.n = 1;
c.n = 2;    // fine: r is not used again, so its loan has ended

The checks

At each statement and terminator, with the states for that point, the checker classifies every place touched as an access: Read, Move, BorrowShared, BorrowMut, Write, StorageDead or Drop. Then:

1. Evaluating a place reads every reference it goes through and every index local: those must be initialized.
2. A read, move or borrow needs its place initialized (UseOfMoved, UseOfUninitialized, UseAfterFree).
3. A move must not go through * or [i].
4. A write or &mut checks mutability along the path: through &mut, *mut or (in unsafe code) gc, the pointer decides; through a box, the owner's mutability still applies; at the root, the local must be mut. Writing an uninitialized local is its initialization, not a second assignment.
5. Every active loan whose place overlaps the accessed place is a conflict, unless both are reads (or the loan is shared and the access only reads or borrows shared). Places overlap when one is a prefix of the other; two index projections are assumed to overlap. Overwriting a reference does not touch what a reborrow through it points at.
6. At return, no loan held by _0 may borrow a local of the function (places behind a non-owning pointer are fine: they belong to someone else). The same holds for a thrown value.
7. StorageDead of a local still borrowed is "does not live long enough".

Each error is reported once per point, kind and message.

Errors

Places are printed in IR form with source names substituted for locals (c.0 is field 0 of the local named c). The messages a frontend can avoid entirely (a copy of a non-Copy type) mostly show up when IR is written by hand.

Source positions

The checker finds errors in IR, but people read source. So the lowering records, for every IR statement, the source position of the HIR statement it came from (FunctionBuilder.Position fills IrFunction.Positions; see Larva IR). When a function has positions, BorrowChecker.Check does two things to each error:

• Source becomes the position of the failing statement (or the nearest earlier statement in its block that has one);
• every at bbN[i] in the message becomes on line N.

A BorrowError with a source prints as file(line,column): error[Kind]: message; without one, as error[Kind]: message followed by --> function bbN[i]. With warn, Severity turns into warning.

Positions are kept in memory only. An object file (.lvo) does not carry them, so errors found later in a linked program, or in IR written by hand, use block names.

An example

This program, conflict.ant, borrows c exclusively, then writes c while the borrow is still used (it is a whole file, but a fence for fragments: with the default borrowcheck: off its references would not compile):

import System;

into namespace Borrows
{
	public value Counter
	{
		public:
			i32 n;
	}

	Main()
	{
		Counter c;
		&mut Counter r = &mut c;
		c.n = 1;
		r.n = 7;
		Console.WriteLine(c.n);
	}
}

Its Main in IR:

fn Borrows.$Module.Main() -> () {
    let mut _0: ();             // return
    let mut _1: Borrows.Counter;// c
    let mut _2: &mut Borrows.Counter;// r
    let mut _3: ();

    bb0: {
        _1 = filler Borrows.Counter;
        _2 = &mut _1;
        _1.0 = const 1_i32;
        (*_2).0 = const 7_i32;
        _3 = System.Console.WriteLine$39(copy _1.0) -> bb1;
    }

    bb1: {
        return;
    }
}

and its positions:

The loan is created at bb0[1] and held by _2. At bb0[2], _2 is live (it is read at bb0[3]), so the loan is active; the statement writes _1.0, which overlaps the loaned place _1. That is a ConflictingBorrow at bb0[2], reported on line 15, with the loan's bb0[1] turned into "line 14":

$ larva build --check --borrowcheck enforce conflict.ant
conflict.ant(15,3): error[ConflictingBorrow]: cannot assign to `c.0` while it is borrowed (mutable borrow of `c` on line 14)

(Larva prints the full path of the file; it is shortened here.) Without positions, the same error reads:

error[ConflictingBorrow]: cannot assign to `c.0` while it is borrowed (mutable borrow of `c` at bb0[1])
   --> Borrows.$Module.Main bb0[2]

Moving c.n = 1; after r.n = 7; fixes it: _2 is dead after its last use, so the loan is no longer active when c is written.

Several kinds at once, in errors.ant (the Counter above, plus):

public class Cell
{
	public:
		i32 n;
}

Bump(&mut i32 n)
{
	n = n + 1;
}

Leak() : &i32
{
	i32 x = 1;
	return &x;
}

Main()
{
	Counter c;
	&mut Counter a = &mut c;
	&mut Counter b = &mut c;
	a.n = 1;
	b.n = 2;

	&Counter s = &c;
	c.n = 3;
	Console.WriteLine(s.n);

	Cell cell = new Cell();
	Bump(&mut cell.n);
}

$ larva build --check --borrowcheck enforce errors.ant
errors.ant(25,3): error[ReturnsLocalReference]: returns a reference to local `x` (borrowed on line 25)
errors.ant(32,3): error[ConflictingBorrow]: cannot borrow `c` as mutable while it is borrowed (mutable borrow of `c` on line 31)
errors.ant(37,3): error[ConflictingBorrow]: cannot assign to `c.0` while it is borrowed (shared borrow of `c` on line 36)
errors.ant(41,3): error[MutationThroughGc]: cannot borrow `(*cell).2` as mutable: fields of objects are read and written by value, never borrowed

The last one shows the object rule: cell.n is field 2 of the object (after the class id and the vtable), and an object's fields are never borrowed. Note that the frontend accepted all four; each was found on IR.

Modes

The checker has three modes (BorrowCheckMode):

Turning references off when the checker is off is deliberate: a program never uses references that nothing checked. The frontend learns the mode through its options ("borrows": false in the options a language pack receives).

Where the mode comes from

The first of these that says something wins:

1. --borrowcheck enforce|warn|off on larva build, larva run or larva lib;
2. borrowcheck: in the project's BUILD chunk;
3. this machine's default, larva config borrowcheck (stored in LARVA_CONFIG, else %APPDATA%/Larva/defaults.json, ~/.config/larva/defaults.json elsewhere);
4. the built-in default, off.

$ larva config borrowcheck
off
$ larva config borrowcheck warn
borrowcheck: warn
$ larva config borrowcheck
warn
$ larva config --unset borrowcheck
borrowcheck: off   (built in)

A project that turns it on for itself, with conflict.ant as its Program.ant (paths shortened in the output, as above):

queen 1.0;

chunk PROJ:
   name: Borrows,
   type: exe

chunk BUILD:
   borrowcheck: enforce,
   backend: x64

$ larva build
Program.ant(15,3): error[ConflictingBorrow]: cannot assign to `c.0` while it is borrowed (mutable borrow of `c` on line 14)
$ larva build --borrowcheck warn
Program.ant(15,3): warning[ConflictingBorrow]: cannot assign to `c.0` while it is borrowed (mutable borrow of `c` on line 14)
…\bin\Borrows.exe (x64 back end, entry Borrows::Borrows.$Module.Main)

Why off by default: references are an advanced feature, the checker adds time to every build, and most programs do not need them. The IR library's own default (CompilationOptions.Default) is enforce, which is what hand-written IR and tools get.

How builds run it

larva build (with or without --check):

1. compiles the sources to HIR, links HIR with the libraries, lowers the whole program to IR;
2. when the mode is not off, borrow checks the functions whose positions point into the program's own source files, skipping the libraries (they were checked when they were built); --timings shows the time as borrow check;
3. prints each error (as a warning in warn mode) and, in enforce mode, stops with exit code 1;
4. with --check, stops here and prints no errors (…).

When it goes on to build, the object step (Compiler.CompileObject) verifies the whole lowered program again: type check, region check and, in the same mode, the borrow checker over every function. A library built as a GC domain of its own (a dependency whose gc: differs) is verified with the IR's default, enforce.

larva lib stops at the frontend: it compiles a library to HIR, where the mode decides whether references are allowed, but it does not lower it, so the IR checker does not run.

In the editor

The language server (larva lsp) runs the same checker in the background, so borrow errors appear as you type:

1. After a document is analyzed, if its project's mode (BUILD, else this machine's default) is not off, the project has no dependency in another GC domain, and the analysis found no errors, a borrow check is scheduled.
2. It waits 400 ms. Each edit bumps a generation counter, and a check that started before the latest edit publishes nothing: typing never waits for it.
3. It compiles the project's sources as the editor has them (open documents with unsaved text included), links them with System.Core and the project's libraries, lowers the program, and checks the functions of the program's own files.
4. Each open document of the project gets its analysis diagnostics plus the borrow errors on its lines: severity error in enforce, warning in warn, source "borrow checker", code the error kind, and a range from the reported column to the end of the line.

Related checks

• The type checker runs first and always: it makes sure the borrow checker sees well-typed IR (and rejects raw pointer dereferences outside unsafe code).
• The region checker enforces the arena modes' rule that nothing from a region outlives it. It uses the same idea of tags following values, but for regions instead of loans, and it is always on in arena modes, whatever the borrow-check mode. See Larva IR.
• MoveAnalysis also drives code generation under reference counting (when a handle is released, whether a drop needs a flag), so the move rules the checker enforces are the same ones the generated code relies on.