borrow scopes should not always be lexical

[metajack]

If you borrow immutably in an if test, the borrow lasts for the whole if expression. This means that mutable borrows in the clauses will cause the borrow checker to fail.

This can also happen when borrowing in the match expression, and needing a mutable borrow in one of the arms.

See here for an example where the if borrows boxes, which causes the nearest upwards @mut to freeze. Then remove_child() which needs to borrow mutably conflicts.

https://github.com/mozilla/servo/blob/master/src/servo/layout/box_builder.rs#L387-L411

Updated example from @Wyverald

fn main() {
    let mut vec = vec!();
    
    match vec.first() {
        None => vec.push(5),
        Some(v) => unreachable!(),
    }
}

[metajack]

nominating for production ready

[nikomatsakis]

I would call this either well-defined or backwards-compat.

[nikomatsakis]

Examples from Jack

[09:57:06] https://github.com/mozilla/servo/blob/master/src/components/servo/layout/box_builder.rs#L387-L411
[10:02:06] servo/servo#435

[metajack]

The code got reorganized, but here is the specific appeasement of the borrow checker i had to do:

metajack/servo@5324cab

metajack/servo@7234635

[nikomatsakis]

After some discussion, it's clear that the real problem here is that the borrow checker makes no effort to track aliases, but rather always relies on the region system to determine when a borrow goes out of scope. I am reluctant to change this, at least not in the short term, because there are a number of other outstanding issues I'd like to address first and any changes would be a significant modification to the borrow checker. See issue #6613 for another related example and a somewhat detailed explanation.

[cscott]

I wonder if we could improve the error messages to make it more clear what's going on? Lexical scopes are relatively easy to understand, but in the examples of this issue that I've stumbled across it was by no means obvious what was going on.

[graydon]

just a bug, removing milestone/nomination.

[graydon]

accepted for far future milestone

[emberian]

triage bump

[nikomatsakis]

I've had some thoughts about the best way to fix this. My basic plan is that we would have a notion of when a value "escapes". It will take some work to formalize that notion. Basically, when a borrowed pointer is created, we will then track whether it has escaped. When the pointer is dead, if it is has not escaped, this can be considered to kill the loan. This basic idea covers cases like "let p = &...; use-p-a-bit-but-never-again; expect-loan-to-be-expired-here;" Part of the analysis will be a rule that indicates when a return value that contains a borrowed pointer can be considered not to have escaped yet. This would cover cases like "match table.find(...) { ... None => { expect-table-not-to-be-loaned-here; } }"

The most interesting part of all this is the escaping rules, of course. I think that the rules would have to take into account the formal definition of the function, and in particular to take advantage of the knowledge bound lifetimes give us. For example, most escape analyses would consider a pointer p to escape if they see a call like foo(p). But we would not necessarily have to do so. If the function were declared as:

fn foo<'a>(x: &'a T) { ... }

then in fact we know that foo does not hold on to p for any longer than the lifetime a. However, a function like bar would have to be considered as escaping:

fn bar<'a>(x: &'a T, y: &mut &'a T)

So presumably the escaping rules would have to consider whether the bound lifetime appeared in a mutable location or not. This is effectively a form of type-based alias analysis. Similar reasoning I think applies to function return values. Hence find ought to be considered to return a non-escaped result:

fn find<'a>(&'a self, k: &K) -> Option<&'a V>

The reason here is that because 'a is bound on find, it cannot appear in the Self or K type parameters, and hence we know it can't be stored in those, and it does not appear in any mutable locations. (Note that we can apply the same inference algorithm as is used today and which will be used as part of the fix for #3598 to tell us whether lifetimes appears in a mutable location)

Another way to think about this is not that the loan is expired early, but rather that the scope of a loan begins (typically) as tied to the borrowed variable and not the full lifetime, and is only promoted to the full lifetime when the variable escapes.

Reborrows are a slight complication, but they can be handled in various ways. A reborrow is when you borrow the contents of a borrowed pointer -- they happen all the time because the compiler inserts them automatically into almost every method call. Consider a borowed pointer let p = &v and a reborrow like let q = &*p. It'd be nice if when q was dead, you could use p again -- and if both p and q were dead, you could use v again (presuming neither p nor q escapes). The complication here is that if q escapes, p must be considered escaped up until the lifetime of q expires. But I think that this falls out somewhat naturally from how we handle it today: that is, the compiler notes that q has borrowed p for (initially) the lifetime "q" (that is, of the variable itself) and if q should escape, that would be promoted to the full lexical lifetime. I guess the tricky part is in the dataflow, knowing where to insert the kills -- we can't insert the kill for p right away when p goes dead if it is reborrowed. Oh well, I'll not waste more time on this, it seems do-able, and at worst there are simpler solutions that would be adequate for common situations (e.g., consider p to have escaped for the full lifetime of q, regardless of whether the q loan escapes or not).

Anyway, more thought is warranted, but I'm starting to see how this could work. I'm still reluctant to embark on any extensions like this until #2202 and #8624 are fixed, those being the two known problems with borrowck. I'd also like to have more progress on a soundness proof before we go about extending the system. The other extension that is on the timeline is #6268.

[toffaletti]

I believe I've run into this bug. My use-case and work-around attempts:

https://gist.github.com/toffaletti/6770126