Upgrade to Rust-1.82 (#4)

* Upgrade verus to support v1.82. * Cleanup build.rs * Set verus lib and tool to the rev supporting v1.82 Signed-off-by: Ziqiao Zhou <[email protected]> * Move vstd.verus.rs to verus vstd & mark memory-related as external * memory related verification needs to add a memory permission and will do it later Signed-off-by: Ziqiao Zhou <[email protected]> * Revert unnecessary change after verus upgrade * revert rust version * revert some code due to version change Signed-off-by: Ziqiao Zhou <[email protected]> * fmt --------- Signed-off-by: Ziqiao Zhou <[email protected]>
coconut-svsm · Oct 30, 2024 · c74be0a · c74be0a
1 parent 9880bdf
commit c74be0a
Show file tree

Hide file tree

Showing 12 changed files with 59 additions and 112 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -54,9 +54,9 @@ zerocopy = { version = "0.8.2", features = ["alloc", "derive"] }
 packit = { git = "https://github.com/coconut-svsm/packit", version = "0.1.1" }
 
 # Verus repos
-builtin = { git = "https://github.com/verus-lang/verus", rev ="2776465", default-features = false }
-builtin_macros = { git = "https://github.com/verus-lang/verus", rev ="2776465", default-features = false }
-vstd = { git = "https://github.com/verus-lang/verus", rev ="2776465", features = ["alloc"], default-features = false }
+builtin = { git = "https://github.com/verus-lang/verus", rev ="31a272f", default-features = false }
+builtin_macros = { git = "https://github.com/verus-lang/verus", rev ="31a272f", default-features = false }
+vstd = { git = "https://github.com/verus-lang/verus", rev ="31a272f", features = ["alloc"], default-features = false }
 
 # Verification libs
 verify_proof = { path = "verify_proof", default-features = false  }

diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml
@@ -2,7 +2,7 @@
 name = "svsm"
 version = "0.1.0"
 edition = "2021"
-rust-version = "1.77.0"
+rust-version = "1.82.0"
 
 [[bin]]
 name = "stage2"

diff --git a/kernel/build.rs b/kernel/build.rs
@@ -4,27 +4,17 @@
 //
 // Author: Joerg Roedel <[email protected]>
 
-use rustc_version::{Channel, Version};
-
 fn main() {
-    let rust_version = rustc_version::version_meta().unwrap();
-    // Check if the version is nightly and higher than 1.78.0
-    let is_expected_version = rust_version.semver >= Version::new(1, 78, 0);
-    if !is_expected_version {
-        if rust_version.channel == Channel::Nightly {
-            // Print the cargo:rustc-cfg directive to enable the feature
-            println!("cargo:rustc-cfg=RUST_BEFORE_1_78");
-        } else {
-            // Optionally handle the case for non-nightly versions
-            panic!("Requires the nightly version or stable version >= 1.78.");
-        }
-    } else {
-        // Extra cfgs
-        println!("cargo::rustc-check-cfg=cfg(fuzzing)");
-        println!("cargo::rustc-check-cfg=cfg(test_in_svsm)");
-        println!("cargo::rustc-check-cfg=cfg(verus_keep_ghost)");
-        println!("cargo::rustc-check-cfg=cfg(RUST_BEFORE_1_78)");
+    // Verification tool only support rust version lower than 1.82
+    // If new features are used, may need to disable them until verus is upraded.
+    if rustc_version::version_meta().unwrap().semver > rustc_version::Version::new(1, 80, 2) {
+        println!("cargo:rustc-cfg=RUST_VERSION_AFTER_VERUS");
     }
+    // Extra cfgs
+    println!("cargo::rustc-check-cfg=cfg(fuzzing)");
+    println!("cargo::rustc-check-cfg=cfg(test_in_svsm)");
+    println!("cargo::rustc-check-cfg=cfg(verus_keep_ghost)");
+    println!("cargo::rustc-check-cfg=cfg(RUST_VERSION_AFTER_VERUS)");
 
     // Stage 2
     println!("cargo:rustc-link-arg-bin=stage2=-nostdlib");

diff --git a/kernel/src/address.rs b/kernel/src/address.rs
@@ -268,11 +268,13 @@ impl VirtAddr {
     }
 
     #[inline]
+    #[verus_verify(external_body)]
     pub fn as_ptr<T>(&self) -> *const T {
         self.0 as *const T
     }
 
     #[inline]
+    #[verus_verify(external_body)]
     pub fn as_mut_ptr<T>(&self) -> *mut T {
         self.0 as *mut T
     }
@@ -285,6 +287,7 @@ impl VirtAddr {
     /// All safety requirements for pointers apply, minus alignment and NULL
     /// checks, which this function already does.
     #[inline]
+    #[verus_verify(external_body)]
     pub unsafe fn aligned_ref<'a, T>(&self) -> Option<&'a T> {
         self.is_aligned_to::<T>()
             .then(|| self.as_ptr::<T>().as_ref())
@@ -299,6 +302,7 @@ impl VirtAddr {
     /// All safety requirements for pointers apply, minus alignment and NULL
     /// checks, which this function already does.
     #[inline]
+    #[verus_verify(external)]
     pub unsafe fn aligned_mut<'a, T>(&self) -> Option<&'a mut T> {
         self.is_aligned_to::<T>()
             .then(|| self.as_mut_ptr::<T>().as_mut())
@@ -327,6 +331,7 @@ impl VirtAddr {
     ///
     /// All Safety requirements from [`core::slice::from_raw_parts`] for the
     /// data pointed to by the `VirtAddr` apply here as well.
+    #[verus_verify(external_body)]
     pub unsafe fn to_slice<T>(&self, len: usize) -> &[T] {
         slice::from_raw_parts::<T>(self.as_ptr::<T>(), len)
     }

diff --git a/kernel/src/address.verus.rs b/kernel/src/address.verus.rs
@@ -34,9 +34,9 @@ broadcast group vaddr_impl_proof {
 }
 
 broadcast use vaddr_impl_proof;
+
 /// Define a broadcast function and its related spec function calls in a inner
 /// module to avoid cyclic self-reference
-
 mod address_spec { include!("address_inner.verus.rs");  }
 
 #[cfg(verus_keep_ghost)]

diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
@@ -5,8 +5,6 @@
 // Author: Nicolai Stange <[email protected]>
 
 #![no_std]
-#![cfg_attr(RUST_BEFORE_1_78, feature(offset_of))] // stable feature after v1.78 but nightly feature in v1.77
-#![cfg_attr(RUST_BEFORE_1_78, feature(inline_const))] // stable feature in v1.78 but nightly feature in v1.77
 #![cfg_attr(all(test, test_in_svsm), no_main)]
 #![cfg_attr(all(test, test_in_svsm), feature(custom_test_frameworks))]
 #![cfg_attr(all(test, test_in_svsm), test_runner(crate::testing::svsm_test_runner))]

diff --git a/kernel/src/mm/page_visibility.rs b/kernel/src/mm/page_visibility.rs
@@ -135,7 +135,7 @@ impl<T> SharedBox<T> {
             copy_bytes(
                 self.ptr.as_ptr() as usize,
                 out as *const T as usize,
-                core::mem::size_of::<T>(),
+                size_of::<T>(),
             );
         }
     }
@@ -150,7 +150,7 @@ impl<T> SharedBox<T> {
             copy_bytes(
                 value as *const T as usize,
                 self.ptr.as_ptr() as usize,
-                core::mem::size_of::<T>(),
+                size_of::<T>(),
             );
         }
     }
@@ -175,7 +175,7 @@ impl<T, const N: usize> SharedBox<[T; N]> {
 
         unsafe {
             // SAFETY: `self.ptr` is valid and we did a bounds check on `n`.
-            write_bytes(self.ptr.as_ptr() as usize, core::mem::size_of::<T>() * n, 0);
+            write_bytes(self.ptr.as_ptr() as usize, size_of::<T>() * n, 0);
         }
 
         Ok(())
@@ -210,7 +210,7 @@ unsafe impl<T> Sync for SharedBox<T> where T: Sync {}
 impl<T> Drop for SharedBox<T> {
     fn drop(&mut self) {
         // Re-encrypt the pages.
-        let res = (0..core::mem::size_of::<Self>())
+        let res = (0..size_of::<Self>())
             .step_by(PAGE_SIZE)
             .try_for_each(|offset| unsafe { make_page_private(self.addr() + offset) });
 

diff --git a/kernel/src/svsm.rs b/kernel/src/svsm.rs
@@ -95,7 +95,7 @@ global_asm!(
 static CPUID_PAGE: ImmutAfterInitCell<SnpCpuidTable> = ImmutAfterInitCell::uninit();
 static LAUNCH_INFO: ImmutAfterInitCell<KernelLaunchInfo> = ImmutAfterInitCell::uninit();
 
-const _: () = assert!(core::mem::size_of::<SnpCpuidTable>() <= PAGE_SIZE);
+const _: () = assert!(size_of::<SnpCpuidTable>() <= PAGE_SIZE);
 
 fn copy_cpuid_table_to_fw(fw_addr: PhysAddr) -> Result<(), SvsmError> {
     let guard = PerCPUPageMappingGuard::create_4k(fw_addr)?;