Intro to Polonius

View From Borrow Checker

The most common borrow checker error comes from accessing a invalid memory location, which the borrow checker intends to prevent in compile time. We will present borrow checker's inner inferring process using Polonius as example. You could learn more about Polonius in this presentation. Before diving into how the borrow checker infers such errors, there are few technical terms we should know:

• path: A path P is an expression that leads to a memory location, for example:

let x = 10;
print!("{}", x); // access a local variable on the stack

let s : SomeStruct = SomeStruct{num = 10};
s.num = 6; // access a field of a path on the stack

• loan: A loan is a name for a borrow expression. It's associated with

  • A path which is borrowed.

  • A mode with which the path was borrowed, it could be either shared or mutable.

  For example:

let y = &x;

    Here, the loan is in shared mode since it's not a mutable     borrow and it's associated to the path x.

let p = &mut q;

    Here, the loan is in mutable mode since it's a mutable     borrow and it's associated to the path q.

The borrow checker will issue error message at some statement N if

• The statement N accesses a path P

• Accessing the path P would violate the terms of some loan L

• L is live

How exactly does the term of a loan mean? Well, for a shared loan of path P, modifying the path will violates the term of the loan, such as changing the value of an immutable reference. The following code will violate the term of a shared loan:

let num = 10;
let ref = #
ref = ref + 1; // error, violates shared loan term

Similarly, for a mutable loan, the borrow is exclusive, which means any access to the path P will will lead to violation. For example,

let mut x = 10;
let r = &mut x;
println!("{}", x); // error, reading variable x will violate mutable loan term
x = x + 1; // error, modifying variable x will violate mutable loan term
*r = 6;

However, if we comment out the last line, there won't be any loan violation:

let mut x = 10;
let r = &mut x;
println!("{}", x); // fine
x = x + 1; // fine

This happens because in the second case, the loan is not live.

Live Variables & Live Loans

For rust, Non-lexical lifetime (NLL) is adapted by borrow checker and have recently obtained a lot support in language features. We will throw out the following definition on lifetime (according to RFC):

• The lifetime of a value: corresponding to the span of time before that value gets freed (or, put another way, before the destructor for the value runs).

• The lifetime of a reference, corresponding to the span of time in which that reference is used.

Consider the former code example:

fn main(){
    let mut x = 10;
    let r = &mut x;
//      ^~~~~~~~~~ r is no longer live
    println!("{}", x); // fine
    x = x + 1; // fine
}

According to NLL, the reference r is already dead on line 3 because it will never be used afterwards. So we can access the path x without any error.

The definition for a live loan is that the reference created by the loan, or some reference derived from it, might be used later.

struct Foo{
    n : u32,
}
fn main(){
    let foo = Foo{y : 10};
    let x = &foo;        // loan L1
    let y = &x.n;        // loan L2
    // ...
    println!("{}", y);   // L1 and L2 are both live
}

In the above example, y is derived from L1 which is assigned to L2. Therefore on the println! statement, both loans are live.

How Polonius Reports Borrow Error

Let's look at the following erroneous code:

let mut x : u32 = 10;
let y : &u32 = &x;
x += 1;
println!("{}", y);

The code is wrong at line 3 because x is borrowed and is not supposed to change the value. The way the borrow checker detects this error in Polonius way is that it will first calculate the origin for each reference. Well, what is an origin?

An origin for a reference R is a set of loans indicating the loans R might have come from.

In the above example, y is derived from loan L1 on line 2, so the origin of y is L1.

Then, we return to the conditions where borrow checker will complain:

The borrow checker will issue error message at some statement N if

• The statement N accesses a path P

• Accessing the path P would violate the terms of some loan L

• L is live

On line 3, x += 1 modifies the path P leading to the value of x stored on program stack. Yet we know x is borrowed on line 2 with origin L1, which happens to have mutable term. So this will be a violation to the term of L1. We then need to verify whether L1 is live. According to previous section, the reference y is used on line 4, which is derived from L1. Therefore, L1 is live on line 3 and the borrow checker will return an error message.