Skip to content

Unsound restoration to E capability after expiry of conditional borrow #137

@zgrannan

Description

@zgrannan

For the following code:

struct G {value: u32}
struct F {f: G, g: G}

fn test6(y0: F, z: F, b: bool) {
    let mut y = y0;
    let mut z = z;
    let mut x;
    if b { // bb1
        x = &mut y;
        consume_F(z);
    } else { // bb2
        x = &mut z;
        consume_F(y);
    }
    // bb3
    let f = &mut x.f;
    // StorageDead(f)
    // StorageDead(x)
    // StorageDead(z)
    // StorageDead(y)
}

At the end of bb1 we have: {y: 0, z: W}, and at the end of bb2 we have
{y: W, z: 0}, at bb3 these are joined so we have {y: 0, z: 0}. Then,
when x expires, capabilities to y and z are both upgraded to E
due to how PCG handles the expiry of mutable borrows. The current rule
is:

When a borrow blocking place p dies, if no other borrow (e.g. a
conditionally-created borrow under another path) is blocking p, then
the capability to p is restored to E.

But this rule is unsound: y is moved-out in bb2, so it cannot have E capability in bb3

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions