Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion src/foreign/alloc/ffi/c_str.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,12 @@ impl<'a> Arbitrary<'a> for CString {
fn arbitrary(u: &mut Unstructured<'a>) -> Result<Self> {
<Vec<u8> as Arbitrary>::arbitrary(u).map(|mut x| {
x.retain(|&c| c != 0);
// SAFETY: all zero bytes have been removed
// SAFETY:
// Contract from `CString::from_vec_unchecked`: the vector must not contain

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's a neat way to write down safety comments in a more structured way. I will, um, yoink this.

If only there was a way to reference the contracts without repeating them a bunch from what's already in the doc for the method... 🤔

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah that's been my rule about good safety comments for a while: list the things you need to prove, then prove them.

Review becomes double checking you got all the invariants (easy if occasionally tedious) and then checking the local proof (usually easy, sometimes not)

// any interior nul (zero) bytes.

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't the canonical name for the zero byte a null byte (not nul or nil for that matter) as per K&R =)

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nul is what it is called in the context of strings

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

thanks. I had done a similar PR and debated to use null or nul when talking about an array of ascii bytes. Sounds like I should have used nul in the comment.

// Evidence: `x.retain(|&c| c != 0)` removes all bytes equal to `0` from the
// vector `x`. Consequently, `x` contains no nul bytes, which guarantees
// it has no interior nul bytes.
unsafe { Self::from_vec_unchecked(x) }
})
}
Expand Down
30 changes: 26 additions & 4 deletions src/foreign/core/array.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,17 @@ impl<T, const N: usize> Drop for ArrayGuard<T, N> {
fn drop(&mut self) {
debug_assert!(self.initialized <= N);
let initialized_part = ptr::slice_from_raw_parts_mut(self.dst, self.initialized);
// SAFETY:
// Contract from `ptr::drop_in_place`: the pointer must be valid for reads and
// writes, and must be properly aligned.
// Evidence:
// - `self.dst` is derived from `MaybeUninit<[T; N]>` on the stack, which remains
// alive and allocated because the guard is a local variable dropped before
// the stack frame is destroyed.
// - The alignment of `self.dst` matches that of `[T; N]`, which is aligned for `T`.
// - Only the first `self.initialized` elements are dropped, which have been
// fully initialized by `ptr::write` in `try_create_array`.
// Therefore the contract of `drop_in_place` is discharged.
unsafe {
ptr::drop_in_place(initialized_part);
}
Expand All @@ -30,17 +41,28 @@ where
{
let mut array: MaybeUninit<[T; N]> = MaybeUninit::uninit();
let array_ptr = array.as_mut_ptr();
let dst = array_ptr as _;
let dst = array_ptr as *mut T;
let mut guard: ArrayGuard<T, N> = ArrayGuard {
dst,
initialized: 0,
};
unsafe {
for (idx, value_ptr) in (*array.as_mut_ptr()).iter_mut().enumerate() {
for idx in 0..N {
// SAFETY: `dst` is a valid pointer to the start of the `[T; N]` array.
// `idx` is within `0..N`, so `dst.add(idx)` is within the bounds of the allocation.
// The pointer is properly aligned for `T`.
unsafe {
let value_ptr = dst.add(idx);
ptr::write(value_ptr, cb(idx)?);
guard.initialized += 1;
}
guard.initialized += 1;
}
unsafe {
mem::forget(guard);
// SAFETY:
// Contract from `MaybeUninit::assume_init`: the value must be fully initialized.
// Evidence: the loop executes exactly `N` times, successfully writing a value
// to each of the `N` indices in the array. Since the loop completed without
// returning early or panicking, all elements of the array are initialized.
Ok(array.assume_init())
}
}
Expand Down
10 changes: 10 additions & 0 deletions src/foreign/core/str.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,16 @@ fn arbitrary_str<'a>(u: &mut Unstructured<'a>, size: usize) -> Result<&'a str> {
Err(e) => {
let i = e.valid_up_to();
let valid = u.bytes(i).unwrap();
// SAFETY:
// Contract from `str::from_utf8_unchecked`: the bytes must be valid UTF-8.
// Evidence:
// - `str::from_utf8` was called on the next `size` peeked bytes from `u`.
// - The call failed, returning a `Utf8Error` `e`.
// - `e.valid_up_to()` returns the length of the prefix of the peeked bytes
// which is guaranteed to be valid UTF-8.
// - `u.bytes(i)` consumes and returns exactly this valid prefix (since `u`
// was not mutated or consumed between peeking and calling `bytes`).
// - Therefore, `valid` is guaranteed to contain valid UTF-8.
let s = unsafe {
debug_assert!(str::from_utf8(valid).is_ok());
str::from_utf8_unchecked(valid)
Expand Down
Loading