Provide proofs of safety.

This commit is contained in:
Sergey Pepyakin 2019-07-03 13:06:28 +02:00
parent 9614eb9508
commit 5b86cb5bca
1 changed files with 73 additions and 18 deletions

View File

@ -1,48 +1,105 @@
//! An implementation of a `ByteBuf` based on virtual memory. //! An implementation of a `ByteBuf` based on virtual memory.
//! //!
//! This implementation uses `mmap` on POSIX systems (and should use `VirtualAlloc` on windows). //! This implementation uses `mmap` on POSIX systems (and should use `VirtualAlloc` on windows).
//! There are possibilities to improve the performance for the reallocating case by reserving
//! memory up to maximum. This might be a problem for systems that don't have a lot of virtual
//! memory.
use std::ptr::{self, NonNull}; use std::ptr::{self, NonNull};
use std::slice; use std::slice;
struct Mmap { struct Mmap {
/// The pointer that points to the start of the mapping.
///
/// This value doesn't change after creation.
ptr: NonNull<u8>, ptr: NonNull<u8>,
/// The length of this mapping.
///
/// Cannot be more than `isize::max_value()`. This value doesn't change after creation.
len: usize, len: usize,
} }
impl Mmap { impl Mmap {
fn new(len: usize) -> Self { fn new(len: usize) -> Self {
assert!(len < isize::max_value() as usize);
assert!(len > 0); assert!(len > 0);
unsafe { let ptr_or_err = unsafe {
let ptr = libc::mmap( // Safety Proof:
// There are not specific safety proofs are required for this call, since the call
// by itself can't invoke any safety problems (however, misusing its result can).
libc::mmap(
// `addr` - let the system to choose the address at which to create the mapping.
ptr::null_mut(), ptr::null_mut(),
// the length of the mapping in bytes.
len, len,
// `prot` - protection flags: READ WRITE !EXECUTE
libc::PROT_READ | libc::PROT_WRITE, libc::PROT_READ | libc::PROT_WRITE,
libc::MAP_PRIVATE | libc::MAP_ANON, // `flags`
// `MAP_ANON` - mapping is not backed by any file and initial contents are
// initialized to zero.
// `MAP_PRIVATE` - the mapping is private to this process.
libc::MAP_ANON | libc::MAP_PRIVATE,
// `fildes` - a file descriptor. Pass -1 as this is required for some platforms
// when the `MAP_ANON` is passed.
-1, -1,
// `offset` - offset from the file.
0, 0,
);; )
assert!(ptr as isize != -1); };
Self {
ptr: NonNull::new(ptr as *mut u8).unwrap(), match ptr_or_err as usize {
len, // `mmap` shouldn't return 0 since it has a special meaning.
x if x == 0 || x as isize == -1 => panic!(),
_ => {
let ptr = unsafe {
// Safety Proof:
// the ptr cannot be null as checked within the enclosing match.
NonNull::new_unchecked(ptr_or_err as *mut u8)
};
Self { ptr, len }
} }
} }
} }
pub fn as_slice(&self) -> &[u8] { fn as_slice(&self) -> &[u8] {
unsafe { slice::from_raw_parts(self.ptr.as_ptr(), self.len) } unsafe {
// Safety Proof:
// - Aliasing guarantees of `self.ptr` are not violated since `self` is the only owner.
// - This pointer was allocated for `self.len` bytes and thus is a valid slice.
// - `self.len` doesn't change throughout the lifetime of `self`.
// - The value is returned valid for the duration of lifetime of `self`.
// `self` cannot be destroyed while the returned slice is alive.
// - `self.ptr` is of `NonNull` type and thus `.as_ptr()` can never return NULL.
// - `self.len` cannot be larger than `isize::max_value()`.
slice::from_raw_parts(self.ptr.as_ptr(), self.len)
}
} }
pub fn as_slice_mut(&mut self) -> &mut [u8] { fn as_slice_mut(&mut self) -> &mut [u8] {
unsafe { slice::from_raw_parts_mut(self.ptr.as_ptr(), self.len) } unsafe {
// Safety Proof:
// - See the proof for `Self::as_slice`
// - Additionally, it is not possible to obtain two mutable references for `self.ptr`
slice::from_raw_parts_mut(self.ptr.as_ptr(), self.len)
}
} }
} }
impl Drop for Mmap { impl Drop for Mmap {
fn drop(&mut self) { fn drop(&mut self) {
let r = unsafe { libc::munmap(self.ptr.as_ptr() as *mut libc::c_void, self.len) }; let ret_val = unsafe {
assert_eq!(r, 0, "munmap failed"); // Safety proof:
// - `self.ptr` was allocated by a call to `mmap`.
// - `self.len` was saved at the same time and it doesn't change throughout the lifetime
// of `self`.
libc::munmap(self.ptr.as_ptr() as *mut libc::c_void, self.len)
};
// There is no reason for `munmap` to fail to deallocate a private annonymous mapping
// allocated by `mmap`.
// However, for the cases when it actually fails prefer to fail, in order to not leak
// and exhaust the virtual memory.
assert_eq!(ret_val, 0, "munmap failed");
} }
} }
@ -53,7 +110,6 @@ pub struct ByteBuf {
impl ByteBuf { impl ByteBuf {
pub fn new(len: usize) -> Self { pub fn new(len: usize) -> Self {
let mmap = if len == 0 { None } else { Some(Mmap::new(len)) }; let mmap = if len == 0 { None } else { Some(Mmap::new(len)) };
Self { mmap } Self { mmap }
} }
@ -66,11 +122,10 @@ impl ByteBuf {
} else { } else {
let mut new_mmap = Mmap::new(new_len); let mut new_mmap = Mmap::new(new_len);
unsafe { {
let src = self.mmap.as_ref().unwrap().as_slice(); let src = self.mmap.as_ref().unwrap().as_slice();
let dst = new_mmap.as_slice_mut(); let dst = new_mmap.as_slice_mut();
dst[..src.len()].copy_from_slice(src);
ptr::copy_nonoverlapping(src.as_ptr(), dst.as_mut_ptr(), src.len());
} }
Some(new_mmap) Some(new_mmap)