What about: use-after-move and (maybe) use-after-drop

[RalfJung]

Miri currently considers Copy and Move the same operation. There are some proposals in particular by @eddyb to make them not the same: it might be beneficial for optimizations to be able to rely on the data not being read again after a Move. This would correspond to replacing the data by Undef. It seems reasonable to do similar things for drop -- though that requires a precise definition of what is actually considered a drop (does that include just the Drop terminator or also calls to drop_in_place?).

(Miri concern: One reason why I am a bit hesitant about this is that this makes read have a side-effect, so we'd have to make all read methods in Miri take the interpreter context by &mut self. Reads already have a side-effect in Stacked Borrows but that is fairly local and we just use a RefCell there.)

@eddyb what would be such optimizations that benefit from this, where StorageDead is not happening so we need to rely on Move?

Potential blockers that would prevent deinit-on-move:

• Safe function MIR reads discriminant of moved-out local rust#91029

Reasons to do deinit-on-move:

• Semantics of MIR function calls rust#71117 (comment) (but might be solved by aliasing restrictions?)

Testcases:

• MIR: Do we allow accesing a moved place? rust#112564

[eddyb]

I was actually betting on having a Move invalidate borrows, I'm not sure it actually helps optimizations to consider the value as undef.

But that doesn't appear to be happening, so this would at most be a correctness check.

As for reads becoming &mut - isn't Operand relatively high-level? Or is the problem that the actual read is performed way after evaluating the Operand into its miri form?

[RalfJung]

I was actually betting on having a Move invalidate borrows, I'm not sure it actually helps optimizations to consider the value as undef.

Oh, interesting. I suppose we could treat a Move as a write to the source. A write to a local invalidates all pointers to that local.

As for reads becoming &mut - isn't Operand relatively high-level? Or is the problem that the actual read is performed way after evaluating the Operand into its miri form?

Not sure what you mean. The actual read is performed by methods in operand.rs that take an interpret::Operand and &self.

We'd have to preserve on an interpret::Operand whether this was a "copy" or "move" operand, and then still change all those methods to &mut self to do the writing. I was so happy when we were able to make them all &self.^^

[RalfJung]

If we make it just act like a write for Stacked Borrows, but not actually change memory, that would work with &self though. Seems like a rather hacky solution though, I'd rather not pollute the spec with such concerns.

StorageDead has the effect you want. But I guess there are examples where that is not appropriate?

[oli-obk]

We could run a second visitor after the evaluation of a statement whose sole purpose is to find Operand::Moves and clear the moved from memory.

We can't use StorageDead for partial moves

[RalfJung]

It would be hard to guarantee that evaluating the statement did not end up changing what those Operand::Move evaluate to. MIR is not pure enough for this.

For partial moves, how would that ever have the effect of invalidating pointers? The neighboring fields have to stay in place after all!

[RalfJung]

To mirror what I said on Zulip: I would like to see an example of an optimization that this enables. Since opening this issue, I've come around to realize that the examples where I thought it would help, are actually not valid.

[RalfJung]

I moved this to the UCG repo because really this is a question of what the semantics should be, not how to implement it in Miri.

[RalfJung]

Jim Blandy asked via email if similar things to what has been proposed for Move, apply to ptr::read: should that leave the memory from which things came as Undef? I think for Copy types the answer is definitely "no", but other types, if we decide to make Move "kill" the memory it came from, we might or might not want to do the same for ptr::read.