RustLog

Where Polonius is different from NLL

by H. Haldi and M. Algelly

Report of the 9th of May 2023

A small recall

/*0*/ let mut x: u32 = 22;
/*1*/ let y: &{L1} u32 = &{L1} x /* Loan L1 */;
/*2*/ x += 1;
/*3*/ print(y);

x has origin L1
y has the same origin L1
line 2 modifies the path x, so violates the terms of the loan L1
y is live on line 2 and its type includes L1
- type of y is &{L1} u32

→ ERROR

Example where Polonius is different from NLL

fn get_or_insert(
    map: &mut HashMap<u32, String>,
) -> &String {
    match map.get(&22) {
        Some(v) => v,
        None => {
            map.insert(22, String::from("hi"));
            &map[&22]
        }
    }
}

Error

error[E0502]: cannot borrow `*map` as mutable because it is also borrowed as immutable
  --> src/main.rs:55:13
   |
50 |     map: &mut HashMap<u32, String>,
   |          - let's call the lifetime of this reference `'1`
51 | ) -> &String {
52 |     match map.get(&22) {
   |           ------------ immutable borrow occurs here
53 |         Some(v) => v,
   |                    - returning this value requires that `*map` is borrowed for `'1`
54 |         None => {
55 |             map.insert(22, String::from("hi"));
   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ mutable borrow occurs here

More explicit code

fn get_or_insert<'a>(
    map: &'a mut HashMap<u32, String>,
) -> &'a String {
    match HashMap::get(&*map, &22) { // Loan of the place *map
        Some(v) => v,
        None => {
            map.insert(22, String::from("hi"));
            &map[&22]
        }
    }
}

However, in NLL, the lifetime of this loan is 'a, and not a set of line numbers.

In NLL, lifetimes can be either:
- a set of line numbers
- a named lifetime (e.g. 'a), which includes all the lines of the function

What Polonius does

fn get_or_insert<'a>(
    map: &'a mut HashMap<u32, String>,
) -> &'a String {
    match HashMap::get(&*map, &22) { // Loan L1
        Some(v) => v,
        None => {
            map.insert(22, String::from("hi")); // Here
            &map[&22]
        }
    }
}

v has the loan L1 in its type
However, v is not live here

→ Mutable borrow on *map is allowed

Starting with inference rules

Basic rule

Let’s define formally, using datalog syntax, how Polonius detects error:

error(P) :-
  invalidates(P, L),
  loan_live_at(L, P).

where P is a program point (statement) and L is a loan.

Invalidates

Invalidates are input facts that will be generated by the compiler.
A point invalidates a loan if:
- For a shared loan of a place P, the point modifies P
- For a mutable loan of a place P, the point accesses P

Loan live at

The rule loan_live_at(L, P) is much more complex.

Check if:
- the region of the loan is live at that point
- and if the region requires the terms of the load to be enforced at that point.

I.e. If the terms of the loan L are invalidated at point P, then the region is invalidated.