[borrowck] mutable reads

[arielb1]

The current version of this RFC considers a mutable borrow to be the same as a read + a write. That is unsound - a mutable borrow invalidates immutable borrows of the deep contents, while a write + read only invalidates mutable borrows of the deep contents and borrows of the shallow contents. For example:

// set the scene
x = Some(0);
y = &mut x;
assert(Discr(*y) is Some);
z = &(*y as Some).0; // (*) this is an immutable borrow

// ... and then
t = &mut y;
**t = None;
// oops
use(z);

The borrow of y must conflict with the borrow at (*)

However, a read+write in that place should borrow-check:

t = &y; 
use(t);
y = &mut whatever;
// the borrow `(*)` is now "orphaned", so using it is ok.
use(z);

EDIT: This used to be this broken version, which doesn't actually work because y is not Copy.

t = y; 
y = &mut whatever;
// the borrow `(*)` is now "orphaned", so using it is ok.
use(z);

[nikomatsakis]

I'm trying to figure out exactly what your concern is.

The borrow of y must conflict with the borrow at (*)... However, a read+write in that place should borrow-check:

The first example (t = &mut y) does give me an error, in the prototype. However, the second example (t = y) also gives an error -- but that seems... appropriate to me.

The error arises because (*y as Some).0 is borrowed, and the borrow is live -- this means that reads of y are disallowed. Both t = &mut y and t = y are considered reads of y.

But in particular the second example seems like something we should not accept.. the fact that y is overwritten after t = y executes doesn't matter: if we accept t = y, we now have z (which is live and will be used) and t both pointing to overlapping things, right?

(As far as I can tell, the use of option is just a distraction here, so I modeled this using structs:

// // set the scene
// x = Some(0);
// y = &mut x;
// assert(Discr(*y) is Some);
// z = &(*y as Some).0; // (*)
//
// // ... and then
// t = &mut y;
// **t = None;
// // oops
// use(z);

struct Map { value: Value }
struct Value { }

let x: Map;
let y: &'_ mut Map;
let z: &'_ mut Value;
let t: &'_ mut &'_ mut Map;

block START {
  x = use();
  y = &'_ mut x;
  z = &'_ mut (*y).value;

  t = &'_ mut y; //! ERROR
  **t = use();
  use(z);
}

[arielb1]

I had a mistake there - I forgot that y is not Copy, so a use of it is actually a consume. I meant

// set the scene
x = Some(0);
y = &mut x;
assert(Discr(*y) is Some);
z = &(*y as Some).0; // (*)

// ... and then
t = &y; // A `read` of y
use(t);
y = &mut whatever; // A `write` to `y`
// the borrow `(*)` is now "orphaned", so using it is ok.
use(z);

The use of options just makes it clear there's an unsoundness.

[nikomatsakis]

OK, so, the mistake was partly mine: in my version, I accidentally changed z = &(*y).value to z = &mut (*y).value. If I change that back, then indeed I get both variants are accepted.

[nikomatsakis]

Proposed modification can be found in nikomatsakis/nll#13.

[arielb1]

Still need a fix on the RFC side.

[nikomatsakis]

@arielb1 indeed, I tagged it as such...