Propagate changes from rust-lang/rust#137483

Rename `sub_ptr` to `offset_from_unsigned`.
The feature gate is still `ptr_sub_ptr`.

Author: Remi Delmas

kani-compiler/src/kani_middle/kani_functions.rs

@@ -87,8 +87,8 @@ pub enum KaniModel {
     Offset,
     #[strum(serialize = "PtrOffsetFromModel")]
     PtrOffsetFrom,
-    #[strum(serialize = "PtrSubPtrModel")]
-    PtrSubPtr,
+    #[strum(serialize = "PtrOffsetFromUnsignedModel")]
+    PtrOffsetFromUnsigned,
     #[strum(serialize = "RunContractModel")]
     RunContract,
     #[strum(serialize = "RunLoopContractModel")]

kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs

@@ -168,7 +168,9 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> {
                         Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal],
                         Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal],
                         Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom],
-                        Intrinsic::PtrOffsetFromUnsigned => self.models[&KaniModel::PtrSubPtr],
+                        Intrinsic::PtrOffsetFromUnsigned => {
+                            self.models[&KaniModel::PtrOffsetFromUnsigned]
+                        }
                         // The rest is handled in codegen.
                         _ => {
                             return self.super_terminator(term);

library/kani_core/src/models.rs

@@ -89,8 +89,8 @@ macro_rules! generate_models {
                 }
             }
 
-            #[kanitool::fn_marker = "PtrSubPtrModel"]
-            pub unsafe fn ptr_sub_ptr<T>(ptr1: *const T, ptr2: *const T) -> usize {
+            #[kanitool::fn_marker = "PtrOffsetFromUnsignedModel"]
+            pub unsafe fn ptr_offset_from_unsigned<T>(ptr1: *const T, ptr2: *const T) -> usize {
                 let offset = ptr_offset_from(ptr1, ptr2);
                 kani::safety_check(offset >= 0, "Expected non-negative distance between pointers");
                 offset as usize

tests/expected/offset-bounds-check/sub_ptr.expected renamed to tests/expected/offset-bounds-check/offset_from_unsigned.expected

@@ -1,29 +1,29 @@
-Checking harness check_sub_ptr_same_dangling...
+Checking harness check_offset_from_unsigned_same_dangling...
 VERIFICATION:- SUCCESSFUL
 
-Checking harness check_sub_ptr_unit_panic...
+Checking harness check_offset_from_unsigned_unit_panic...
 Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize
 VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
 
-Checking harness check_sub_ptr_negative_result...
+Checking harness check_offset_from_unsigned_negative_result...
 Failed Checks: Expected non-negative distance between pointers
 VERIFICATION:- FAILED
 
-Checking harness check_sub_ptr_diff_alloc...
+Checking harness check_offset_from_unsigned_diff_alloc...
 Failed Checks: Offset result and original pointer should point to the same allocation
 VERIFICATION:- FAILED
 
-Checking harness check_sub_ptr_oob_ptr...
+Checking harness check_offset_from_unsigned_oob_ptr...
 Failed Checks: Offset result and original pointer should point to the same allocation
 VERIFICATION:- FAILED
 
-Checking harness check_sub_ptr_self_oob...
+Checking harness check_offset_from_unsigned_self_oob...
 Failed Checks: Offset result and original pointer should point to the same allocation
 VERIFICATION:- FAILED
 
 Summary:
-Verification failed for - check_sub_ptr_negative_result
-Verification failed for - check_sub_ptr_diff_alloc
-Verification failed for - check_sub_ptr_oob_ptr
-Verification failed for - check_sub_ptr_self_oob
+Verification failed for - check_offset_from_unsigned_negative_result
+Verification failed for - check_offset_from_unsigned_diff_alloc
+Verification failed for - check_offset_from_unsigned_oob_ptr
+Verification failed for - check_offset_from_unsigned_self_oob
 Complete - 2 successfully verified harnesses, 4 failures, 6 total.

tests/expected/offset-bounds-check/sub_ptr.rs renamed to tests/expected/offset-bounds-check/offset_from_unsigned.rs

@@ -1,70 +1,70 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-//! Check that Kani can detect UB due to `sub_ptr` with out-of-bounds pointer or wrong order.
+//! Check that Kani can detect UB due to `offset_from_unsigned` with out-of-bounds pointer or wrong order.
 
 #![feature(ptr_sub_ptr)]
 
 #[kani::proof]
-fn check_sub_ptr_self_oob() {
+fn check_offset_from_unsigned_self_oob() {
     let val = 10u128;
     let ptr: *const u128 = &val;
     let ptr_oob: *const u128 = ptr.wrapping_add(10);
     // SAFETY: This is not safe!
-    let _offset = unsafe { ptr_oob.sub_ptr(ptr) };
+    let _offset = unsafe { ptr_oob.offset_from_unsigned(ptr) };
 }
 
 #[kani::proof]
-fn check_sub_ptr_oob_ptr() {
+fn check_offset_from_unsigned_oob_ptr() {
     let val = 10u128;
     let ptr: *const u128 = &val;
     let ptr_oob: *const u128 = ptr.wrapping_sub(10);
     // SAFETY: This is not safe!
-    let _offset = unsafe { ptr.sub_ptr(ptr_oob) };
+    let _offset = unsafe { ptr.offset_from_unsigned(ptr_oob) };
 }
 
 #[kani::proof]
-fn check_sub_ptr_diff_alloc() {
+fn check_offset_from_unsigned_diff_alloc() {
     let val1 = kani::any();
     let val2 = kani::any();
     let ptr1: *const u128 = &val1;
     let ptr2: *const u128 = &val2;
     // SAFETY: This is not safe!
-    let _offset = unsafe { ptr1.sub_ptr(ptr2) };
+    let _offset = unsafe { ptr1.offset_from_unsigned(ptr2) };
 }
 
 #[kani::proof]
-fn check_sub_ptr_negative_result() {
+fn check_offset_from_unsigned_negative_result() {
     let val: [u8; 10] = kani::any();
     let ptr_first: *const _ = &val[0];
     let ptr_last: *const _ = &val[9];
     // SAFETY: This is safe!
-    let offset_ok = unsafe { ptr_last.sub_ptr(ptr_first) };
+    let offset_ok = unsafe { ptr_last.offset_from_unsigned(ptr_first) };
 
     // SAFETY: This is not safe!
-    let offset_not_ok = unsafe { ptr_first.sub_ptr(ptr_last) };
+    let offset_not_ok = unsafe { ptr_first.offset_from_unsigned(ptr_last) };
 
     // Just use the result.
     assert!(offset_ok != offset_not_ok);
 }
 
 #[kani::proof]
 #[kani::should_panic]
-fn check_sub_ptr_unit_panic() {
+fn check_offset_from_unsigned_unit_panic() {
     let val1 = kani::any();
     let val2 = kani::any();
     let ptr1: *const () = &val1 as *const _ as *const ();
     let ptr2: *const () = &val2 as *const _ as *const ();
     // SAFETY: This is safe but will panic...
-    let _offset = unsafe { ptr1.sub_ptr(ptr2) };
+    let _offset = unsafe { ptr1.offset_from_unsigned(ptr2) };
 }
 
 #[kani::proof]
-fn check_sub_ptr_same_dangling() {
+fn check_offset_from_unsigned_same_dangling() {
     let val = 10u128;
     let ptr: *const u128 = &val;
     let ptr_oob_1: *const u128 = ptr.wrapping_add(10);
     let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5);
     // SAFETY: This is safe since the pointer is the same!
-    let offset = unsafe { ptr_oob_1.sub_ptr(ptr_oob_2) };
+    let offset = unsafe { ptr_oob_1.offset_from_unsigned(ptr_oob_2) };
     assert_eq!(offset, 0);
 }

tests/kani/PointerOffset/offset_from_vec.rs

@@ -18,6 +18,6 @@ fn offset_non_power_two() {
         let offset = kani::any_where(|o: &usize| *o <= v.len());
         let begin = v.as_mut_ptr();
         let end = begin.add(offset);
-        assert_eq!(end.sub_ptr(begin), offset);
+        assert_eq!(end.offset_from_unsigned(begin), offset);
     }
 }