Skip to content

Soundness: CastPtr::borrow_mut #542

Description

@rikosellic

The borrow_mut method produces a mutable reference; however, we have no control over inner_perm to keep it related to the mutable reference, so when it goes out of scope, there is no way to establish final(perm).wf(&final(perm).inner_perms).

#[verifier::external_body]
pub exec fn borrow_mut<'a>(self, Tracked(perm): Tracked<&'a mut PointsTo<R, T>>) -> (v:
&'a mut T)
requires
old(perm).pptr() == self,
old(perm).is_init(),
old(perm).wf(&old(perm).inner_perms),
ensures
*v == old(perm).value(),
final(perm).pptr() == old(perm).pptr(),
final(perm).is_init(),
final(perm).wf(&final(perm).inner_perms),
final(perm).value() == *final(v),
{
// SAFETY: `Repr<R> for T` asserts layout compatibility between R and
// T. The tracked `perm` guards against concurrent access.
unsafe { &mut *(self.ptr.addr() as *mut T) }
}
}

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    model designModel or specification of system designverification bugUnsoundness, verification panics, or unsupported features

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions