offset_from, offset: clearly separate safety requirements the user needs to prove from corollaries that automatically follow #127275
Conversation
|
Cc @rust-lang/opsem |
|
Some changes occurred to the CTFE / Miri engine cc @rust-lang/miri |
ebabe18 to
1ec2432
Compare
library/core/src/ptr/mut_ptr.rs
Outdated
| /// Allocated objects can never be larger than `isize::MAX` and they never "wrap around" the | ||
| /// edge of the address space, so as a consequence of this, `count * size_of::<T>()` must | ||
| /// fit in an `isize` and adding the computed offset to `self` produces a resulting address | ||
| /// that fits into a `usize`. |
There was a problem hiding this comment.
I have now also done the same kind of editing to offset: clearly state what the user needs to prove, and what follows automatically due to the invariants we have about the address space.
These docs are copied a couple of times, so I will wait for PR feedback before updating all the copies.
library/core/src/ptr/mut_ptr.rs
Outdated
| /// | ||
| /// * The computed offset, **in bytes**, cannot overflow an `isize`. | ||
| /// * If the computed offset is non-zero, then the entire memory range between `self` and the | ||
| /// result must be in bounds of the [allocated object] `self` is derived from. |
There was a problem hiding this comment.
This sentence sounds like it refers to the allocated object of the pointer itself (self), rather than what it is pointing to.
There was a problem hiding this comment.
In offset_from we talk about self being derived from a pointer to a particular allocated object... but adding that here makes the sentence too nested, I think. I should probably give a name to the allocated object.
library/core/src/ptr/mut_ptr.rs
Outdated
| /// If any of the following conditions are violated, the result is Undefined | ||
| /// Behavior: | ||
| /// The resulting pointer's address is computed as the address of the original pointer plus the | ||
| /// computed offset, `count * size_of::<T>()`, with infinite precision. |
There was a problem hiding this comment.
| /// computed offset, `count * size_of::<T>()`, with infinite precision. | |
| /// computed offset, `count * size_of::<T>()` bytes. |
I think talking about infinite precision here is more confusing than it helps. It's clearly to just say the calculation is not allowed to overflow.
There was a problem hiding this comment.
Then we'd have to spell out how exactly it is not allowed to overflow -- i.e., what the bounds are. The nice thing about doing the arithmetic in infinite precision is that we can avoid that, since it falls out of the in-bounds requirement. But this spec is too clever for its own good...
d5505a7 to
f4f6724
Compare
|
@Amanieu I have pushed a new revision, attempting to resolve your comments. |
|
LGTM r=me |
f4f6724 to
80d0f14
Compare
|
I have updated the other copies of the |
also, isize::MIN is an impossible distance
80d0f14 to
9ba492f
Compare
|
I found more copies of these docs on |
|
@bors r+ rollup |
By landing #116675 we decided that objects larger than
isize::MAXcannot exist in the address space of a Rust program, which lets us simplify these rules.For
offset_from, we can even state that the absolute distance fits into anisize, and therefore excludeisize::MIN. This PR also changes Miri to treat anisize::MINdifference like the other isize-overflowing cases.