Why does the assigment to a reference kill the loan that was previous assigned to the reference?

help
1

Consider this example:

fn main() {
    let mut data = vec![1, 2, 3];
    let mut x = &data[0];
    println!("{}", x); // #0
    data.push(4);  // #1
    x = &data[3]; // #2
    println!("{}", x); // #3
}

If there were no #2, #1 would cause the borrowing checker error. This example is a bit like the example in 2094-nll - The Rust RFC Book

let mut foo: T = ...;
let mut bar: T = ...;
let mut p: &T;

p = &foo;
// (0)
if condition {
    print(*p);
    // (1)
    p = &bar;
    // (2)
}
// (3)
print(*p);
// (4)

The RFC comments on this example as:

The key point of this example is that the variable foo should only be considered borrowed at points 0 and 3, but not point 1.

However, it seems there is no wording that says why foo is not considered to be used at (1). If completing the example as the following like this:

fn main() {
    let mut foo = 0;
    let mut bar = 1;
    let mut p: & /*'p*/ i32;
    //      --
    p = &/*'foo*/ foo;
    //   ----
    if false {
        println!("{}",*p);
        // (1)
        foo = 2;
        p = &/*'bar*/ bar;
        //   ----
    }
    //foo = 2;
    println!("{}",*p);
}

foo = 2; won't cause the borrowing checker error. That implies, the loan ('foo,shared, foo) is not in the point (1) in the CFG, so, it's not considered as a relevant borrowing for the access foo = 2.

The rules for computing loans in the scope are:

For a statement at point P in the graph, we define the “transfer function” – that is, which loans it brings into or out of scope – as follows:

  • any loans whose region does not include P are killed;
  • if this is a borrow statement, the corresponding loan is generated;
  • if this is an assignment lv = <rvalue>, then any loan for some path P of which lv is a prefix is killed.

I don't think the third bullet is saying about p = &/*'bar*/ bar, it intends to say the loan for some path P of which p is prefix. For the loan ('foo,shared, foo), it is not the case.

So, the relevant bullet should be the first one. However, NLL does not define why the region of the loan ('foo,shared, foo) does not include (1)? How to understand this point?

2

the assignment kills the loan of the lhs, in this example, it means p (i.e. & /*'foo*/ foo from (0)), and foo is a prefix of foo itself, so it is killed.

this talk on polonius by niko explains the borrow checker very well, like the concept of paths, loans, etc, I highly recommend you to watch it:

3

The borrowing &'foo foo generates the loan ('foo, shared, foo) whose lvalue is foo, the assignment to p, by executing the wording, is any loan for some path P of which p is a prefix is killed. It's abviously that the ('foo, shared, foo) whose path is foo and p is not a prefix of foo.

4

you are right, I misread your question.

the reason the assignment to p makes the code compile is not because it "kills" the loan, but that it changes the region of p's liveness.

specifically, by control flow analysis, inside the if condition { ... } branch at (1), p is NOT live, thus the access to the path foo = 2 is not an error, because it only violated a dead (not-live) loan.

it is described in the section of "liveness", quoting:

One key ingredient to understanding how NLL should work is understanding liveness. The term “liveness” derives from compiler analysis, but it’s fairly intuitive. We say that a variable is live if the current value that it holds may be used later.

it is also mentioned in the "rough outline of our solution" section:

Intuitively, in the new proposal, the lifetime of a reference lasts only for those portions of the function in which the reference may later be used (where the reference is live, in compiler speak).

1 Like
5

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.