From db064d4e95a2b3cc9cd330b678f1c13ec56d1fcc Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 18 Aug 2025 15:13:36 -0700 Subject: [PATCH 01/12] add loop invariant and harness for slice repeat --- library/alloc/src/slice.rs | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index ce9f967cc387a..5d84fe04b6856 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -52,6 +52,10 @@ pub use core::slice::{from_mut_ptr_range, from_ptr_range}; pub use core::slice::{from_raw_parts, from_raw_parts_mut}; #[unstable(feature = "slice_range", issue = "76393")] pub use core::slice::{range, try_range}; +#[cfg(kani)] +use crate::kani; +#[cfg(kani)] +use core::ptr::slice_from_raw_parts; //////////////////////////////////////////////////////////////////////////////// // Basic slice extension methods @@ -524,6 +528,18 @@ impl [T] { { let mut m = n >> 1; // If `m > 0`, there are remaining bits up to the leftmost '1'. + #[cfg(kani)] + let buf_ptr= slice_from_raw_parts(buf.as_ptr(), capacity); + #[cfg(kani)] + let len_ptr = unsafe {(&buf as *const Vec as *const usize).add(2)}; + #[kani::loop_invariant( + kani::mem::same_allocation(buf.as_ptr(), buf.as_ptr().wrapping_add(capacity)) && + unsafe {*len_ptr <= T::MAX_SLICE_LEN} && + unsafe {*len_ptr <= capacity} && + m.leading_zeros() > n.leading_zeros() && + unsafe {*len_ptr == sef.len() * (1usize << (m.leading_zeros() - n.leading_zeros() - 1))} + )] + #[kani::loop_modifies(&m, buf_ptr, len_ptr)] while m > 0 { // `buf.extend(buf)`: unsafe { @@ -867,3 +883,23 @@ impl sort::stable::BufGuard for Vec { self.spare_capacity_mut() } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod slice_verify { + use super::*; + + #[kani::proof] + fn check_repeat_u8() { + let mut a: [u8; 10] = kani::any(); + let n = kani::any_where(|i| *i < 10); + let _result = repeat(a.as_slice(), n); + } + + #[kani::proof] + fn check_repeat_u16() { + let mut a: [u16; 10] = kani::any(); + let n = kani::any_where(|i| *i < 10); + let _result = repeat(a.as_slice(), n); + } +} From 9ebc91914d226e2a5460f73ac9f44a9a3dac1fc4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 19 Aug 2025 14:26:07 +0200 Subject: [PATCH 02/12] Formatting --- library/alloc/src/slice.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index 5d84fe04b6856..7bc9f6c20c71c 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -54,8 +54,6 @@ pub use core::slice::{from_raw_parts, from_raw_parts_mut}; pub use core::slice::{range, try_range}; #[cfg(kani)] use crate::kani; -#[cfg(kani)] -use core::ptr::slice_from_raw_parts; //////////////////////////////////////////////////////////////////////////////// // Basic slice extension methods @@ -529,9 +527,9 @@ impl [T] { let mut m = n >> 1; // If `m > 0`, there are remaining bits up to the leftmost '1'. #[cfg(kani)] - let buf_ptr= slice_from_raw_parts(buf.as_ptr(), capacity); + let buf_ptr = ptr::slice_from_raw_parts(buf.as_ptr(), capacity); #[cfg(kani)] - let len_ptr = unsafe {(&buf as *const Vec as *const usize).add(2)}; + let len_ptr = unsafe {(&buf as *const Vec as *const usize).add(2)}; #[kani::loop_invariant( kani::mem::same_allocation(buf.as_ptr(), buf.as_ptr().wrapping_add(capacity)) && unsafe {*len_ptr <= T::MAX_SLICE_LEN} && From f94999db7598dd24e41574865e0ae6679c3897d8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 19 Aug 2025 14:32:02 +0200 Subject: [PATCH 03/12] Formatting --- library/alloc/src/slice.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index 7bc9f6c20c71c..b9401114af5ba 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -52,8 +52,6 @@ pub use core::slice::{from_mut_ptr_range, from_ptr_range}; pub use core::slice::{from_raw_parts, from_raw_parts_mut}; #[unstable(feature = "slice_range", issue = "76393")] pub use core::slice::{range, try_range}; -#[cfg(kani)] -use crate::kani; //////////////////////////////////////////////////////////////////////////////// // Basic slice extension methods @@ -64,6 +62,8 @@ use crate::alloc::Global; #[cfg(not(no_global_oom_handling))] use crate::borrow::ToOwned; use crate::boxed::Box; +#[cfg(kani)] +use crate::kani; use crate::vec::Vec; impl [T] { @@ -529,7 +529,7 @@ impl [T] { #[cfg(kani)] let buf_ptr = ptr::slice_from_raw_parts(buf.as_ptr(), capacity); #[cfg(kani)] - let len_ptr = unsafe {(&buf as *const Vec as *const usize).add(2)}; + let len_ptr = unsafe { (&buf as *const Vec as *const usize).add(2) }; #[kani::loop_invariant( kani::mem::same_allocation(buf.as_ptr(), buf.as_ptr().wrapping_add(capacity)) && unsafe {*len_ptr <= T::MAX_SLICE_LEN} && From 60ceb6250f75b908202b2b073d19b4abd736e8ee Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 19 Aug 2025 14:36:21 +0200 Subject: [PATCH 04/12] Formatting --- library/alloc/src/slice.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index b9401114af5ba..6ca5c4ea90409 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -529,7 +529,7 @@ impl [T] { #[cfg(kani)] let buf_ptr = ptr::slice_from_raw_parts(buf.as_ptr(), capacity); #[cfg(kani)] - let len_ptr = unsafe { (&buf as *const Vec as *const usize).add(2) }; + let len_ptr = unsafe { (&buf as *const Vec as *const usize).add(2) }; #[kani::loop_invariant( kani::mem::same_allocation(buf.as_ptr(), buf.as_ptr().wrapping_add(capacity)) && unsafe {*len_ptr <= T::MAX_SLICE_LEN} && From 8f660c49eee63e8bdf50507bdf58dc88312d691e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 19 Aug 2025 15:03:14 +0200 Subject: [PATCH 05/12] Fix import --- library/alloc/src/slice.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index 6ca5c4ea90409..4f5b2bc4358ae 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -12,6 +12,8 @@ use core::borrow::{Borrow, BorrowMut}; #[cfg(not(no_global_oom_handling))] use core::cmp::Ordering::{self, Less}; +#[cfg(kani)] +use core::kani; #[cfg(not(no_global_oom_handling))] use core::mem::MaybeUninit; #[cfg(not(no_global_oom_handling))] @@ -62,8 +64,6 @@ use crate::alloc::Global; #[cfg(not(no_global_oom_handling))] use crate::borrow::ToOwned; use crate::boxed::Box; -#[cfg(kani)] -use crate::kani; use crate::vec::Vec; impl [T] { From 46ad48ab20c233c41915ba0360e6027959e35c3d Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 19 Aug 2025 07:01:12 -0700 Subject: [PATCH 06/12] add use SizedTypeProperties --- library/alloc/src/slice.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index 5d84fe04b6856..c77bab9f92401 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -56,6 +56,8 @@ pub use core::slice::{range, try_range}; use crate::kani; #[cfg(kani)] use core::ptr::slice_from_raw_parts; +#[cfg(kani)] +use core::mem::SizedTypeProperties; //////////////////////////////////////////////////////////////////////////////// // Basic slice extension methods @@ -532,14 +534,14 @@ impl [T] { let buf_ptr= slice_from_raw_parts(buf.as_ptr(), capacity); #[cfg(kani)] let len_ptr = unsafe {(&buf as *const Vec as *const usize).add(2)}; - #[kani::loop_invariant( + #[safety::loop_invariant( kani::mem::same_allocation(buf.as_ptr(), buf.as_ptr().wrapping_add(capacity)) && unsafe {*len_ptr <= T::MAX_SLICE_LEN} && unsafe {*len_ptr <= capacity} && m.leading_zeros() > n.leading_zeros() && unsafe {*len_ptr == sef.len() * (1usize << (m.leading_zeros() - n.leading_zeros() - 1))} )] - #[kani::loop_modifies(&m, buf_ptr, len_ptr)] + #[safety::loop_modifies(&m, buf_ptr, len_ptr)] while m > 0 { // `buf.extend(buf)`: unsafe { From eaab066d977de584374f9f5760927214c0b21dcc Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 19 Aug 2025 07:04:33 -0700 Subject: [PATCH 07/12] add use SizedTypeProperties --- library/alloc/src/slice.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index c098525e19733..0e5700c2d2706 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -54,15 +54,12 @@ pub use core::slice::{from_mut_ptr_range, from_ptr_range}; pub use core::slice::{from_raw_parts, from_raw_parts_mut}; #[unstable(feature = "slice_range", issue = "76393")] pub use core::slice::{range, try_range}; -<<<<<<< HEAD #[cfg(kani)] use crate::kani; #[cfg(kani)] use core::ptr::slice_from_raw_parts; #[cfg(kani)] use core::mem::SizedTypeProperties; -======= ->>>>>>> 8f660c49eee63e8bdf50507bdf58dc88312d691e //////////////////////////////////////////////////////////////////////////////// // Basic slice extension methods From 9cf51772d716f76d5be5e448cb51f1a2a3709f11 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 19 Aug 2025 07:18:59 -0700 Subject: [PATCH 08/12] fix format --- library/alloc/src/slice.rs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index 0e5700c2d2706..36ecfb23c7a6c 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -16,8 +16,12 @@ use core::cmp::Ordering::{self, Less}; use core::kani; #[cfg(not(no_global_oom_handling))] use core::mem::MaybeUninit; +#[cfg(kani)] +use core::mem::SizedTypeProperties; #[cfg(not(no_global_oom_handling))] use core::ptr; +#[cfg(kani)] +use core::ptr::slice_from_raw_parts; #[unstable(feature = "array_windows", issue = "75027")] pub use core::slice::ArrayWindows; #[stable(feature = "inherent_ascii_escape", since = "1.60.0")] @@ -54,12 +58,6 @@ pub use core::slice::{from_mut_ptr_range, from_ptr_range}; pub use core::slice::{from_raw_parts, from_raw_parts_mut}; #[unstable(feature = "slice_range", issue = "76393")] pub use core::slice::{range, try_range}; -#[cfg(kani)] -use crate::kani; -#[cfg(kani)] -use core::ptr::slice_from_raw_parts; -#[cfg(kani)] -use core::mem::SizedTypeProperties; //////////////////////////////////////////////////////////////////////////////// // Basic slice extension methods @@ -70,6 +68,8 @@ use crate::alloc::Global; #[cfg(not(no_global_oom_handling))] use crate::borrow::ToOwned; use crate::boxed::Box; +#[cfg(kani)] +use crate::kani; use crate::vec::Vec; impl [T] { @@ -535,7 +535,7 @@ impl [T] { #[cfg(kani)] let buf_ptr = ptr::slice_from_raw_parts(buf.as_ptr(), capacity); #[cfg(kani)] - let len_ptr = unsafe {(&buf as *const Vec as *const usize).add(2)}; + let len_ptr = unsafe { (&buf as *const Vec as *const usize).add(2) }; #[safety::loop_invariant( kani::mem::same_allocation(buf.as_ptr(), buf.as_ptr().wrapping_add(capacity)) && unsafe {*len_ptr <= T::MAX_SLICE_LEN} && From d8aa566037200d0ad295ad68402c9571605289fa Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 19 Aug 2025 08:00:20 -0700 Subject: [PATCH 09/12] add feature target for loop invariant --- library/alloc/src/lib.rs | 2 ++ library/alloc/src/slice.rs | 14 +++++++------- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index 97b809233ed0d..a1a7e686aefd6 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -93,6 +93,8 @@ // Library features: // tidy-alphabetical-start #![cfg_attr(kani, feature(kani))] +#![cfg_attr(kani, feature(proc_macro_hygiene))] +#![cfg_attr(kani, feature(stmt_expr_attributes))] #![feature(alloc_layout_extra)] #![feature(allocator_api)] #![feature(array_into_iter_constructors)] diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index 36ecfb23c7a6c..9e350f8ab32f2 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -14,6 +14,8 @@ use core::borrow::{Borrow, BorrowMut}; use core::cmp::Ordering::{self, Less}; #[cfg(kani)] use core::kani; +#[cfg(kani)] +use core::kani; #[cfg(not(no_global_oom_handling))] use core::mem::MaybeUninit; #[cfg(kani)] @@ -68,8 +70,6 @@ use crate::alloc::Global; #[cfg(not(no_global_oom_handling))] use crate::borrow::ToOwned; use crate::boxed::Box; -#[cfg(kani)] -use crate::kani; use crate::vec::Vec; impl [T] { @@ -536,14 +536,14 @@ impl [T] { let buf_ptr = ptr::slice_from_raw_parts(buf.as_ptr(), capacity); #[cfg(kani)] let len_ptr = unsafe { (&buf as *const Vec as *const usize).add(2) }; - #[safety::loop_invariant( + #[cfg_attr(kani, kani::loop_invariant( kani::mem::same_allocation(buf.as_ptr(), buf.as_ptr().wrapping_add(capacity)) && unsafe {*len_ptr <= T::MAX_SLICE_LEN} && unsafe {*len_ptr <= capacity} && m.leading_zeros() > n.leading_zeros() && unsafe {*len_ptr == sef.len() * (1usize << (m.leading_zeros() - n.leading_zeros() - 1))} - )] - #[safety::loop_modifies(&m, buf_ptr, len_ptr)] + ))] + #[cfg_attr(kani, kani::loop_modifies(&m, buf_ptr, len_ptr))] while m > 0 { // `buf.extend(buf)`: unsafe { @@ -897,13 +897,13 @@ pub mod slice_verify { fn check_repeat_u8() { let mut a: [u8; 10] = kani::any(); let n = kani::any_where(|i| *i < 10); - let _result = repeat(a.as_slice(), n); + let _result = a.repeat(n); } #[kani::proof] fn check_repeat_u16() { let mut a: [u16; 10] = kani::any(); let n = kani::any_where(|i| *i < 10); - let _result = repeat(a.as_slice(), n); + let _result = a.repeat(n); } } From b28a36865c29252c476708be1c3a895e86fc4576 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 19 Aug 2025 08:18:31 -0700 Subject: [PATCH 10/12] remove redundant import --- library/alloc/src/lib.rs | 1 - library/alloc/src/slice.rs | 4 +--- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index a1a7e686aefd6..23764ec8ec62f 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -94,7 +94,6 @@ // tidy-alphabetical-start #![cfg_attr(kani, feature(kani))] #![cfg_attr(kani, feature(proc_macro_hygiene))] -#![cfg_attr(kani, feature(stmt_expr_attributes))] #![feature(alloc_layout_extra)] #![feature(allocator_api)] #![feature(array_into_iter_constructors)] diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index 9e350f8ab32f2..f4c453d2e3460 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -14,8 +14,6 @@ use core::borrow::{Borrow, BorrowMut}; use core::cmp::Ordering::{self, Less}; #[cfg(kani)] use core::kani; -#[cfg(kani)] -use core::kani; #[cfg(not(no_global_oom_handling))] use core::mem::MaybeUninit; #[cfg(kani)] @@ -541,7 +539,7 @@ impl [T] { unsafe {*len_ptr <= T::MAX_SLICE_LEN} && unsafe {*len_ptr <= capacity} && m.leading_zeros() > n.leading_zeros() && - unsafe {*len_ptr == sef.len() * (1usize << (m.leading_zeros() - n.leading_zeros() - 1))} + unsafe {*len_ptr == self.len() * (1usize << (m.leading_zeros() - n.leading_zeros() - 1))} ))] #[cfg_attr(kani, kani::loop_modifies(&m, buf_ptr, len_ptr))] while m > 0 { From 67758db92be7b94e0c048fd00ce572a4ce495529 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 19 Aug 2025 08:36:57 -0700 Subject: [PATCH 11/12] add ptr type --- library/alloc/src/slice.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index f4c453d2e3460..5fab702b7311e 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -535,7 +535,7 @@ impl [T] { #[cfg(kani)] let len_ptr = unsafe { (&buf as *const Vec as *const usize).add(2) }; #[cfg_attr(kani, kani::loop_invariant( - kani::mem::same_allocation(buf.as_ptr(), buf.as_ptr().wrapping_add(capacity)) && + kani::mem::same_allocation(buf.as_ptr() as *const T, (buf.as_ptr() as *const T).wrapping_add(capacity)) && unsafe {*len_ptr <= T::MAX_SLICE_LEN} && unsafe {*len_ptr <= capacity} && m.leading_zeros() > n.leading_zeros() && From 2a05d069fc84482294b1f800038ffb28a6f51b27 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 22 Aug 2025 10:44:16 +0200 Subject: [PATCH 12/12] Try to use Z3 --- library/alloc/src/slice.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/alloc/src/slice.rs b/library/alloc/src/slice.rs index 5fab702b7311e..cf68e8b94ab1d 100644 --- a/library/alloc/src/slice.rs +++ b/library/alloc/src/slice.rs @@ -892,6 +892,7 @@ pub mod slice_verify { use super::*; #[kani::proof] + #[kani::solver(z3)] fn check_repeat_u8() { let mut a: [u8; 10] = kani::any(); let n = kani::any_where(|i| *i < 10);