Copy propagation on "move" assignments introduces UB (using Miri/MiniRust semantics)

[RalfJung]

So far, we have a theory for what move could mean on function calls, but we don't have a clear idea what it could mean in assignments (#416). Turns out the two are tightly linked: this example compiles to the following MIR without optimizations:

fn src(_1: Foo) -> () {
    debug x => _1;
    let mut _0: ();
    let _2: ();
    let _3: &Foo;
    let _4: ();

    bb0: {
        _3 = &_1;
        _2 = escape(copy _3) -> [return: bb1, unwind continue];
    }

    bb1: {
        _4 = move_arg(move _1) -> [return: bb2, unwind continue];
    }

    bb2: {
        return;
    }
}

And the following with optimizations:

fn src(_1: Foo) -> () {
    debug x => _1;
    let mut _0: ();
    let _2: ();
    let mut _3: Foo;
    scope 1 (inlined escape) {
        let mut _4: *const Foo;
        let mut _5: *mut *const Foo;
    }

    bb0: {
        _4 = &raw const _1;
        StorageLive(_5);
        _5 = const {alloc1: *mut *const Foo};
        (*_5) = copy _4;
        StorageDead(_5);
        StorageLive(_3);
        _3 = move _1;
        _2 = move_arg(move _3) -> [return: bb1, unwind continue];
    }

    bb1: {
        StorageDead(_3);
        return;
    }
}

Miri semantics says the former program has UB (though I have not managed to actually executed that MIR in Miri, passing -O is not enough somehow), while the latter is fine. The latter is fine since _3 = move _1; ignores the move, and so the argument actually moved to move_arg is _3 and that argument gets protected for the duration of the call.

I assume we want to allow the transformation that removes the extra move (though I don't know if we currently perform such an optimization); that is very tricky: _1 might be accessed in various ways after the move (even if we consider a move to de-init memory, one can still write to it); if the argument moved to move_arg becomes an alias of _1 that can easily introduce conflicts.

[CAD97]

IIUC, move place in a function argument makes a new &mut retag as if passing &mut place, including protectors for the duration of the call, and then uninitializes the place after the call.

Would it work for assignment move to instead make a &mut retag that's protected until the place is StorageDead? Or would it be too ad-hoc to have protectors expire not inside the function epilogue? If that works, it should work for argument move as well.

I'm also unclear on how this scheme is supposed to justify the argument place address aliasing the source place, so maybe I'm missing something.

[RalfJung]

Would it work for assignment move to instead make a &mut retag that's protected until the place is StorageDead?

Given that the LHS is an arbitrary place, and StorageDead works on locals, that's not even a well-defined statement.

I'm also unclear on how this scheme is supposed to justify the argument place address aliasing the source place

That's explicitly discussed as an open problem in #416 or one of the adjacent issues.