MIRI disagree with the documentation of `ptr::drop_in_place`

[SkiFire13]

Location

https://doc.rust-lang.org/stable/std/ptr/fn.drop_in_place.html

Summary

The documentation for ptr::drop_in_place claims that:

This is semantically equivalent to calling ptr::read and discarding the result.

However when tested in a playground MIRI complained about the use of ptr::read but not of ptr::drop_in_place: https://play.rust-lang.org/?version=nightly&mode=debug&edition=2021&gist=c3dfe878ef015b93f051785b67239752

Although the ptr::drop_in_place documentation lists a bunch of cases where they differ, none of them seems to apply to this one.

Some details of the reproduction:

• it uses #[may_dangle] both because the issue derived from this user.rust-lang.com thread on #[may_dangle] and because I didn't find a quicker way to create a dangling reference. However this doesn't seem fundamental to the issue and likely is not required.
• this seems to only work with exclusive references, MIRI won't complain with shared ones

[slightlyoutofphase]

Neither function has a "real" Rust implementation, but it does seem like their internal instantiation occurs in different places within the compiler. Probably this is related to that in some way.

[RalfJung]

Yeah the documentation is imprecise and conservative. It mostly wants to make sure people don't cause UB.^^ So we document the safety constraint as equivalent to ptr::read just to be safe; it is actually weaker. However we don't yet want to commit to how much weaker it is, so we're saying they are actually the same.

This is a somewhat dubious use of "semantically equivalent" -- basically the equivalence is a library-level spec and what you are doing causes library UB, but currently does not cause language UB. The library might change in a way that it can become language UB in the future.

[RalfJung]

Also the claim "This is semantically equivalent to calling ptr::read and discarding the result" is definitely wrong for pinned types, where it is important that we do the drop in-place.

It might be better to just remove this sentence.

EDI: Actually that part is spelled out in the docs.