From d3ef481a4ca97fb1d55c057ba72916a3ddb69c68 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 24 Oct 2024 13:36:18 -0500 Subject: [PATCH 1/8] Add loop contracts and harness for str::small_slice_eq --- library/core/src/lib.rs | 1 + library/core/src/str/pattern.rs | 50 ++++++++++++++++++++++++++++++++- scripts/run-kani.sh | 2 +- 3 files changed, 51 insertions(+), 2 deletions(-) diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 402c1e05b4400..7873a2a44c679 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -263,6 +263,7 @@ #![feature(tbm_target_feature)] #![feature(wasm_target_feature)] #![feature(x86_amx_intrinsics)] +#![cfg_attr(kani, feature(proc_macro_hygiene))] // tidy-alphabetical-end // allow using `core::` in intra-doc links diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 2f1096db8f00c..eda8ca17746dd 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -43,6 +43,13 @@ use crate::convert::TryInto as _; use crate::slice::memchr; use crate::{cmp, fmt}; +use safety::{requires, ensures}; + +#[cfg(kani)] +use crate::kani; +#[cfg(kani)] +use crate::kani::mem::same_allocation; + // Pattern /// A string pattern. @@ -1880,8 +1887,9 @@ fn simd_contains(needle: &str, haystack: &str) -> Option { /// # Safety /// /// Both slices must have the same length. -#[cfg(all(target_arch = "x86_64", target_feature = "sse2"))] // only called on x86 +#[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] // only called on x86 #[inline] +#[requires(x.len() == y.len())] unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { debug_assert_eq!(x.len(), y.len()); // This function is adapted from @@ -1926,6 +1934,10 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { unsafe { let (mut px, mut py) = (x.as_ptr(), y.as_ptr()); let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4)); + #[cfg_attr(kani, kani::loop_invariant(same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py) + && px as isize >= x.as_ptr() as isize + && py as isize >= y.as_ptr() as isize + && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize)))] while px < pxend { let vx = (px as *const u32).read_unaligned(); let vy = (py as *const u32).read_unaligned(); @@ -1940,3 +1952,39 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { vx == vy } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use super::*; + + // Copied from https://github.com/model-checking/kani/blob/main/library/kani/src/slice.rs + // should be removed when these functions are moved to `kani_core` + pub fn any_slice_of_array(arr: &[T; LENGTH]) -> &[T] { + let (from, to) = any_range::(); + &arr[from..to] + } + + fn any_range() -> (usize, usize) { + let from: usize = kani::any(); + let to: usize = kani::any(); + kani::assume(to <= LENGTH); + kani::assume(from <= to); + (from, to) + } + + #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86 + #[kani::proof] + #[kani::unwind(4)] + pub fn check_small_slice_eq() { + const ARR_SIZE: usize = 1000; + let x: [u8; ARR_SIZE] = kani::any(); + let y: [u8; ARR_SIZE] = kani::any(); + let xs = any_slice_of_array(&x); + let ys = any_slice_of_array(&y); + kani::assume(xs.len() == ys.len()); + unsafe { + small_slice_eq(xs, ys); + } + } +} diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 8ce27dac5d207..310ee6a1adf2c 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -183,7 +183,7 @@ main() { echo "Running Kani verify-std command..." - "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args + "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 8 } main From 6f1e8794d01254c5b130514554e25a1a2f513f7b Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 7 Nov 2024 15:12:26 -0600 Subject: [PATCH 2/8] Remove proof without contracts for testing --- library/core/src/alloc/layout.rs | 4 ++-- library/core/src/lib.rs | 2 +- library/core/src/num/mod.rs | 4 ++-- library/core/src/ptr/unique.rs | 6 +++--- library/core/src/str/pattern.rs | 25 ++++++------------------- library/core/src/unicode/mod.rs | 4 ++-- 6 files changed, 16 insertions(+), 29 deletions(-) diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs index 808e2245045e0..83590c20dfa2a 100644 --- a/library/core/src/alloc/layout.rs +++ b/library/core/src/alloc/layout.rs @@ -655,7 +655,7 @@ mod verify { } // pub const fn size(&self) -> usize - #[kani::proof] + //#[kani::proof] pub fn check_size() { let s = kani::any::(); let a = kani::any::(); @@ -667,7 +667,7 @@ mod verify { } // pub const fn align(&self) -> usize - #[kani::proof] + //#[kani::proof] pub fn check_align() { let layout = kani::any::(); assert!(layout.align().is_power_of_two()); diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 2137ad785016e..8331248c8f883 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -230,6 +230,7 @@ #![feature(unboxed_closures)] #![feature(unsized_fn_params)] #![feature(with_negative_coherence)] +#![cfg_attr(kani, feature(proc_macro_hygiene))] // tidy-alphabetical-end // // Target features: @@ -247,7 +248,6 @@ #![feature(tbm_target_feature)] #![feature(wasm_target_feature)] #![feature(x86_amx_intrinsics)] -#![cfg_attr(kani, feature(proc_macro_hygiene))] // tidy-alphabetical-end // allow using `core::` in intra-doc links diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 765052e9cbaa6..f62413802ad83 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1770,7 +1770,7 @@ mod verify { macro_rules! generate_carrying_mul_intervals { ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => { $( - #[kani::proof] + //#[kani::proof] pub fn $harness_name() { let lhs: $type = kani::any::<$type>(); let rhs: $type = kani::any::<$type>(); @@ -1807,7 +1807,7 @@ mod verify { macro_rules! generate_widening_mul_intervals { ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => { $( - #[kani::proof] + //#[kani::proof] pub fn $harness_name() { let lhs: $type = kani::any::<$type>(); let rhs: $type = kani::any::<$type>(); diff --git a/library/core/src/ptr/unique.rs b/library/core/src/ptr/unique.rs index fd0dd6c46681f..dbe2f7f5b4f51 100644 --- a/library/core/src/ptr/unique.rs +++ b/library/core/src/ptr/unique.rs @@ -263,7 +263,7 @@ mod verify { } // pub const unsafe fn as_ref(&self) -> &T - #[kani::proof] + //#[kani::proof] pub fn check_as_ref() { let mut x : i32 = kani::any(); let xptr = &mut x; @@ -274,7 +274,7 @@ mod verify { } // pub const unsafe fn as_mut(&mut self) -> &mut T - #[kani::proof] + //#[kani::proof] pub fn check_as_mut() { let mut x : i32 = kani::any(); let xptr = &mut x; @@ -285,7 +285,7 @@ mod verify { } // pub const fn cast(self) -> Unique - #[kani::proof] + //#[kani::proof] pub fn check_cast() { let mut x : i32 = kani::any(); let xptr = &mut x; diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 4c119992f8e9e..a53d644978e47 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -1959,10 +1959,10 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { unsafe { let (mut px, mut py) = (x.as_ptr(), y.as_ptr()); let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4)); - #[cfg_attr(kani, kani::loop_invariant(same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py) + #[safety::loop_invariant(same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py) && px as isize >= x.as_ptr() as isize && py as isize >= y.as_ptr() as isize - && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize)))] + && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))] while px < pxend { let vx = (px as *const u32).read_unaligned(); let vy = (py as *const u32).read_unaligned(); @@ -1983,30 +1983,17 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { pub mod verify { use super::*; - // Copied from https://github.com/model-checking/kani/blob/main/library/kani/src/slice.rs - // should be removed when these functions are moved to `kani_core` - pub fn any_slice_of_array(arr: &[T; LENGTH]) -> &[T] { - let (from, to) = any_range::(); - &arr[from..to] - } - - fn any_range() -> (usize, usize) { - let from: usize = kani::any(); - let to: usize = kani::any(); - kani::assume(to <= LENGTH); - kani::assume(from <= to); - (from, to) - } - #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86 #[kani::proof] #[kani::unwind(4)] pub fn check_small_slice_eq() { + // ARR_SIZE can `std::usize::MAX` with cbmc argument + // `--arrays-uf-always` const ARR_SIZE: usize = 1000; let x: [u8; ARR_SIZE] = kani::any(); let y: [u8; ARR_SIZE] = kani::any(); - let xs = any_slice_of_array(&x); - let ys = any_slice_of_array(&y); + let xs = kani::slice::any_slice_of_array(&x); + let ys = kani::slice::any_slice_of_array(&y); kani::assume(xs.len() == ys.len()); unsafe { small_slice_eq(xs, ys); diff --git a/library/core/src/unicode/mod.rs b/library/core/src/unicode/mod.rs index 5ee17570bbc42..e49bf7910af9e 100644 --- a/library/core/src/unicode/mod.rs +++ b/library/core/src/unicode/mod.rs @@ -38,13 +38,13 @@ mod verify { use crate::kani; /// Checks that `to_upper` does not trigger UB or panics for all valid characters. - #[kani::proof] + //#[kani::proof] fn check_to_upper_safety() { let _ = to_upper(kani::any()); } /// Checks that `to_lower` does not trigger UB or panics for all valid characters. - #[kani::proof] + //#[kani::proof] fn check_to_lower_safety() { let _ = to_lower(kani::any()); } From 708fcbefe02b5c46943151c2b7dc232b74af256e Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 7 Nov 2024 20:59:57 -0600 Subject: [PATCH 3/8] Update Kani version --- library/core/src/alloc/layout.rs | 4 ++-- library/core/src/lib.rs | 2 +- library/core/src/num/mod.rs | 4 ++-- library/core/src/ptr/unique.rs | 6 +++--- library/core/src/str/pattern.rs | 7 ++++--- library/core/src/unicode/mod.rs | 4 ++-- tool_config/kani-version.toml | 2 +- 7 files changed, 15 insertions(+), 14 deletions(-) diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs index 83590c20dfa2a..808e2245045e0 100644 --- a/library/core/src/alloc/layout.rs +++ b/library/core/src/alloc/layout.rs @@ -655,7 +655,7 @@ mod verify { } // pub const fn size(&self) -> usize - //#[kani::proof] + #[kani::proof] pub fn check_size() { let s = kani::any::(); let a = kani::any::(); @@ -667,7 +667,7 @@ mod verify { } // pub const fn align(&self) -> usize - //#[kani::proof] + #[kani::proof] pub fn check_align() { let layout = kani::any::(); assert!(layout.align().is_power_of_two()); diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 8331248c8f883..7c0596768b784 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -230,7 +230,7 @@ #![feature(unboxed_closures)] #![feature(unsized_fn_params)] #![feature(with_negative_coherence)] -#![cfg_attr(kani, feature(proc_macro_hygiene))] +#![feature(proc_macro_hygiene)] // tidy-alphabetical-end // // Target features: diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index f62413802ad83..765052e9cbaa6 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1770,7 +1770,7 @@ mod verify { macro_rules! generate_carrying_mul_intervals { ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => { $( - //#[kani::proof] + #[kani::proof] pub fn $harness_name() { let lhs: $type = kani::any::<$type>(); let rhs: $type = kani::any::<$type>(); @@ -1807,7 +1807,7 @@ mod verify { macro_rules! generate_widening_mul_intervals { ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => { $( - //#[kani::proof] + #[kani::proof] pub fn $harness_name() { let lhs: $type = kani::any::<$type>(); let rhs: $type = kani::any::<$type>(); diff --git a/library/core/src/ptr/unique.rs b/library/core/src/ptr/unique.rs index dbe2f7f5b4f51..fd0dd6c46681f 100644 --- a/library/core/src/ptr/unique.rs +++ b/library/core/src/ptr/unique.rs @@ -263,7 +263,7 @@ mod verify { } // pub const unsafe fn as_ref(&self) -> &T - //#[kani::proof] + #[kani::proof] pub fn check_as_ref() { let mut x : i32 = kani::any(); let xptr = &mut x; @@ -274,7 +274,7 @@ mod verify { } // pub const unsafe fn as_mut(&mut self) -> &mut T - //#[kani::proof] + #[kani::proof] pub fn check_as_mut() { let mut x : i32 = kani::any(); let xptr = &mut x; @@ -285,7 +285,7 @@ mod verify { } // pub const fn cast(self) -> Unique - //#[kani::proof] + #[kani::proof] pub fn check_cast() { let mut x : i32 = kani::any(); let xptr = &mut x; diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index a53d644978e47..1a3d6c32a7ac6 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -43,7 +43,8 @@ use crate::convert::TryInto as _; use crate::slice::memchr; use crate::{cmp, fmt}; -use safety::{requires, ensures}; +#[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] // only called on x86 +use safety::{loop_invariant, requires}; #[cfg(kani)] use crate::kani; @@ -1959,7 +1960,7 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { unsafe { let (mut px, mut py) = (x.as_ptr(), y.as_ptr()); let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4)); - #[safety::loop_invariant(same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py) + #[loop_invariant(same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py) && px as isize >= x.as_ptr() as isize && py as isize >= y.as_ptr() as isize && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))] @@ -1987,7 +1988,7 @@ pub mod verify { #[kani::proof] #[kani::unwind(4)] pub fn check_small_slice_eq() { - // ARR_SIZE can `std::usize::MAX` with cbmc argument + // TODO: ARR_SIZE can be `std::usize::MAX` with cbmc argument // `--arrays-uf-always` const ARR_SIZE: usize = 1000; let x: [u8; ARR_SIZE] = kani::any(); diff --git a/library/core/src/unicode/mod.rs b/library/core/src/unicode/mod.rs index e49bf7910af9e..5ee17570bbc42 100644 --- a/library/core/src/unicode/mod.rs +++ b/library/core/src/unicode/mod.rs @@ -38,13 +38,13 @@ mod verify { use crate::kani; /// Checks that `to_upper` does not trigger UB or panics for all valid characters. - //#[kani::proof] + #[kani::proof] fn check_to_upper_safety() { let _ = to_upper(kani::any()); } /// Checks that `to_lower` does not trigger UB or panics for all valid characters. - //#[kani::proof] + #[kani::proof] fn check_to_lower_safety() { let _ = to_lower(kani::any()); } diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml index f75f2058e67f2..c28d156262481 100644 --- a/tool_config/kani-version.toml +++ b/tool_config/kani-version.toml @@ -2,4 +2,4 @@ # incompatible with the verify-std repo. [kani] -commit = "2565ef65767a696f1d519b42621b4e502e8970d0" +commit = "8400296f5280be4f99820129bc66447e8dff63f4" From 79d6af816c358f24aa371958298aa7bfbd53b275 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 7 Nov 2024 23:21:54 -0600 Subject: [PATCH 4/8] Increase object bits --- scripts/run-kani.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 310ee6a1adf2c..1c62a05969e34 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -183,7 +183,7 @@ main() { echo "Running Kani verify-std command..." - "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 8 + "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 12 } main From b4b4f89ea352162c16724440350335fc5d6225e7 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 00:42:13 -0600 Subject: [PATCH 5/8] Add harness for dangling pointer --- library/core/src/str/pattern.rs | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 1a3d6c32a7ac6..8c168400f7df0 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -43,13 +43,11 @@ use crate::convert::TryInto as _; use crate::slice::memchr; use crate::{cmp, fmt}; -#[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] // only called on x86 +#[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] use safety::{loop_invariant, requires}; #[cfg(kani)] use crate::kani; -#[cfg(kani)] -use crate::kani::mem::same_allocation; // Pattern @@ -1960,7 +1958,8 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { unsafe { let (mut px, mut py) = (x.as_ptr(), y.as_ptr()); let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4)); - #[loop_invariant(same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py) + #[loop_invariant(crate::ub_checks::same_allocation(x.as_ptr(), px) + && crate::ub_checks::same_allocation(y.as_ptr(), py) && px as isize >= x.as_ptr() as isize && py as isize >= y.as_ptr() as isize && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))] @@ -2000,4 +1999,23 @@ pub mod verify { small_slice_eq(xs, ys); } } + + #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86 + #[kani::proof] + #[kani::unwind(4)] + pub fn check_small_slice_eq_empty() { + let ptr_x = kani::any_where::(|val| *val != 0) as *const u8; + let ptr_y = kani::any_where::(|val| *val != 0) as *const u8; + kani::assume(ptr_x.is_aligned()); + kani::assume(ptr_y.is_aligned()); + unsafe { + assert_eq!( + small_slice_eq( + crate::slice::from_raw_parts(ptr_x, 0), + crate::slice::from_raw_parts(ptr_y, 0), + ), + true + ); + } + } } From 44196af562b093ba54dadef455a66da17a7ce14b Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 15:46:36 -0600 Subject: [PATCH 6/8] Update library/core/src/str/pattern.rs Co-authored-by: Celina G. Val --- library/core/src/str/pattern.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 8c168400f7df0..489cf3a09bb16 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -1960,8 +1960,8 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4)); #[loop_invariant(crate::ub_checks::same_allocation(x.as_ptr(), px) && crate::ub_checks::same_allocation(y.as_ptr(), py) - && px as isize >= x.as_ptr() as isize - && py as isize >= y.as_ptr() as isize + && px.addr() >= x.addr() + && py.addr() >= y.addr() && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))] while px < pxend { let vx = (px as *const u32).read_unaligned(); From 452ab444877662aee0472fb965c7ee6db7596b7a Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 15:46:43 -0600 Subject: [PATCH 7/8] Update library/core/src/str/pattern.rs Co-authored-by: Celina G. Val --- library/core/src/str/pattern.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 489cf3a09bb16..88ef249474811 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -1962,7 +1962,7 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { && crate::ub_checks::same_allocation(y.as_ptr(), py) && px.addr() >= x.addr() && py.addr() >= y.addr() - && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))] + && px.addr() - x.addr() == py.addr() - y.addr())] while px < pxend { let vx = (px as *const u32).read_unaligned(); let vy = (py as *const u32).read_unaligned(); From efdbc01f153869a14c4397c9b845948e4beeb138 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 16:16:51 -0600 Subject: [PATCH 8/8] Remove test for dangling pointer for now --- library/core/src/lib.rs | 1 + library/core/src/str/pattern.rs | 23 ++++++++++++++--------- 2 files changed, 15 insertions(+), 9 deletions(-) diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 7c0596768b784..2c813ca0cb412 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -230,6 +230,7 @@ #![feature(unboxed_closures)] #![feature(unsized_fn_params)] #![feature(with_negative_coherence)] +// Required for Kani loop contracts, which are annotated as custom stmt attributes. #![feature(proc_macro_hygiene)] // tidy-alphabetical-end // diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 88ef249474811..f0b767ae2d4e9 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -1960,9 +1960,9 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4)); #[loop_invariant(crate::ub_checks::same_allocation(x.as_ptr(), px) && crate::ub_checks::same_allocation(y.as_ptr(), py) - && px.addr() >= x.addr() - && py.addr() >= y.addr() - && px.addr() - x.addr() == py.addr() - y.addr())] + && px.addr() >= x.as_ptr().addr() + && py.addr() >= y.as_ptr().addr() + && px.addr() - x.as_ptr().addr() == py.addr() - y.as_ptr().addr())] while px < pxend { let vx = (px as *const u32).read_unaligned(); let vy = (py as *const u32).read_unaligned(); @@ -2000,6 +2000,10 @@ pub mod verify { } } + /* This harness check `small_slice_eq` with dangling pointer to slice + with zero size. Kani finds safety issue of `small_slice_eq` in this + harness and hence the proof will fail. + #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86 #[kani::proof] #[kani::unwind(4)] @@ -2008,14 +2012,15 @@ pub mod verify { let ptr_y = kani::any_where::(|val| *val != 0) as *const u8; kani::assume(ptr_x.is_aligned()); kani::assume(ptr_y.is_aligned()); - unsafe { - assert_eq!( + assert_eq!( + unsafe { small_slice_eq( crate::slice::from_raw_parts(ptr_x, 0), crate::slice::from_raw_parts(ptr_y, 0), - ), - true - ); - } + ) + }, + true + ); } + */ }