Borrow Checker Logic Question

help
1

Hi everyone,

I have a question about how the borrow checker works to figure out that borrows don't last long enough. I have some sample code here that just pushes a reference onto a vector.

fn push_value<'a>(
    array: &mut Vec<&'a u32>,
    value: &'a u32
) {
    array.push(
        value
    );
}

fn main() {
    let mut reference_array :Vec<&u32> =
        vec![];

    {
        let value1 =
            10;

        push_value(
            &mut reference_array,
            &value1
        );
    }

    println!(
        "{}",
        reference_array[0]
    );
}

When I compile the code, I get:

15 | let value1 =
| ------ binding value1 declared here
...
20 | &value1
| ^^^^^^^ borrowed value does not live long enough
21 | );
22 | }
| - value1 dropped here while still borrowed
...
26 | reference_array[0]
| --------------- borrow later used here

Now, I know this is the correct error, but how on Earth does the borrow checker know that value1 and reference_array are intertwined? If I comment out the code that pushes the value, I get the same error.

Thanks.

2

for an explanation of the formulation of the borrow checker, I highly recommend you to read:

https://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/

3

That's because all of the information that the compiler is using is in the function signature. You called

        push_value(
            &mut reference_array,
            &value1
        );

and therefore, the type checker knows that reference_array must be a Vec<&'a u32> (for some lifetime 'a) and that &value1 must be (or coerce to) a &'a u32. Then the borrow checker looks at whether value1 will actually live long enough, or reference_array short enough, for 'a to mean something non-contradictory.

More abstractly: The part of your program that matters to this question is how the multiple uses of one lifetime variable 'a relate to each other. That's what makes the connection between different function arguments that the borrow checker then checks.

If you had not used the same lifetime variable twice, then push_value wouldn't care about how it was called, but the push() in its body wouldn't compile.

2 Likes
4

This video might be a good watch for you (and not really long), IIRC it also explains well how the type signatures of functions are essential to borrow checking, and it looks like the main example being discusses is almost identical to the code you’ve been looking at:

1 Like
5

In broad strokes, the borrow checker

  • Looks at the uses of all values to figure out when lifetimes must be valid
  • Uses those to figure out how[1] and for how long borrows of variables[2] last[3]
  • Looks at the uses again and makes sure each use doesn't conflict with a borrow

For example it's ok to copy something which is shared-borrowed, but it's not ok to overwrite something that's exclusive-borrowed or drop something that's borrowed in any way.

fn push_value<'a>(array: &mut Vec<&'a u32>, value: &'a u32) {

The signature says that *value must be borrowed for 'a -- it must remain borrowed for however long the lifetime 'a is valid. Moreover, the type of the Vec must be exactly Vec<&'a u32>. This effectively means that 'a must remain valid wherever the Vec is used.

    {
        let value1 = 10; // L1
        push_value(&mut reference_array, &value1); // L2
    } // L3

    println!("{}", reference_array[0]); // L4

So the borrow of value1 begins on L2 and lasts for whatever the lifetime in the type of reference_array is; let's call it 'r. reference_array is used on L4, so 'r must remain valid from L2 through L4. That means value1 is still shared-borrowed on L3.

But value1 drops at L3. That's a use of value1 that's incompatible with being borrowed.

  1. exclusive or shared ↩︎

  2. and other places like fields, dereferences, ... ↩︎

  3. usually the same as some lifetime, but it can be shorter in some circumstances which I'll ignore in the rest of this post ↩︎

6

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.