nikomatsakis / borrowck

Modeling NLL and the Rust borrowck
Apache License 2.0
75 stars 12 forks source link

Slightly-too-long lifetime for Loan inferred #18

Open alexanderjsummers opened 6 years ago

alexanderjsummers commented 6 years ago

In the following code, it doesn't seem correct that the first Loan struct computed includes the line START/6 - it seems that that value of list is dead by that point, and the lifetime of the borrow on x shouldn't extend beyond the penultimate statement.

struct List<+> {
  value: 0,
}

let x: List<()>;
let y: List<()>;
let list: &'list mut List<()>;
let v: &'v mut ();

block START {
    x = use();
    y = use();
    list = &'b1 mut x;
    v = &'b2 mut (*list).value;
    list = &'b3 mut y;
    use(v);
    use(list);
}

//  Loan {
//      point: START/2,
//      path: Var(Variable { name: "x" }),
//      kind: Mut,
//      region: {START/3, START/4, START/5, START/6} }
//  Loan {
//      point: START/3,
//      path: Extension(Extension(Var(Variable { name: "list" }), FieldName { name: "*" }), FieldName { name: "value" }),
//      kind: Mut,
//      region: {START/4, START/5} }
//  Loan {
//      point: START/4,
//      path: Var(Variable { name: "y" }),
//      kind: Mut,
//      region: {START/5, START/6} }

//  assert 'list == {START/3, START/4, START/5, START/6};
//  assert 'v == {START/4, START/5};
//  assert 'b1 == {START/3, START/4, START/5, START/6};
//  assert 'b2 == {START/4, START/5};
//  assert 'b3 == {START/5, START/6};
nikomatsakis commented 6 years ago

Interesting. This does seem like a case where SSA-style rewriting would help; I wonder if there is another solution. The constraints that arise are roughly like this:

'b1: 'list @ START/2
'list: 'v @ START/3
'b2: 'v @ START/3
'b3: 'list @ START/4

Ignoring 'v, the first constraint would not ordinarily add START/6 into 'b1, because it would not be reachable from 'b1 (that is, ignoring 'v, 'b1 would not contain START/4). However, in this case, we wind up adding START/4 and START/5 into 'b1 from 'v, which then forms a path from the borrow of 'b1 to START/6.

This is an interesting effect. I'm not sure how best to fix it.