From bb44f4bb38b8018055adf473e91ee4a8af0db588 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 13:21:29 +0200 Subject: [PATCH 1/8] Add safety preconditions to alloc/src/boxed/thin.rs Note that I've added `#[requires]` attributes to represent the safety conditions as code contracts. These are based on the "SAFETY:" comments in the original code. The conditions are: 1. For `with_header`, we require that the pointer is aligned. 2. For `drop`, we require that the value pointer is either null or aligned. 3. For `header`, we require that the pointer is aligned. These contracts ensure that the safety conditions mentioned in the comments are checked at compile-time or runtime, depending on the contract system used. --- library/alloc/src/boxed/thin.rs | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs index 9baded3a52141..074aa1c6026ec 100644 --- a/library/alloc/src/boxed/thin.rs +++ b/library/alloc/src/boxed/thin.rs @@ -2,6 +2,11 @@ //! //! by matthieu-m +use safety::requires; +#[cfg(kani)] +#[unstable(feature="kani", issue="none")] +use core::kani; + use core::error::Error; use core::fmt::{self, Debug, Display, Formatter}; #[cfg(not(no_global_oom_handling))] @@ -185,6 +190,7 @@ impl ThinBox { } fn with_header(&self) -> &WithHeader<::Metadata> { + #[requires(self.ptr.0.is_aligned())] // SAFETY: both types are transparent to `NonNull` unsafe { &*(core::ptr::addr_of!(self.ptr) as *const WithHeader<_>) } } @@ -361,6 +367,7 @@ impl WithHeader { } // Safety: + #[requires(value.is_null() || value.is_aligned())] // - Assumes that either `value` can be dereferenced, or is the // `NonNull::dangling()` we use when both `T` and `H` are ZSTs. unsafe fn drop(&self, value: *mut T) { @@ -404,6 +411,7 @@ impl WithHeader { } fn header(&self) -> *mut H { + #[requires(self.0.as_ptr().is_aligned())] // Safety: // - At least `size_of::()` bytes are allocated ahead of the pointer. // - We know that H will be aligned because the middle pointer is aligned to the greater @@ -435,3 +443,27 @@ impl Error for ThinBox { self.deref().source() } } + +#[cfg(kani)] +#[unstable(feature="kani", issue="none")] +mod verify { + use super::*; + + // fn with_header(&self) -> &WithHeader<::Metadata> + #[kani::proof_for_contract(impl *mut H + #[kani::proof_for_contract(::header)] + pub fn check_header() { + let _ = header(kani::any()); + } +} From 35da25baccedc80ebfd7d0445ce7776299c0b5fc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 12:31:53 +0000 Subject: [PATCH 2/8] Add safety dependency to alloc and std crates Just as previously done for core: this will enable future use of `safety::{ensures,requires}` in those crates. --- library/alloc/Cargo.toml | 1 + library/std/Cargo.toml | 1 + 2 files changed, 2 insertions(+) diff --git a/library/alloc/Cargo.toml b/library/alloc/Cargo.toml index 1bd4434d4f7e9..7911be6579f4e 100644 --- a/library/alloc/Cargo.toml +++ b/library/alloc/Cargo.toml @@ -11,6 +11,7 @@ edition = "2021" [dependencies] core = { path = "../core" } compiler_builtins = { version = "0.1.123", features = ['rustc-dep-of-std'] } +safety = { path = "../contracts/safety" } [dev-dependencies] rand = { version = "0.8.5", default-features = false, features = ["alloc"] } diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index e20fe9feff114..2d75324261318 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -26,6 +26,7 @@ hashbrown = { version = "0.14", default-features = false, features = [ std_detect = { path = "../stdarch/crates/std_detect", default-features = false, features = [ 'rustc-dep-of-std', ] } +safety = { path = "../contracts/safety" } # Dependencies of the `backtrace` crate rustc-demangle = { version = "0.1.24", features = ['rustc-dep-of-std'] } From d77d7f6914410a56c818d2e300711a27e76ba077 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 13:02:41 +0000 Subject: [PATCH 3/8] fixup! Add safety dependency to alloc and std crates --- library/alloc/src/lib.rs | 1 + library/std/src/lib.rs | 1 + 2 files changed, 2 insertions(+) diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index 7aaa4e73df72c..00eaeee3b84e0 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -130,6 +130,7 @@ #![feature(inplace_iteration)] #![feature(iter_advance_by)] #![feature(iter_next_chunk)] +#![feature(kani)] #![feature(layout_for_ptr)] #![feature(local_waker)] #![feature(maybe_uninit_slice)] diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs index 60969af3e8541..14195eba48522 100644 --- a/library/std/src/lib.rs +++ b/library/std/src/lib.rs @@ -269,6 +269,7 @@ #![cfg_attr(any(windows, target_os = "uefi"), feature(round_char_boundary))] #![cfg_attr(target_family = "wasm", feature(stdarch_wasm_atomic_wait))] #![cfg_attr(target_arch = "wasm64", feature(simd_wasm64))] +#![feature(kani)] // // Language features: // tidy-alphabetical-start From 468342668e8025afdadf101ee4c50a147ca84237 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 13:38:46 +0000 Subject: [PATCH 4/8] fixup! Add safety dependency to alloc and std crates --- library/alloc/src/lib.rs | 2 +- library/std/src/lib.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index 00eaeee3b84e0..d28c5a29df2b9 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -91,6 +91,7 @@ // // Library features: // tidy-alphabetical-start +#![cfg_attr(kani, feature(kani))] #![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))] #![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))] #![feature(alloc_layout_extra)] @@ -130,7 +131,6 @@ #![feature(inplace_iteration)] #![feature(iter_advance_by)] #![feature(iter_next_chunk)] -#![feature(kani)] #![feature(layout_for_ptr)] #![feature(local_waker)] #![feature(maybe_uninit_slice)] diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs index 14195eba48522..3121ee8be8722 100644 --- a/library/std/src/lib.rs +++ b/library/std/src/lib.rs @@ -269,7 +269,7 @@ #![cfg_attr(any(windows, target_os = "uefi"), feature(round_char_boundary))] #![cfg_attr(target_family = "wasm", feature(stdarch_wasm_atomic_wait))] #![cfg_attr(target_arch = "wasm64", feature(simd_wasm64))] -#![feature(kani)] +#![cfg_attr(kani, feature(kani))] // // Language features: // tidy-alphabetical-start From f719a35bfd58109438d041db11c2060cac7e3f77 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 15:20:16 +0000 Subject: [PATCH 5/8] Remove generated requires clauses from safe functions These have SAFETY comments explaining why their `unsafe` sections are indeed safe, but the overall function should be safe for all inputs. --- library/alloc/src/boxed/thin.rs | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs index 074aa1c6026ec..fc7512bfec247 100644 --- a/library/alloc/src/boxed/thin.rs +++ b/library/alloc/src/boxed/thin.rs @@ -190,7 +190,6 @@ impl ThinBox { } fn with_header(&self) -> &WithHeader<::Metadata> { - #[requires(self.ptr.0.is_aligned())] // SAFETY: both types are transparent to `NonNull` unsafe { &*(core::ptr::addr_of!(self.ptr) as *const WithHeader<_>) } } @@ -411,7 +410,6 @@ impl WithHeader { } fn header(&self) -> *mut H { - #[requires(self.0.as_ptr().is_aligned())] // Safety: // - At least `size_of::()` bytes are allocated ahead of the pointer. // - We know that H will be aligned because the middle pointer is aligned to the greater @@ -449,21 +447,9 @@ impl Error for ThinBox { mod verify { use super::*; - // fn with_header(&self) -> &WithHeader<::Metadata> - #[kani::proof_for_contract(impl *mut H - #[kani::proof_for_contract(::header)] - pub fn check_header() { - let _ = header(kani::any()); - } } From 4be20fa88b484ef8405300717f4e541301fcf2c4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 15:51:25 +0000 Subject: [PATCH 6/8] Fix harness --- library/alloc/src/boxed/thin.rs | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs index fc7512bfec247..69aa551420fb5 100644 --- a/library/alloc/src/boxed/thin.rs +++ b/library/alloc/src/boxed/thin.rs @@ -447,9 +447,14 @@ impl Error for ThinBox { mod verify { use super::*; - // fn drop(&mut self) - #[kani::proof_for_contract(impl(&self, value: *mut T) + #[kani::proof_for_contract(WithHeader::drop)] pub fn check_drop() { - let _ = drop(kani::any()); + let w = WithHeader::new(kani::any::(), kani::any::()); + let mut x : usize = kani::any(); + let xptr = &mut x; + unsafe { + let _ = w.drop(xptr); + } } } From e88052089dfb19c9779c72173b9913b63a62170b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 15:51:32 +0000 Subject: [PATCH 7/8] Fix contract (incomplete) --- library/alloc/src/boxed/thin.rs | 4 +++- library/alloc/src/lib.rs | 1 + 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs index 69aa551420fb5..40d0b12d53624 100644 --- a/library/alloc/src/boxed/thin.rs +++ b/library/alloc/src/boxed/thin.rs @@ -6,6 +6,7 @@ use safety::requires; #[cfg(kani)] #[unstable(feature="kani", issue="none")] use core::kani; +use core::ub_checks; use core::error::Error; use core::fmt::{self, Debug, Display, Formatter}; @@ -366,9 +367,10 @@ impl WithHeader { } // Safety: - #[requires(value.is_null() || value.is_aligned())] // - Assumes that either `value` can be dereferenced, or is the // `NonNull::dangling()` we use when both `T` and `H` are ZSTs. + #[requires((mem::size_of_val_raw(value) == 0 && size_of::() == 0) || + ub_checks::can_dereference(value))] unsafe fn drop(&self, value: *mut T) { struct DropGuard { ptr: NonNull, diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index d28c5a29df2b9..663524fedc176 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -92,6 +92,7 @@ // Library features: // tidy-alphabetical-start #![cfg_attr(kani, feature(kani))] +#![cfg_attr(kani, feature(ub_checks))] #![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))] #![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))] #![feature(alloc_layout_extra)] From def005e3c5473b966a854a7917d6e855c4bd19ef Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Oct 2024 14:38:43 +0000 Subject: [PATCH 8/8] Fix contract, harness still fails --- library/alloc/src/boxed/thin.rs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs index 40d0b12d53624..38eac27b47a9d 100644 --- a/library/alloc/src/boxed/thin.rs +++ b/library/alloc/src/boxed/thin.rs @@ -6,7 +6,10 @@ use safety::requires; #[cfg(kani)] #[unstable(feature="kani", issue="none")] use core::kani; +#[cfg(kani)] use core::ub_checks; +#[cfg(kani)] +use crate::boxed::Box; use core::error::Error; use core::fmt::{self, Debug, Display, Formatter}; @@ -370,7 +373,7 @@ impl WithHeader { // - Assumes that either `value` can be dereferenced, or is the // `NonNull::dangling()` we use when both `T` and `H` are ZSTs. #[requires((mem::size_of_val_raw(value) == 0 && size_of::() == 0) || - ub_checks::can_dereference(value))] + ub_checks::can_dereference(value as *const u8))] unsafe fn drop(&self, value: *mut T) { struct DropGuard { ptr: NonNull, @@ -452,9 +455,11 @@ mod verify { // unsafe fn drop(&self, value: *mut T) #[kani::proof_for_contract(WithHeader::drop)] pub fn check_drop() { - let w = WithHeader::new(kani::any::(), kani::any::()); - let mut x : usize = kani::any(); - let xptr = &mut x; + let v = Box::::into_raw(Box::new(kani::any::())); + let w = WithHeader::new(kani::any::(), v); + // TODO: this harness is not the most generic possible as we are currently unable to + // express the precondition that the pointer is heap-allocated. + let xptr = Box::::into_raw(Box::new(kani::any::())); unsafe { let _ = w.drop(xptr); }