Polonius Development

Context


Start with this program:

let mut x = 22;
let p: &u32 = &x;
x += 1;
drop(p);

In Rustc, plan is to first type-check (more-or-less) without regions, giving us types like &u32. We use this to create MIR.

In MIR, we create fresh region variables for every possible region, and we have a list of loans, one per borrow expression:

let mut x = 22;
let p: &'a u32 = &'b x; // Loan L0
x += 1;
drop(p);

For each loan, we know:
  • path that was borrowed (x)
  • kind of borrow (shared)
  • region of the borrow ('b)

By running a type-check, we can also deduce some things:

  • e.g., at the let p = … statement, 'b: 'a must hold

Why?

&'b u32 <: &'a u32 if
'b: 'a

Concept: Live regions

A live variable (in compiler parlance) is one whose current value that may be used later.

Definition: A variable x is live at some point P if:
  • there is some future point Q where the value of x is read
  • and there is a path from P → Q where x is not overwritten.

let x = 22;

// x is live here
read(x);

// x is dead here, current value is overwritten
x = 44;

// x is live here