Liveness annotation in MIR

When a reference is no longer used we say that it is dead. How is that noted in the MIR? For example: fn main() { let mut x = 32; let _y = &x;
x += 1; print!("{}", x); } y is 'dead' so mutating of x is allowed. Looking at the MIR in the playground, there is 'StorageLive' when y is created but a 'StorageDead' is after the mutation of x is allowed. How is the 'deadness' noted for the borrow checker to allow the mutation? I am learning ... patience appreciated :slight_smile:

The liveness of references is internal information of the borrow checker and not visible in MIR.

but a 'StorageDead' is after the mutation of x is allowed

Compared to borrow checker, StorageLive/StorageDead is much more conservative. The reason is that borrow checker will employ various dataflow analysis (you can explore it more here), while StorageLive/StorageDead are, I assume, mostly generated according to the lexical scope. And I guess they do not rely on each other currently.

If we put parentheses around { let _y = &x; }, you can see the StorageDead occurs earlier.