Skip to content

Commit

Permalink
Add some SAFETY preconditions and invariants
Browse files Browse the repository at this point in the history
  • Loading branch information
dureuill committed Mar 16, 2024
1 parent 0b7d869 commit bab87c5
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 3 deletions.
10 changes: 9 additions & 1 deletion src/box_scope.rs
Original file line number Diff line number Diff line change
Expand Up @@ -97,13 +97,17 @@ where

let raw_scope: *mut RawScope<T, F> = raw_scope.cast();

// SAFETY:
// 1. `raw_scope` allocated by the `Box` so is valid memory.
// 2. TODO
unsafe {
RawScope::open(raw_scope, scope);
}

mem::forget(panic_guard); // defuse guard
// (guard field has no drop glue, so this does not leak anything, it just skips the above `Drop` impl)

// SAFETY: `raw_scope` allocated by the `Box` so is non-null.
BoxScope(unsafe { NonNull::new_unchecked(raw_scope) })
}
}
Expand All @@ -124,7 +128,11 @@ where
where
G: for<'a> FnOnce(&'a mut <T as Family<'a>>::Family) -> Output,
{
// SAFETY: `self.0` is dereference-able due to coming from a `Box`.
// SAFETY:
// 1. `self.0` is dereference-able due to coming from a `Box`.
// 2. The object pointed to by `self.0` did not move and won't before deallocation.
// 3. `BoxScope::enter` takes an exclusive reference.
// 4. TODO
unsafe { RawScope::enter(self.0, f) }
}
}
23 changes: 21 additions & 2 deletions src/raw_scope.rs
Original file line number Diff line number Diff line change
Expand Up @@ -141,17 +141,22 @@ where
{
/// # Safety
///
/// TODO docs
/// 1. `this` is dereferenceable
/// 2. TODO: any precondition on `this` for RawScope::fields is satisfied.
pub(crate) unsafe fn open<S: TopScope<Family = T, Future = F>>(this: *mut Self, scope: S)
where
T: for<'a> Family<'a>,
F: Future<Output = Never>,
S: TopScope<Family = T>,
{
// SAFETY: precondition (2)
let RawScopeFields { state, active_fut } = unsafe { Self::fields(this) };

let time_capsule = TimeCapsule { state };

// SAFETY:
// - precondition (1)
// - using `scope.run` from the executor.
unsafe {
active_fut.write(scope.run(time_capsule));
}
Expand All @@ -165,21 +170,32 @@ where
{
/// # Safety
///
/// TODO docs
/// 1. `this` is dereferenceable
/// 2. `this` verifies the guarantees of `Pin` (one of its fields is pinned in this function)
/// 3. No other exclusive reference to the frozen value. In particular, no concurrent calls to this function.
/// 4. TODO: any precondition on `this` for RawScope::fields is satisfied.
#[allow(unused_unsafe)]
pub(crate) unsafe fn enter<'borrow, Output: 'borrow, G>(this: NonNull<Self>, f: G) -> Output
where
G: for<'a> FnOnce(&'a mut <T as Family<'a>>::Family) -> Output,
{
// SAFETY: precondition (4)
let RawScopeFields { state, active_fut } = unsafe { Self::fields(this.as_ptr()) };

// SAFETY: precondition (2)
let active_fut: Pin<&mut F> = unsafe { Pin::new_unchecked(&mut *active_fut) };

match active_fut.poll(&mut std::task::Context::from_waker(&waker::create())) {
Poll::Ready(never) => match never {},
Poll::Pending => {}
}

// SAFETY:
// - dereferenceable: precondition (1)
// - drop: reading a reference (no drop glue)
// - aliasing: precondition (3) + `mut_ref` cannot escape this function via `f`
// - lifetime: the value is still live due to the precondition on `Scope::run`,
// preventing <https://github.com/dureuill/nolife/issues/8>
let mut_ref = unsafe {
state
.read()
Expand All @@ -201,6 +217,9 @@ where
mut self: std::pin::Pin<&mut Self>,
_cx: &mut std::task::Context<'_>,
) -> Poll<Self::Output> {
// SAFETY:
// - state was set to a valid value in [`TimeCapsule::freeze`]
// - the value is still 'live', due to the lifetime in `FrozenFuture`
let state: &mut State<T> = unsafe { &mut *self.state };
if state.is_none() {
let mut_ref = self
Expand Down

0 comments on commit bab87c5

Please sign in to comment.