From f717f66b5e1766e59a195315a21ff2099450a5a8 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 6 Dec 2024 18:15:15 -0800 Subject: [PATCH] A few tests adjustments including a new fixme test --- tests/expected/offset-wraps-around/expected | 14 +++++- tests/expected/offset-wraps-around/main.rs | 44 +++++++------------ .../fixme_wrap_nonzero_offset.rs | 18 ++++++++ 3 files changed, 47 insertions(+), 29 deletions(-) create mode 100644 tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs diff --git a/tests/expected/offset-wraps-around/expected b/tests/expected/offset-wraps-around/expected index cacc000d09e5..2fedc9da1a89 100644 --- a/tests/expected/offset-wraps-around/expected +++ b/tests/expected/offset-wraps-around/expected @@ -1,2 +1,12 @@ -FAILURE\ -assertion failed: high_offset == wrapped_offset.try_into().unwrap() \ No newline at end of file +Checking harness check_wrap_around_ptr... +VERIFICATION:- SUCCESSFUL + +Checking harness harness_without_ub... +VERIFICATION:- SUCCESSFUL + +Checking harness original_harness... +Failed Checks: assertion failed: high_offset == wrapped_offset.try_into().unwrap() +VERIFICATION:- FAILED + +Verification failed for - original_harness +Complete - 2 successfully verified harnesses, 1 failures, 3 total. \ No newline at end of file diff --git a/tests/expected/offset-wraps-around/main.rs b/tests/expected/offset-wraps-around/main.rs index bcca66dea438..205ba56cb3e1 100644 --- a/tests/expected/offset-wraps-around/main.rs +++ b/tests/expected/offset-wraps-around/main.rs @@ -5,8 +5,8 @@ //! the add operation wraps. //! //! Note that CBMC offset logic will wrap around the object bits, not the entire address space, when -//! computing the offset between pointers. Doing that is UB in Rust, so we should be OK -//! as long as Kani can detect UB in that case. +//! computing the offset between pointers. +//! See for more details. use std::convert::TryInto; @@ -15,15 +15,14 @@ fn original_harness() { let v: &[u128] = &[0; 10]; let v_0: *const u128 = &v[0]; let high_offset = usize::MAX / (std::mem::size_of::() * 4); - unsafe { - let v_wrap: *const u128 = v_0.wrapping_add(high_offset); - // This should trigger UB!! - let wrapped_offset = unsafe { v_wrap.offset_from(v_0) }; - // Without UB detection, the offsets are the same, but CBMC pointer arithmetic - // would "wrap around" making this incorrect - // https://github.com/model-checking/kani/issues/1150 - assert!(high_offset == wrapped_offset.try_into().unwrap()); - } + let v_wrap: *const u128 = v_0.wrapping_add(high_offset); + // FIX-ME: This should trigger UB!! + // https://github.com/model-checking/kani/issues/3756 + let wrapped_offset = unsafe { v_wrap.offset_from(v_0) }; + // Without UB detection, the offsets are the same, but CBMC pointer arithmetic + // would "wrap around" making this incorrect + // https://github.com/model-checking/kani/issues/1150 + assert!(high_offset == wrapped_offset.try_into().unwrap()); } /// This harness is similar to the `original_harness`, but we replace the `offset_from` with @@ -33,27 +32,18 @@ fn harness_without_ub() { let v: &[u128] = &[0; 10]; let v_0: *const u128 = &v[0]; let high_offset = usize::MAX / (size_of::() * 4); - unsafe { - let v_wrap: *const u128 = v_0.wrapping_add(high_offset); - // The only way to compute offset of pointers out of bounds is to convert them to integers. - let wrapped_offset = (v_wrap.addr() - v_0.addr()) / size_of::(); - // Now this should work - assert_eq!(high_offset, wrapped_offset); - } + let v_wrap: *const u128 = v_0.wrapping_add(high_offset); + // The only way to compute offset of pointers out of bounds is to convert them to integers. + let wrapped_offset = (v_wrap.addr() - v_0.addr()) / size_of::(); + // Now this should work + assert_eq!(high_offset, wrapped_offset); } +/// Check that wrapping offset by `usize::MAX + 1` bytes will result in the same base pointer. #[kani::proof] -fn check_wrap_ptr_max() { +fn check_wrap_around_ptr() { let v: &[u128] = &[0; 10]; let orig_ptr: *const u128 = &v[0]; let new_ptr: *const u128 = orig_ptr.wrapping_byte_add(usize::MAX).wrapping_byte_add(1); assert_eq!(orig_ptr as usize, new_ptr as usize); } - -#[kani::proof] -fn check_wrap_ptr_10_bits() { - let v: &[u128] = &[0; 10]; - let orig_ptr: *const u128 = &v[0]; - let new_ptr: *const u128 = orig_ptr.wrapping_byte_add(1 << 63); - assert_ne!(orig_ptr as usize, new_ptr as usize); -} diff --git a/tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs b/tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs new file mode 100644 index 000000000000..fdc0496ff648 --- /dev/null +++ b/tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Testcase for issue [#1150](https://github.com/model-checking/kani/issues/1150) that shows +//! bug with wrapping offset operations in Kani. + +/// This harness shows the issue with the current implementation of wrapping offset. +/// +/// Invoking `wrapping_byte_offset` should return a pointer that is different from the original +/// pointer if the offset value is not 0. +/// See issue [#1150](https://github.com/model-checking/kani/issues/1150). +#[kani::proof] +fn fixme_incorrect_wrapping_offset() { + let ptr: *const u8 = &0u8; + let offset = kani::any_where(|v: &isize| *v != 0); + let new_ptr = ptr.wrapping_byte_offset(offset); + assert_ne!(ptr, new_ptr, "Expected new_ptr to be different than ptr"); +}