diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index f95e1acc4899..8913c399c959 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -99,29 +99,35 @@ macro_rules! generate_models { /// An offset model that checks UB. #[kanitool::fn_marker = "OffsetModel"] pub fn offset, O: ToISize>(ptr: P, offset: O) -> P { - let offset = offset.to_isize(); let t_size = core::mem::size_of::() as isize; - if offset == 0 || t_size == 0 { + if t_size == 0 { + // It's always safe to perform an offset on a ZST. + return ptr; + } + + // Note that this check must come after the t_size check, c.f. https://github.com/model-checking/kani/issues/3896 + let offset = offset.to_isize(); + if offset == 0 { // It's always safe to perform an offset of length 0. - ptr - } else { - let (byte_offset, overflow) = offset.overflowing_mul(t_size); - kani::safety_check(!overflow, "Offset in bytes overflows isize"); - let orig_ptr = ptr.to_const_ptr(); - // NOTE: For CBMC, using the pointer addition can have unexpected behavior - // when the offset is higher than the object bits since it will wrap around. - // See for more details: https://github.com/model-checking/kani/issues/1150 - // - // However, when I tried implementing this using usize operation, we got some - // unexpected failures that still require further debugging. - // let new_ptr = orig_ptr.addr().wrapping_add_signed(byte_offset) as *const T; - let new_ptr = orig_ptr.wrapping_byte_offset(byte_offset); - kani::safety_check( - kani::mem::same_allocation_internal(orig_ptr, new_ptr), - "Offset result and original pointer must point to the same allocation", - ); - P::from_const_ptr(new_ptr) + return ptr; } + + let (byte_offset, overflow) = offset.overflowing_mul(t_size); + kani::safety_check(!overflow, "Offset in bytes overflows isize"); + let orig_ptr = ptr.to_const_ptr(); + // NOTE: For CBMC, using the pointer addition can have unexpected behavior + // when the offset is higher than the object bits since it will wrap around. + // See for more details: https://github.com/model-checking/kani/issues/1150 + // + // However, when I tried implementing this using usize operation, we got some + // unexpected failures that still require further debugging. + // let new_ptr = orig_ptr.addr().wrapping_add_signed(byte_offset) as *const T; + let new_ptr = orig_ptr.wrapping_byte_offset(byte_offset); + kani::safety_check( + kani::mem::same_allocation_internal(orig_ptr, new_ptr), + "Offset result and original pointer must point to the same allocation", + ); + P::from_const_ptr(new_ptr) } pub trait Ptr { diff --git a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected index d8c6e135adc9..e0cb28198a18 100644 --- a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected +++ b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected @@ -1,4 +1,6 @@ Failed Checks: Offset result and original pointer must point to the same allocation -Verification failed for - check_ptr_oob +Failed Checks: Offset result and original pointer must point to the same allocation -Complete - 1 successfully verified harnesses, 1 failures, 2 total. +Verification failed for - test_offset_overflow +Verification failed for - check_ptr_oob +Complete - 1 successfully verified harnesses, 2 failures, 3 total. diff --git a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs index e6b4310269a1..fd08e7a76876 100644 --- a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs +++ b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs @@ -2,6 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Check that Kani offset operations correctly detect out-of-bound access. +#![feature(core_intrinsics)] +use std::intrinsics::offset; + /// Verification should fail because safety violation is not a regular panic. #[kani::proof] #[kani::should_panic] @@ -24,3 +27,15 @@ fn check_ptr_end() { // Safety: Pointers point to the same allocation assert_eq!(unsafe { end_ptr.offset_from(base_ptr) }, 1); } + +#[kani::proof] +fn test_offset_overflow() { + let s: &str = "123"; + let ptr: *const u8 = s.as_ptr(); + + unsafe { + // This should fail because adding `isize::MAX` to `ptr` would overflow + // `isize` + let _d = offset(ptr, isize::MAX); + } +} diff --git a/tests/expected/offset-overflow/expected b/tests/expected/offset-overflow/expected deleted file mode 100644 index af5ea73875ca..000000000000 --- a/tests/expected/offset-overflow/expected +++ /dev/null @@ -1,4 +0,0 @@ -Failed Checks: Offset result and original pointer must point to the same allocation -Verification failed for - test_offset_overflow - -Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/offset-overflow/main.rs b/tests/expected/offset-overflow/main.rs deleted file mode 100644 index fc9f36b9cc5d..000000000000 --- a/tests/expected/offset-overflow/main.rs +++ /dev/null @@ -1,19 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Checks that `offset` fails if the offset computation would -// result in an arithmetic overflow -#![feature(core_intrinsics)] -use std::intrinsics::offset; - -#[kani::proof] -fn test_offset_overflow() { - let s: &str = "123"; - let ptr: *const u8 = s.as_ptr(); - - unsafe { - // This should fail because adding `isize::MAX` to `ptr` would overflow - // `isize` - let _d = offset(ptr, isize::MAX); - } -} diff --git a/tests/expected/offset-overflows-isize/expected b/tests/expected/offset-overflows-isize/expected new file mode 100644 index 000000000000..f554e2b1804b --- /dev/null +++ b/tests/expected/offset-overflows-isize/expected @@ -0,0 +1,8 @@ +::to_isize.safety_check\ + - Status: FAILURE\ + - Description: "Offset value overflows isize" + +Failed Checks: Offset value overflows isize + +Verification failed for - test_non_zst +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/offset-overflows-isize/main.rs b/tests/expected/offset-overflows-isize/main.rs new file mode 100644 index 000000000000..06400c1163d7 --- /dev/null +++ b/tests/expected/offset-overflows-isize/main.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `offset` does not accept a `count` greater than isize::MAX, +// except for ZSTs, c.f. https://github.com/model-checking/kani/issues/3896 + +#[kani::proof] +fn test_zst() { + let mut x = (); + let ptr: *mut () = &mut x as *mut (); + let count: usize = (isize::MAX as usize) + 1; + let _ = unsafe { ptr.add(count) }; +} + +#[kani::proof] +fn test_non_zst() { + let mut x = 7; + let ptr: *mut i32 = &mut x as *mut i32; + let count: usize = (isize::MAX as usize) + 1; + let _ = unsafe { ptr.add(count) }; +}