Skip to content

Commit

Permalink
Add safety considerations for RawScopeFields
Browse files Browse the repository at this point in the history
  • Loading branch information
dureuill committed Mar 16, 2024
1 parent bab87c5 commit 9aa2c0a
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 12 deletions.
11 changes: 6 additions & 5 deletions src/box_scope.rs
Original file line number Diff line number Diff line change
Expand Up @@ -98,8 +98,10 @@ 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
// 1. `raw_scope` allocated by the `Box` so is valid memory, although the future is not yet initialized
// 2. `raw_scope` was created from a valid `RawScope::<T, MaybeUninit<F>>`, so `state` is fully initialized.
//
// Note: as a post-condition of `RawScope`, `raw_scope` is fully initialized.
unsafe {
RawScope::open(raw_scope, scope);
}
Expand Down Expand Up @@ -129,10 +131,9 @@ where
G: for<'a> FnOnce(&'a mut <T as Family<'a>>::Family) -> Output,
{
// SAFETY:
// 1. `self.0` is dereference-able due to coming from a `Box`.
// 1. `self.0` is valid as a post-condition of `new_typed`.
// 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
// 3. `BoxScope::enter` takes an exclusive reference and the reference passed to `f` cannot escape `f`.
unsafe { RawScope::enter(self.0, f) }
}
}
23 changes: 16 additions & 7 deletions src/raw_scope.rs
Original file line number Diff line number Diff line change
Expand Up @@ -126,9 +126,15 @@ impl<T, F: ?Sized> RawScope<T, F>
where
T: for<'a> Family<'a>,
{
/// SAFETY:
///
/// 1. `this` points to an allocation that can hold a `RawScope<T, F>`,
/// not necessarily initialized or properly aligned.
unsafe fn fields(this: *mut Self) -> RawScopeFields<T, F> {
RawScopeFields {
// SAFETY: precondition (1)
state: unsafe { addr_of_mut!((*this).state) },
// SAFETY: precondition (1)
active_fut: unsafe { addr_of_mut!((*this).active_fut) },
}
}
Expand All @@ -141,22 +147,26 @@ where
{
/// # Safety
///
/// 1. `this` is dereferenceable
/// 2. TODO: any precondition on `this` for RawScope::fields is satisfied.
/// 1. `this` points to a properly aligned allocation that can hold a `RawScope<T, F>`, where `active_fut` is not necessarily initialized.
/// 2. `this.state` is initialized.
///
/// # Post-condition
///
/// 1. `this.active_fut` is fully initialized
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)
// SAFETY: precondition (1)
let RawScopeFields { state, active_fut } = unsafe { Self::fields(this) };

let time_capsule = TimeCapsule { state };

// SAFETY:
// - precondition (1)
// - using `scope.run` from the executor.
// - using `scope.run` from the executor
unsafe {
active_fut.write(scope.run(time_capsule));
}
Expand All @@ -170,16 +180,15 @@ where
{
/// # Safety
///
/// 1. `this` is dereferenceable
/// 1. `this` points to a properly aligned, fully initialized `RawScope<T, F>`.
/// 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)
// SAFETY: precondition (1)
let RawScopeFields { state, active_fut } = unsafe { Self::fields(this.as_ptr()) };

// SAFETY: precondition (2)
Expand Down

0 comments on commit 9aa2c0a

Please # to comment.