-
Notifications
You must be signed in to change notification settings - Fork 59
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
What are the preconditions for (overlapping) ptr::copy
?
#549
Comments
It's perhaps somewhat relevant to note that TB's "3 phase" mutable borrows would make the question moot, as reading would still be permitted. IIRC, miri implements |
Miri currently indeed first triggers a full read of the src range, then a full write of the dst range. We could probably trigger another read of the src range afterwards and hopefully that is enough to cover all permutations?
The writes to |
Read-write-read is actually not enough, since @JoJoDeveloping is there some theorem for how often we have to alternative to be sure TB has reached a steady state? |
a safe upper bound is as many as there are states in the TB machine. But here probably it's write, followed by foreign actions, followed by write. This is because a On a more general question, why is this necessary? The specification here seems overly restrictive, there is no sensible implementation that reads a memory cell via |
If you copy naively in a loop, and the ranges overlap partially, you might first write via dst and then read via src, no? For instance consider src to be at offset 0, dst at offset 5, and the size is 10. The cell at offset 5 is first written to via dst (when we copy element 0), and then later read via src (when we copy element 5). |
yeah if they overlap you have to copy the spans in reverse, depending on the relative positions of src and dst. that's memmove basics. |
No, because then you would read the new value, which is precisely what |
Ah right I guess we are specifying that we don't see the odd copying artifacts, fair.
I mixed this up with |
Even for |
rust-lang/rust#134606 fixes the |
From the docs:
I read this first requirement of saying that after writes to
dst
, reading fromsrc
must still be possible, even in the positions that have been written to… it says “whendst
is written forcount * size_of::<T>()
bytes”, which should mean “when the whole range ofdst
has [possibly] been written to”, right?Of course, the docs also say:
Which when taken literally could be interpreted to say - in particular - that each place is only ever written to via
dst
after it has been read viasrc
. But I - as a reader - would actually understand this particular sentence to be only about the question of "which bytes are in what places at the end of this" (because I guess otherwise it's also reasonable to assume that acopy
operation might only 'technically' allow overlap to reduce UB, but still mix up the order of the data/elements in that case).As far as what I can (currently) observe in miri, the documented precondition is not checked.
(playground)
So, either the precondition is wrong, or miri is wrong, or I'm misinterpreting something, or the behavior isn't fully defined yet and std docs make conservative restrictions for future compat, whilst miri conservatively allows stuff that isn't "actual" UB today.
Perhaps someone here knows more context?
AFAICT, given that the
copy
itself actually accesses all the memory/bytes in question anyways, this can't be a case wheremiri
is simply unable to enforce the documented precondition efficiently. [Unlike many cases of documented library-UB for instance.]The text was updated successfully, but these errors were encountered: