Pls explain this code why am getting error

1 
#![allow(warnings)]
fn main() {
    let mut z = 4;
    let mut x = &mut z;

    let mut s = 44;
    let mut d: &mut u32 = x;

    let mut f = 4444;
    let mut q = 444;

    d = &mut f;
    x = &mut q;

    println!("{}", q);
    println!("{}", d);
}

(Playground)

2 Likes
3

Looks like the compiler is not clever enough to understand (in its borrow check) that the first assignment let mut d: &mut u32 = x; is annulled by the second assignment d = &mut f, although it states the value of the first assignment is never read (that's a different check tho).

Maybe someone with more intimate knowledge of the compiler borrow checks can shed some light on the "why".

Replacing the first assigment by let mut d: &mut u32; removes the compiler error.

4

I want to know what is the compiler thinking process at that point

let mut d : &mut u32 = x ;

5

i have reduced the code tho this:

fn main() {
    let mut z = &mut 4;

    let mut d: &mut u32 = z;

    let mut q = 444;

    z = &mut q; // mutable borrow of q

    println!("{}", q); // immutable borrow of q

    println!("{}", d); // z still live here which is ref to q
}

and it still gives the same error:

i can notice that d is mutable ref to x and x is mutable refer to q
so at the time when we println!("{}" q) , we are borrowoing imutabley a variable that is borrowed mutably.

6

The current borrow checker treats the code similarly to this:

    let mut q = 444;
    let x = &mut q;
    let d: &mut u32 = x;
    println!("{}", q);
    println!("{}", d);

Due to how lifetimes and borrowed places are propagated. (It is correct for the above code to be rejected, as d is an exclusive reference that points to q on the last two lines, so accessing q cannot be allowed.)

/* @  3 */    let mut z = 4;
/* @  4 */    let mut x = &mut z;
/* @  5 */
/* @  6 */    let mut s = 44;
/* @  7 */    let mut d: &mut u32 = x;

Call x a &'0 mut u32 and call d a &'1 mut u32. Uses of '1 keep '0 active because '0: '1 is a requirement of the assignment.

/* @ 12 */    d = &mut f;
/* @ 13 */    x = &mut q;
/* @ 14 */
/* @ 15 */    println!("{}", q);
/* @ 16 */    println!("{}", d);

f is borrowed for '1 and q is borrowed for '0 as variables do not change type. As '1 is active on line 13, uses of d (which has '1 in its type) keep the borrow of q (associated with '0) active. This causes q to still be exclusively borrowed on line 15.

Unlike my snippet at the top, the borrowed places reachable from d and x are no longer the same.[1] So a different sort of analysis could soundly accept the OP code.

This seems like a good time to suggest the following video that gives an overview of how the current borrow checker (NLL) works and how the next borrow checker (Polonius) works.

Polonius accepts the OP. Let's walk through the OP in Polonius terms and see if it makes sense why.

There are three loans in the OP code, and an assignment where a loan can "flow" somewhere else.

/* @  4 */    let mut x = &mut z;       /* Loan L1 */ /* '0: { L1 } */
// ...
/* @  7 */    let mut d: &mut u32 = x;                /* '1: { L1 } */
// ...
/* @ 12 */    d = &mut f;               /* Loan L2 */ /* '1: { L1, L2 } */
/* @ 13 */    x = &mut q;               /* Loan L3 */ /* '0: { L1, L3 } */

After this point, only d and q are used.

/* @ 15 */    println!("{}", q); // Access of `q` which is loaned by `L3`
/* @ 16 */    println!("{}", d); // Use of `'1` which has origins `L1, L2`

The access of q on line 15 is an error if L3 is alive. Is it alive? The only loan-carrying variable alive after this point is d, which has the origin set { L1, L2 }. So no, L3 is not alive, and the access of q is not an error.

I think the only tricky thing here is a bit of flow sensitivity: We only added L1 to '1 on line 7 because L3 didn't exist yet / was not part of '0 yet.

  1. and don't overlap more generally ↩ī¸Ž

4 Likes