A few tests adjustments including a new fixme test

Author: celinval

tests/expected/offset-wraps-around/expected

@@ -1,2 +1,12 @@
-FAILURE\
-assertion failed: high_offset == wrapped_offset.try_into().unwrap()
+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.

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 <https://github.com/model-checking/kani/issues/1150> 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::<u128>() * 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::<u128>() * 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::<u128>();
-        // 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::<u128>();
+    // 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);
-}

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");
+}

tests/kani/Vectors/vector_extend_bytes.rs

@@ -1,10 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Check that we propertly handle `Vec::extend` with a constant byte slice.
+//! Check that we properly handle `Vec::extend` with a constant byte slice.
 //! This used to fail previously (see
 //! https://github.com/model-checking/kani/issues/2656).
 
+#[kani::unwind(4)]
 #[kani::proof]
 fn check_extend_const_byte_slice() {
     const MY_CONSTANT: &[u8] = b"Hi";