From c786cf1d5b4cfe640884e3ebd47f9f7b9cf02a81 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Wed, 31 Dec 2025 11:14:19 +0800 Subject: [PATCH] Use manuallydrop std_spec --- Cargo.lock | 4 +- aster_common/src/mm/frame/frame_ref.rs | 4 +- .../src/mm/page_table/node/entry_owners.rs | 6 +-- ostd/src/mm/frame/frame_ref.rs | 1 - ostd/src/mm/page_table/cursor/mod.rs | 4 +- ostd/src/mm/page_table/node/entry.rs | 8 ++-- ostd/src/mm/page_table/node/mod.rs | 16 ++++---- ostd/src/sync/rcu/non_null/mod.rs | 2 +- vstd_extra/src/external/deref.rs | 6 --- vstd_extra/src/external/manually_drop.rs | 37 ------------------- vstd_extra/src/external/mod.rs | 2 - 11 files changed, 21 insertions(+), 69 deletions(-) delete mode 100644 vstd_extra/src/external/manually_drop.rs diff --git a/Cargo.lock b/Cargo.lock index 5bb3ef418..c6d237811 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -576,7 +576,7 @@ dependencies = [ [[package]] name = "verus_builtin" -version = "0.0.0-2025-12-14-0054" +version = "0.0.0-2025-12-28-0056" [[package]] name = "verus_builtin_macros" @@ -631,7 +631,7 @@ checksum = "af8ca9a5d4debca0633e697c88269395493cebf2e10db21ca2dbde37c1356452" [[package]] name = "vstd" -version = "0.0.0-2025-12-14-0054" +version = "0.0.0-2025-12-28-0056" dependencies = [ "verus_builtin", "verus_builtin_macros", diff --git a/aster_common/src/mm/frame/frame_ref.rs b/aster_common/src/mm/frame/frame_ref.rs index 49e6a4d18..c215fab14 100644 --- a/aster_common/src/mm/frame/frame_ref.rs +++ b/aster_common/src/mm/frame/frame_ref.rs @@ -4,8 +4,6 @@ use std::ops::Deref; use core::mem::ManuallyDrop; -use vstd_extra::external::manually_drop::*; - use super::*; verus! { @@ -20,7 +18,7 @@ pub struct FrameRef<'a, M: AnyFrameMeta> { impl Deref for FrameRef<'_, M> { type Target = Frame; - #[verus_spec(ensures returns manually_drop_deref_spec(&self.inner))] + #[verus_spec(returns &self.inner@)] fn deref(&self) -> &Self::Target { &self.inner } diff --git a/aster_common/src/mm/page_table/node/entry_owners.rs b/aster_common/src/mm/page_table/node/entry_owners.rs index b7c86296b..1350b885a 100644 --- a/aster_common/src/mm/page_table/node/entry_owners.rs +++ b/aster_common/src/mm/page_table/node/entry_owners.rs @@ -17,8 +17,8 @@ pub tracked struct NodeEntryOwner<'rcu, C: PageTableConfig> { impl<'rcu, C: PageTableConfig> Inv for NodeEntryOwner<'rcu, C> { open spec fn inv(self) -> bool { &&& self.guard_perm.is_init() - &&& self.guard_perm.value().inner.inner.ptr.addr() == self.as_node.meta_perm.addr() - &&& self.guard_perm.value().inner.inner.wf(self.as_node) + &&& self.guard_perm.value().inner.inner@.ptr.addr() == self.as_node.meta_perm.addr() + &&& self.guard_perm.value().inner.inner@.wf(self.as_node) &&& self.as_node.inv() &&& meta_to_frame(self.as_node.meta_perm.addr()) < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR() @@ -76,7 +76,7 @@ impl<'rcu, C: PageTableConfig> EntryOwner<'rcu, C> { pub open spec fn relate_parent_guard_perm(self, guard_perm: PointsTo>) -> bool { &&& guard_perm.addr() == self.guard_addr &&& guard_perm.is_init() - &&& guard_perm.value().inner.inner.ptr.addr() == self.base_addr + &&& guard_perm.value().inner.inner@.ptr.addr() == self.base_addr } } diff --git a/ostd/src/mm/frame/frame_ref.rs b/ostd/src/mm/frame/frame_ref.rs index 1c35e0a2e..891723735 100644 --- a/ostd/src/mm/frame/frame_ref.rs +++ b/ostd/src/mm/frame/frame_ref.rs @@ -3,7 +3,6 @@ use core::{marker::PhantomData, mem::ManuallyDrop, ops::Deref, ptr::NonNull}; use vstd::prelude::*; -use vstd_extra::external::manually_drop::*; use vstd_extra::ownership::*; use aster_common::prelude::frame::*; diff --git a/ostd/src/mm/page_table/cursor/mod.rs b/ostd/src/mm/page_table/cursor/mod.rs index c33203880..26cdfb87b 100644 --- a/ostd/src/mm/page_table/cursor/mod.rs +++ b/ostd/src/mm/page_table/cursor/mod.rs @@ -366,9 +366,9 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> { #[verus_spec(with Tracked(&mut child_node_owner.guard_perm))] let pt_guard = pt.make_guard_unchecked(rcu_guard); - assert(parent_node_owner.guard_perm.value().inner.inner.wf(parent_node_owner.as_node)); + assert(parent_node_owner.guard_perm.value().inner.inner@.wf(parent_node_owner.as_node)); // assert(parent_node_owner.guard_perm.value().inner.inner.ptr.addr() == parent_node_owner.as_node.meta_perm.addr()) by { admit() }; - assert(child_node_owner.guard_perm.value().inner.inner.ptr.addr() == child_node_owner.as_node.meta_perm.points_to.addr()) by { admit() }; + assert(child_node_owner.guard_perm.value().inner.inner@.ptr.addr() == child_node_owner.as_node.meta_perm.points_to.addr()) by { admit() }; assert(parent_node_owner.as_node.inv()) by { admit() }; #[verus_spec(with Tracked(&mut child_node_owner.as_node))] diff --git a/ostd/src/mm/page_table/node/entry.rs b/ostd/src/mm/page_table/node/entry.rs index e0ee8af60..b1cbf3b2e 100644 --- a/ostd/src/mm/page_table/node/entry.rs +++ b/ostd/src/mm/page_table/node/entry.rs @@ -48,8 +48,8 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'rcu, C> { self.node == guard_perm.pptr(), guard_perm.is_init(), owner.is_node(), // The owner is the owner of the parent node, so should always be a node - inner_perm.addr() == guard_perm.value().inner.inner.ptr.addr(), - inner_perm.points_to.addr() == guard_perm.value().inner.inner.ptr.addr(), + inner_perm.addr() == guard_perm.value().inner.inner@.ptr.addr(), + inner_perm.points_to.addr() == guard_perm.value().inner.inner@.ptr.addr(), inner_perm.is_init(), inner_perm.wf(), { @@ -172,8 +172,8 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'rcu, C> { new_child is PageTable, FRAME_METADATA_RANGE().start <= frame_to_index(new_child.get_node().unwrap().ptr.addr()) < FRAME_METADATA_RANGE().end, - inner_perm.addr() == old(guard_perm).value().inner.inner.ptr.addr(), - inner_perm.points_to.addr() == old(guard_perm).value().inner.inner.ptr.addr(), + inner_perm.addr() == old(guard_perm).value().inner.inner@.ptr.addr(), + inner_perm.points_to.addr() == old(guard_perm).value().inner.inner@.ptr.addr(), inner_perm.is_init(), inner_perm.wf(), { diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs index 82df440b2..a6e1defc0 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/ostd/src/mm/page_table/node/mod.rs @@ -221,8 +221,8 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> { )] pub fn nr_children(&self) -> (nr: u16) requires - self.inner.inner.ptr.addr() == old(owner).meta_perm.addr(), - self.inner.inner.ptr.addr() == old(owner).meta_perm.points_to.addr(), + self.inner.inner@.ptr.addr() == old(owner).meta_perm.addr(), + self.inner.inner@.ptr.addr() == old(owner).meta_perm.points_to.addr(), old(owner).inv(), ensures owner == old(owner) @@ -242,8 +242,8 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> { pub fn stray_mut(&mut self) -> PCell requires owner.is_node(), - old(self).inner.inner.ptr.addr() == owner.node.unwrap().as_node.meta_perm.addr(), - old(self).inner.inner.ptr.addr() == owner.node.unwrap().as_node.meta_perm.points_to.addr(), + old(self).inner.inner@.ptr.addr() == owner.node.unwrap().as_node.meta_perm.addr(), + old(self).inner.inner@.ptr.addr() == owner.node.unwrap().as_node.meta_perm.points_to.addr(), owner.inv(), { let tracked node_owner = owner.node.tracked_borrow(); @@ -270,8 +270,8 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> { )] pub fn read_pte(&self, idx: usize) -> C::E requires - self.inner.inner.ptr.addr() == owner.meta_perm.addr, - self.inner.inner.ptr.addr() == owner.meta_perm.points_to.addr(), + self.inner.inner@.ptr.addr() == owner.meta_perm.addr(), + self.inner.inner@.ptr.addr() == owner.meta_perm.points_to.addr(), owner.inv(), meta_to_frame(owner.meta_perm.addr) < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(), FRAME_METADATA_RANGE().start <= owner.meta_perm.addr < FRAME_METADATA_RANGE().end, @@ -337,8 +337,8 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> { )] fn nr_children_mut<'a>(&'a mut self) -> &'a PCell requires - old(self).inner.inner.ptr.addr() == meta_perm.addr(), - old(self).inner.inner.ptr.addr() == meta_perm.points_to.addr(), + old(self).inner.inner@.ptr.addr() == meta_perm.addr(), + old(self).inner.inner@.ptr.addr() == meta_perm.points_to.addr(), meta_perm.is_init(), meta_perm.wf(), { diff --git a/ostd/src/sync/rcu/non_null/mod.rs b/ostd/src/sync/rcu/non_null/mod.rs index 5ae148c9e..13da503a7 100644 --- a/ostd/src/sync/rcu/non_null/mod.rs +++ b/ostd/src/sync/rcu/non_null/mod.rs @@ -274,7 +274,7 @@ impl<'a, T> ArcRef<'a, T> { } pub closed spec fn deref_as_arc_spec(&self) -> &Arc { - manually_drop_deref_spec(&self.inner) + &self.inner@ } /// A workaround that Verus does not support implementing spec for Deref trait yet. diff --git a/vstd_extra/src/external/deref.rs b/vstd_extra/src/external/deref.rs index 464f9492f..416b26a5c 100644 --- a/vstd_extra/src/external/deref.rs +++ b/vstd_extra/src/external/deref.rs @@ -1,4 +1,3 @@ -use super::manually_drop::manually_drop_deref_spec; use core::hint::spin_loop; use core::mem::ManuallyDrop; use core::ops::Deref; @@ -47,11 +46,6 @@ pub broadcast axiom fn arc_deref_spec(a: std::sync::Arc) #[trigger] *(a.deref_spec()) == *a, ; -pub broadcast axiom fn manually_drop_deref_spec_eq(v: &ManuallyDrop) - ensures - #[trigger] &**v == manually_drop_deref_spec(v), -; - pub broadcast group group_deref_spec { ref_deref_spec, box_deref_spec, diff --git a/vstd_extra/src/external/manually_drop.rs b/vstd_extra/src/external/manually_drop.rs deleted file mode 100644 index 8c87fe1f0..000000000 --- a/vstd_extra/src/external/manually_drop.rs +++ /dev/null @@ -1,37 +0,0 @@ -use core::mem::ManuallyDrop; -use core::ops::Deref; -use vstd::prelude::*; - -verus! { - -pub uninterp spec fn manually_drop_deref_spec(v: &ManuallyDrop) -> &T; - -pub uninterp spec fn manually_drop_new_spec(v: T) -> ManuallyDrop; - -pub open spec fn manually_drop_unwrap(v: ManuallyDrop) -> T { - *manually_drop_deref_spec(&v) -} - -#[verifier::when_used_as_spec(manually_drop_new_spec)] -pub assume_specification[ ManuallyDrop::new ](v: T) -> (res: ManuallyDrop) - ensures - manually_drop_deref_spec(&res) == &v, - returns - manually_drop_new_spec(v), -; - -#[verifier::when_used_as_spec(manually_drop_deref_spec)] -pub assume_specification[ as Deref>::deref ]( - v: &ManuallyDrop, -) -> (res: &T) - ensures - res == manually_drop_deref_spec(v), -; - -#[verifier::when_used_as_spec(manually_drop_unwrap)] -pub assume_specification[ ManuallyDrop::::into_inner ](v: ManuallyDrop) -> T - returns - manually_drop_unwrap(v), -; - -} // verus! diff --git a/vstd_extra/src/external/mod.rs b/vstd_extra/src/external/mod.rs index 7871a0056..4d7454e3d 100644 --- a/vstd_extra/src/external/mod.rs +++ b/vstd_extra/src/external/mod.rs @@ -1,13 +1,11 @@ // Specifications for external functions and traits pub mod deref; pub mod ilog2; -pub mod manually_drop; pub mod nonnull; pub mod smart_ptr; pub use deref::*; pub use ilog2::*; -pub use manually_drop::*; pub use nonnull::*; pub use smart_ptr::*;