Handle borrows of unions in NLL

[KiChjang]

This is a small addition to RFC2094 so that we can handle unions as outlined in RFC1444.

Rendered

[arielb1]

This is vague ("if a borrow contains a union field"), and doesn't look like the right place to specify borrows of union fields.

[arielb1]

I think the right place to specify the handling of unions is the place describing

Accessing an lvalue LV

And I think we can write something as follows

• there is a loan for the path lvalue;
  • so: writing a path like a.b.c is illegal if a.b.c is borrowed
• there is a loan for some prefix of the path lvalue;
  • so: writing a path like a.b.c is illegal if a or a.b is borrowed
• lvalue is a shallow prefix of the loan path
  • shallow prefixes are found by stripping away fields, but stop at
    any dereference
  • so: writing a path like a is illegal if a.b is borrowed
  • but: writing a is legal if *a is borrowed, whether or not a
    is a shared or mutable reference
• the loan path has a shallow prefix <base>.<field1> that accesses a field of a union, and lvalue has a prefix of the form <base>.<field2> for a different field with the same base union.
  • so: if a.b is a union with distinct fields x and y, shallowly accessing a path a.b.x.c is illegal if a.b.y or a.b.y.s is borrowed. There <base> is a.b, <field1> is y and <field2> is x.
  • but: unless a.b.x is also a union, it is legal to access the a.b.x.c is legal if a.b.x.d is borrowed, because the same union field is used in both borrows.
  • the prefix of lvalue can be an arbitrary prefix - if a.b.y.s is borrowed, then it is illegal to shallowly access *(*a.b.x.c).t.

And on the supporting section:

• the loan path has a supporting prefix <base>.<field1> that accesses a field of a union, and lvalue has a prefix of the form <base>.<field2> for a different field with the same base union.
  • so: if a.b is a union with distinct fields x and y, deeply accessing a path a.b.x.c is illegal if a.b.y, a.b.y.s, or (in contrast with shallow accesses, and as long as both dereferences are of a &mut T) *(*a.b.y.s).t is borrowed. There <base> is a.b, <field1> is y and <field2> is x.

[KiChjang]

@arielb1 So from the union RFC, we have this property:

any borrow conflicting with a borrow of the union (including a borrow of another union field or a borrow of a structure containing the union) will produce an error.

In your example, that would also mean that a also cannot be borrowed, I.e. we need to add in additional conditions as follows:

• the loan path has a shallow prefix <base>.<field1> that accesses a field of a union, and lvalue has a prefix of the form <base>.<field2> for a different field with the same base union, or <base> is in the form of <prefix>.<union> where <union> is a union and its field accesses, and lvalue is a prefix of <prefix>.

[KiChjang]

Disregard my previous comment, the case that I was concerned about is covered by the "lvalue is a shallow prefix of the loan path" rule.

[KiChjang]

Updated the text to display a more correct version of handling union fields.

[petrochenkov]

Specifying borrowing errors through loan path "intersection" seems significantly more complex than recursive definition "borrow<'a>(prefix.field) -> borrow<'a>(prefix) && borrow<'a>(prefix.siblings), repeat until there prefix is empty".

[petrochenkov]

Oh my.
rust-lang/rust#45157

[nikomatsakis]

OK, sorry for coming late to the party. I finally carved out some time to read these changes. I agree that these sound roughly correct. I was, however, curious if we could frame this check in a more generic way -- essentially, the key question we are testing here is whether two paths are "disjoint" (i.e., refer to distinct memory).

I was thinking we could frame this in terms of some inference rules. For fun, I typed these up in Prolog, and you can try them out here. The rules are basically like this:

/* Two distinct variables are disjoint */
disjoint(var(V0), var(V1)) :- V0 \= V1.

/* Two paths `p.f` and `p.g` are disjoint
 * if the fields `f` and `g` are disjoint. */
disjoint(field(P, F0), field(P, F1)) :- disjoint_fields(F0, F1).

/* Two paths `p.f` and `q` are disjoint
 * if `p` is disjoint from `q`. */
disjoint(field(P0, _), P1) :- disjoint(P0, P1).
disjoint(P0, field(P1, _)) :- disjoint(P0, P1).

The rules for disjoint fields are then:

/* Two distinct fields in the same struct are disjoint. */
disjoint_fields(F0, F1) :-
    type_of(F0, S),
    type_of(F1, S),
    is_struct(S),
    F0 \= F1.

/* Fields declared in two distinct types are disjoint. */
disjoint_fields(F0, F1) :-
    type_of(F0, S0),
    type_of(F1, S1),
    S0 \= S1.

This seems to behave like I expect -- I included a number of examples in the link above, including rust-lang/rust#45157 (that's the last example, I believe). When I run them, they seem to yield true/false as I expect. =)

What I like about this formulation is that it scales quite readily to supporting fields in traits -- we simply have to make the disjoint_fields predicate line up. I also like that it's declarative.

I'm not proposing that we necessarily implement the rules like this, in any case, but I think it might be a useful way to specify them. I'm not sure yet if this PR is equivalent to the rules I wrote above -- I suspect it is, but I ran out of my quota allotted to reading and thinking here and have to go and get ready for Rust Belt Rust! =)

EDIT: (Incidentally, turning this intuition regarding union into borrowck rules is a bit harder than I expected. It's kind of the inverse of the existing rules, which specify what is illegal, since the disjoint formulation come at it from the POV of specifying what is legal. It seems like a better way to go, but it's making my head hurt. Perhaps in the morning.)

[nikomatsakis]

A meta question: should we keep updating the RFC here, or in the nll-rfc repo? I think I'd prefer to iterate on the nll-rfc repo (which I could move to rust-lang-nursery or something), just because these are narrow questions and I don't know that we need to use the full RFC repo. And we are still tracking some other unresolved questions there as well. But I'm kind of open to either.

[KiChjang]

Superseded by #2174.