ptr_offset_from: Replace arithmetic over pointers by offset arithmetic (#4180)

Makes `pointer_offset` crate-available just like `pointer_object` is.
This enables its use in `ptr_offset_from`, whereby we create expressions
that CBMC's simplifier can more readily deal with.

Resolves: #2235

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

library/kani_core/src/mem.rs

@@ -287,14 +287,9 @@ macro_rules! kani_mem {
 
         /// Get the object offset of the given pointer.
         #[doc(hidden)]
-        #[crate::kani::unstable_feature(
-            feature = "ghost-state",
-            issue = 3184,
-            reason = "experimental ghost state/shadow memory API"
-        )]
         #[kanitool::fn_marker = "PointerOffsetHook"]
         #[inline(never)]
-        pub fn pointer_offset<T: PointeeSized>(_ptr: *const T) -> usize {
+        pub(crate) fn pointer_offset<T: PointeeSized>(_ptr: *const T) -> usize {
             kani_intrinsic()
         }
     };

library/kani_core/src/models.rs

@@ -85,7 +85,9 @@ macro_rules! generate_models {
                         "Offset result and original pointer should point to the same allocation",
                     );
                     // The offset must fit in isize since this represents the same allocation.
-                    let offset_bytes = ptr1.addr().wrapping_sub(ptr2.addr()) as isize;
+                    let offset_bytes = kani::mem::pointer_offset(ptr1)
+                        .wrapping_sub(kani::mem::pointer_offset(ptr2))
+                        as isize;
                     let t_size = size_of::<T>() as isize;
                     kani::safety_check(
                         offset_bytes % t_size == 0,

tests/expected/shadow/unsupported_object_size/test.rs

@@ -5,12 +5,17 @@
 // This test checks the maximum object size supported by Kani's shadow
 // memory model (currently 64)
 
+#![feature(core_intrinsics)]
+use std::intrinsics::ptr_offset_from_unsigned;
+
 static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
 
 fn check_max_objects<const N: usize>() {
     let arr: [u8; N] = [0; N];
     let last = &arr[N - 1];
-    assert_eq!(kani::mem::pointer_offset(last as *const u8), N - 1);
+    unsafe {
+        assert_eq!(ptr_offset_from_unsigned(last as *const u8, &arr[0] as *const u8), N - 1);
+    }
     // the following call to `set_init` would fail if the object offset for
     // `last` exceeds the maximum allowed by Kani's shadow memory model
     unsafe {

tests/expected/string-repeat/2235.expected

@@ -0,0 +1,3 @@
+Failed Checks: called `Option::unwrap()` on a `None` value
+Verification failed for - repeat_panic
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.

tests/expected/string-repeat/2235.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn repeat_const() {
+    let s = String::from("a").repeat(1);
+    assert_eq!(s.chars().nth(0).unwrap(), 'a');
+}
+
+#[kani::proof]
+fn repeat_panic() {
+    let x = String::new().repeat(1);
+    let z = x.chars().nth(1).unwrap();
+}