From 9822a02ee7d2b1c0106e6a0bdc2ee3d96369fdf2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 13:15:17 +0200 Subject: [PATCH 01/11] Add safety preconditions to alloc/src/alloc.rs These changes add code contracts in the form of `#[requires(...)]` attributes to various methods in the `Global` allocator implementation. These contracts ensure that the safety conditions mentioned in the comments are explicitly stated as preconditions for the functions. --- library/alloc/src/alloc.rs | 71 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 71 insertions(+) diff --git a/library/alloc/src/alloc.rs b/library/alloc/src/alloc.rs index cddf4f6f39963..d42d1bea45175 100644 --- a/library/alloc/src/alloc.rs +++ b/library/alloc/src/alloc.rs @@ -6,6 +6,10 @@ #[doc(inline)] pub use core::alloc::*; #[cfg(not(test))] +use safety::requires; +#[cfg(kani)] +use crate::kani; + use core::hint; #[cfg(not(test))] use core::ptr::{self, NonNull}; @@ -174,6 +178,7 @@ pub unsafe fn alloc_zeroed(layout: Layout) -> *mut u8 { impl Global { #[inline] fn alloc_impl(&self, layout: Layout, zeroed: bool) -> Result, AllocError> { + #[requires(layout.size() == 0 || layout.align() != 0)] match layout.size() { 0 => Ok(NonNull::slice_from_raw_parts(layout.dangling(), 0)), // SAFETY: `layout` is non-zero in size, @@ -186,6 +191,10 @@ impl Global { } // SAFETY: Same as `Allocator::grow` + #[requires(new_layout.size() >= old_layout.size())] + #[requires(old_layout.size() == 0 || old_layout.align() != 0)] + #[requires(new_layout.size() == 0 || new_layout.align() != 0)] + #[requires(ptr.as_ptr() as usize % old_layout.align() == 0)] #[inline] unsafe fn grow_impl( &self, @@ -247,6 +256,8 @@ unsafe impl Allocator for Global { } #[inline] + #[requires(layout.size() == 0 || layout.align() != 0)] + #[requires(ptr.as_ptr() as usize % layout.align() == 0)] unsafe fn deallocate(&self, ptr: NonNull, layout: Layout) { if layout.size() != 0 { // SAFETY: `layout` is non-zero in size, @@ -256,6 +267,10 @@ unsafe impl Allocator for Global { } #[inline] + #[requires(new_layout.size() >= old_layout.size())] + #[requires(old_layout.size() == 0 || old_layout.align() != 0)] + #[requires(new_layout.size() == 0 || new_layout.align() != 0)] + #[requires(ptr.as_ptr() as usize % old_layout.align() == 0)] unsafe fn grow( &self, ptr: NonNull, @@ -267,6 +282,10 @@ unsafe impl Allocator for Global { } #[inline] + #[requires(new_layout.size() >= old_layout.size())] + #[requires(old_layout.size() == 0 || old_layout.align() != 0)] + #[requires(new_layout.size() == 0 || new_layout.align() != 0)] + #[requires(ptr.as_ptr() as usize % old_layout.align() == 0)] unsafe fn grow_zeroed( &self, ptr: NonNull, @@ -278,6 +297,10 @@ unsafe impl Allocator for Global { } #[inline] + #[requires(new_layout.size() <= old_layout.size())] + #[requires(old_layout.size() == 0 || old_layout.align() != 0)] + #[requires(new_layout.size() == 0 || new_layout.align() != 0)] + #[requires(ptr.as_ptr() as usize % old_layout.align() == 0)] unsafe fn shrink( &self, ptr: NonNull, @@ -423,3 +446,51 @@ pub mod __alloc_error_handler { } } } + +#[cfg(kani)] +#[unstable(feature="kani", issue="none")] +mod verify { + use super::*; + + // fn alloc_impl(&self, layout: Layout, zeroed: bool) -> Result, AllocError> + #[kani::proof_for_contract(Global::alloc_impl)] + pub fn check_alloc_impl() { + let obj : Global = kani::any(); + let _ = obj.alloc_impl(kani::any()); + } + + // unsafe fn grow_impl(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout, zeroed: bool) -> Result, AllocError> + #[kani::proof_for_contract(Global::grow_impl)] + pub fn check_grow_impl() { + let obj : Global = kani::any(); + let _ = obj.grow_impl(kani::any()); + } + + // unsafe fn deallocate(&self, ptr: NonNull, layout: Layout) + #[kani::proof_for_contract(Allocator::deallocate)] + pub fn check_deallocate() { + let obj : Allocator = kani::any(); + let _ = obj.deallocate(kani::any()); + } + + // unsafe fn grow(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> + #[kani::proof_for_contract(Allocator::grow)] + pub fn check_grow() { + let obj : Allocator = kani::any(); + let _ = obj.grow(kani::any()); + } + + // unsafe fn grow_zeroed(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> + #[kani::proof_for_contract(Allocator::grow_zeroed)] + pub fn check_grow_zeroed() { + let obj : Allocator = kani::any(); + let _ = obj.grow_zeroed(kani::any()); + } + + // unsafe fn shrink(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> + #[kani::proof_for_contract(Allocator::shrink)] + pub fn check_shrink() { + let obj : Allocator = kani::any(); + let _ = obj.shrink(kani::any()); + } +} From 80a888621f889be2a7a5b65968b6ee9921dc7d0f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 12:31:53 +0000 Subject: [PATCH 02/11] 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 f68538954068c720e0f6a8b565c6b344156ae362 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 12:35:47 +0000 Subject: [PATCH 03/11] Fix placement of use directives --- library/alloc/src/alloc.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/library/alloc/src/alloc.rs b/library/alloc/src/alloc.rs index d42d1bea45175..303336ddb4756 100644 --- a/library/alloc/src/alloc.rs +++ b/library/alloc/src/alloc.rs @@ -6,14 +6,15 @@ #[doc(inline)] pub use core::alloc::*; #[cfg(not(test))] -use safety::requires; -#[cfg(kani)] -use crate::kani; - use core::hint; #[cfg(not(test))] use core::ptr::{self, NonNull}; +use safety::requires; +#[cfg(kani)] +#[unstable(feature="kani", issue="none")] +use core::kani; + #[cfg(test)] mod tests; From f529e5d8cd53849a2a36765c9e5d9459694c9e7c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 13:02:16 +0000 Subject: [PATCH 04/11] Fix placement of requires clause --- library/alloc/src/alloc.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/alloc/src/alloc.rs b/library/alloc/src/alloc.rs index 303336ddb4756..3443e3216fa09 100644 --- a/library/alloc/src/alloc.rs +++ b/library/alloc/src/alloc.rs @@ -177,9 +177,9 @@ pub unsafe fn alloc_zeroed(layout: Layout) -> *mut u8 { #[cfg(not(test))] impl Global { + #[requires(layout.size() == 0 || layout.align() != 0)] #[inline] fn alloc_impl(&self, layout: Layout, zeroed: bool) -> Result, AllocError> { - #[requires(layout.size() == 0 || layout.align() != 0)] match layout.size() { 0 => Ok(NonNull::slice_from_raw_parts(layout.dangling(), 0)), // SAFETY: `layout` is non-zero in size, From 71061d395090780a18db102f5efbe22d7e8abbd1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 13:02:41 +0000 Subject: [PATCH 05/11] 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 247d3be956968a2ae4fe188dbc83a70a5dfc2594 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 13:32:07 +0000 Subject: [PATCH 06/11] Fix harnesses --- library/alloc/src/alloc.rs | 42 +++++++++++++++++++++++++++----------- 1 file changed, 30 insertions(+), 12 deletions(-) diff --git a/library/alloc/src/alloc.rs b/library/alloc/src/alloc.rs index 3443e3216fa09..ecb58645ab005 100644 --- a/library/alloc/src/alloc.rs +++ b/library/alloc/src/alloc.rs @@ -456,42 +456,60 @@ mod verify { // fn alloc_impl(&self, layout: Layout, zeroed: bool) -> Result, AllocError> #[kani::proof_for_contract(Global::alloc_impl)] pub fn check_alloc_impl() { - let obj : Global = kani::any(); - let _ = obj.alloc_impl(kani::any()); + let _ = Global.alloc_impl(kani::any(), kani::any()); } // unsafe fn grow_impl(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout, zeroed: bool) -> Result, AllocError> #[kani::proof_for_contract(Global::grow_impl)] pub fn check_grow_impl() { - let obj : Global = kani::any(); - let _ = obj.grow_impl(kani::any()); + let raw_ptr = kani::any::() as *mut u8; + unsafe { + let n = NonNull::new_unchecked(raw_ptr); + let _ = Global.grow_impl(n, kani::any(), kani::any(), kani::any()); + } } // unsafe fn deallocate(&self, ptr: NonNull, layout: Layout) #[kani::proof_for_contract(Allocator::deallocate)] pub fn check_deallocate() { - let obj : Allocator = kani::any(); - let _ = obj.deallocate(kani::any()); + let obj : &dyn Allocator = &Global; + let raw_ptr = kani::any::() as *mut u8; + unsafe { + let n = NonNull::new_unchecked(raw_ptr); + let _ = obj.deallocate(n, kani::any()); + } } // unsafe fn grow(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> #[kani::proof_for_contract(Allocator::grow)] pub fn check_grow() { - let obj : Allocator = kani::any(); - let _ = obj.grow(kani::any()); + let obj : &dyn Allocator = &Global; + let raw_ptr = kani::any::() as *mut u8; + unsafe { + let n = NonNull::new_unchecked(raw_ptr); + let _ = obj.grow(n, kani::any(), kani::any()); + } } // unsafe fn grow_zeroed(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> #[kani::proof_for_contract(Allocator::grow_zeroed)] pub fn check_grow_zeroed() { - let obj : Allocator = kani::any(); - let _ = obj.grow_zeroed(kani::any()); + let obj : &dyn Allocator = &Global; + let raw_ptr = kani::any::() as *mut u8; + unsafe { + let n = NonNull::new_unchecked(raw_ptr); + let _ = obj.grow_zeroed(n, kani::any(), kani::any()); + } } // unsafe fn shrink(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> #[kani::proof_for_contract(Allocator::shrink)] pub fn check_shrink() { - let obj : Allocator = kani::any(); - let _ = obj.shrink(kani::any()); + let obj : &dyn Allocator = &Global; + let raw_ptr = kani::any::() as *mut u8; + unsafe { + let n = NonNull::new_unchecked(raw_ptr); + let _ = obj.shrink(n, kani::any(), kani::any()); + } } } From f17509eb2065a8122443f2a0e478289984bb6fba Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 17 Oct 2024 13:38:46 +0000 Subject: [PATCH 07/11] 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 cb4b65069e60bcb132ae3a14cf220d92e7e6e0b0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Oct 2024 12:51:57 +0000 Subject: [PATCH 08/11] Disable unsupported harnesses of trait contracts --- library/alloc/src/alloc.rs | 90 ++++++++++++++++++++------------------ 1 file changed, 47 insertions(+), 43 deletions(-) diff --git a/library/alloc/src/alloc.rs b/library/alloc/src/alloc.rs index ecb58645ab005..fc499d43e9851 100644 --- a/library/alloc/src/alloc.rs +++ b/library/alloc/src/alloc.rs @@ -469,47 +469,51 @@ mod verify { } } - // unsafe fn deallocate(&self, ptr: NonNull, layout: Layout) - #[kani::proof_for_contract(Allocator::deallocate)] - pub fn check_deallocate() { - let obj : &dyn Allocator = &Global; - let raw_ptr = kani::any::() as *mut u8; - unsafe { - let n = NonNull::new_unchecked(raw_ptr); - let _ = obj.deallocate(n, kani::any()); - } - } - - // unsafe fn grow(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> - #[kani::proof_for_contract(Allocator::grow)] - pub fn check_grow() { - let obj : &dyn Allocator = &Global; - let raw_ptr = kani::any::() as *mut u8; - unsafe { - let n = NonNull::new_unchecked(raw_ptr); - let _ = obj.grow(n, kani::any(), kani::any()); - } - } - - // unsafe fn grow_zeroed(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> - #[kani::proof_for_contract(Allocator::grow_zeroed)] - pub fn check_grow_zeroed() { - let obj : &dyn Allocator = &Global; - let raw_ptr = kani::any::() as *mut u8; - unsafe { - let n = NonNull::new_unchecked(raw_ptr); - let _ = obj.grow_zeroed(n, kani::any(), kani::any()); - } - } - - // unsafe fn shrink(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> - #[kani::proof_for_contract(Allocator::shrink)] - pub fn check_shrink() { - let obj : &dyn Allocator = &Global; - let raw_ptr = kani::any::() as *mut u8; - unsafe { - let n = NonNull::new_unchecked(raw_ptr); - let _ = obj.shrink(n, kani::any(), kani::any()); - } - } + // TODO: disabled as Kani does not currently support contracts on traits + // // unsafe fn deallocate(&self, ptr: NonNull, layout: Layout) + // #[kani::proof_for_contract(Allocator::deallocate)] + // pub fn check_deallocate() { + // let obj : &dyn Allocator = &Global; + // let raw_ptr = kani::any::() as *mut u8; + // unsafe { + // let n = NonNull::new_unchecked(raw_ptr); + // let _ = obj.deallocate(n, kani::any()); + // } + // } + + // TODO: disabled as Kani does not currently support contracts on traits + // // unsafe fn grow(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> + // #[kani::proof_for_contract(Allocator::grow)] + // pub fn check_grow() { + // let obj : &dyn Allocator = &Global; + // let raw_ptr = kani::any::() as *mut u8; + // unsafe { + // let n = NonNull::new_unchecked(raw_ptr); + // let _ = obj.grow(n, kani::any(), kani::any()); + // } + // } + + // TODO: disabled as Kani does not currently support contracts on traits + // // unsafe fn grow_zeroed(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> + // #[kani::proof_for_contract(Allocator::grow_zeroed)] + // pub fn check_grow_zeroed() { + // let obj : &dyn Allocator = &Global; + // let raw_ptr = kani::any::() as *mut u8; + // unsafe { + // let n = NonNull::new_unchecked(raw_ptr); + // let _ = obj.grow_zeroed(n, kani::any(), kani::any()); + // } + // } + + // TODO: disabled as Kani does not currently support contracts on traits + // // unsafe fn shrink(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> + // #[kani::proof_for_contract(Allocator::shrink)] + // pub fn check_shrink() { + // let obj : &dyn Allocator = &Global; + // let raw_ptr = kani::any::() as *mut u8; + // unsafe { + // let n = NonNull::new_unchecked(raw_ptr); + // let _ = obj.shrink(n, kani::any(), kani::any()); + // } + // } } From b1bad7a1db6d14edc2160f54738a0e2612d89da7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Oct 2024 13:01:19 +0000 Subject: [PATCH 09/11] Global::alloc_impl isn't unsafe, so we should only have post-conditions --- library/alloc/src/alloc.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/alloc/src/alloc.rs b/library/alloc/src/alloc.rs index fc499d43e9851..b0b4c05aaa46f 100644 --- a/library/alloc/src/alloc.rs +++ b/library/alloc/src/alloc.rs @@ -10,7 +10,7 @@ use core::hint; #[cfg(not(test))] use core::ptr::{self, NonNull}; -use safety::requires; +use safety::{ensures,requires}; #[cfg(kani)] #[unstable(feature="kani", issue="none")] use core::kani; @@ -177,8 +177,8 @@ pub unsafe fn alloc_zeroed(layout: Layout) -> *mut u8 { #[cfg(not(test))] impl Global { - #[requires(layout.size() == 0 || layout.align() != 0)] #[inline] + #[ensures(|ret| layout.size() != 0 || ret.is_ok())] fn alloc_impl(&self, layout: Layout, zeroed: bool) -> Result, AllocError> { match layout.size() { 0 => Ok(NonNull::slice_from_raw_parts(layout.dangling(), 0)), From d28ca19ccf90a1cffadd6bfefb97a00aed18d430 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Oct 2024 13:05:08 +0000 Subject: [PATCH 10/11] fixup! Disable unsupported harnesses of trait contracts --- library/alloc/src/alloc.rs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/library/alloc/src/alloc.rs b/library/alloc/src/alloc.rs index b0b4c05aaa46f..a198531104ff4 100644 --- a/library/alloc/src/alloc.rs +++ b/library/alloc/src/alloc.rs @@ -469,7 +469,8 @@ mod verify { } } - // TODO: disabled as Kani does not currently support contracts on traits + // TODO: disabled as Kani does not currently support contracts on traits. See + // https://github.com/model-checking/kani/issues/1997 // // unsafe fn deallocate(&self, ptr: NonNull, layout: Layout) // #[kani::proof_for_contract(Allocator::deallocate)] // pub fn check_deallocate() { @@ -481,7 +482,8 @@ mod verify { // } // } - // TODO: disabled as Kani does not currently support contracts on traits + // TODO: disabled as Kani does not currently support contracts on traits. See + // https://github.com/model-checking/kani/issues/1997 // // unsafe fn grow(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> // #[kani::proof_for_contract(Allocator::grow)] // pub fn check_grow() { @@ -493,7 +495,8 @@ mod verify { // } // } - // TODO: disabled as Kani does not currently support contracts on traits + // TODO: disabled as Kani does not currently support contracts on traits. See + // https://github.com/model-checking/kani/issues/1997 // // unsafe fn grow_zeroed(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> // #[kani::proof_for_contract(Allocator::grow_zeroed)] // pub fn check_grow_zeroed() { @@ -505,7 +508,8 @@ mod verify { // } // } - // TODO: disabled as Kani does not currently support contracts on traits + // TODO: disabled as Kani does not currently support contracts on traits. See + // https://github.com/model-checking/kani/issues/1997 // // unsafe fn shrink(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout) -> Result, AllocError> // #[kani::proof_for_contract(Allocator::shrink)] // pub fn check_shrink() { From d640ef60c9c17ac5c72b49facc833cd3be1879de Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Oct 2024 13:30:31 +0000 Subject: [PATCH 11/11] Disable check_grow_impl as we cannot currently express the necessary precondition --- library/alloc/src/alloc.rs | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/library/alloc/src/alloc.rs b/library/alloc/src/alloc.rs index a198531104ff4..44b1c680c5e9b 100644 --- a/library/alloc/src/alloc.rs +++ b/library/alloc/src/alloc.rs @@ -459,15 +459,17 @@ mod verify { let _ = Global.alloc_impl(kani::any(), kani::any()); } - // unsafe fn grow_impl(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout, zeroed: bool) -> Result, AllocError> - #[kani::proof_for_contract(Global::grow_impl)] - pub fn check_grow_impl() { - let raw_ptr = kani::any::() as *mut u8; - unsafe { - let n = NonNull::new_unchecked(raw_ptr); - let _ = Global.grow_impl(n, kani::any(), kani::any(), kani::any()); - } - } + // TODO: Kani correctly detects that the precondition is too weak. We'd need a way to express + // that ptr either points to a ZST (we can do this), or else is heap-allocated (we cannot). + // // unsafe fn grow_impl(&self, ptr: NonNull, old_layout: Layout, new_layout: Layout, zeroed: bool) -> Result, AllocError> + // #[kani::proof_for_contract(Global::grow_impl)] + // pub fn check_grow_impl() { + // let raw_ptr = kani::any::() as *mut u8; + // unsafe { + // let n = NonNull::new_unchecked(raw_ptr); + // let _ = Global.grow_impl(n, kani::any(), kani::any(), kani::any()); + // } + // } // TODO: disabled as Kani does not currently support contracts on traits. See // https://github.com/model-checking/kani/issues/1997