diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 01d237bf0773..85936041cc38 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/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")] diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index 79238e423e62..43f8e5b7013f 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/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); diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index 8913c399c959..39fd786f0249 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -89,8 +89,8 @@ macro_rules! generate_models { } } - #[kanitool::fn_marker = "PtrSubPtrModel"] - pub unsafe fn ptr_sub_ptr(ptr1: *const T, ptr2: *const T) -> usize { + #[kanitool::fn_marker = "PtrOffsetFromUnsignedModel"] + pub unsafe fn ptr_offset_from_unsigned(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 diff --git a/tests/expected/offset-bounds-check/sub_ptr.expected b/tests/expected/offset-bounds-check/offset_from_unsigned.expected similarity index 52% rename from tests/expected/offset-bounds-check/sub_ptr.expected rename to tests/expected/offset-bounds-check/offset_from_unsigned.expected index 611fe2e565c7..fff02a3d96af 100644 --- a/tests/expected/offset-bounds-check/sub_ptr.expected +++ b/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. diff --git a/tests/expected/offset-bounds-check/sub_ptr.rs b/tests/expected/offset-bounds-check/offset_from_unsigned.rs similarity index 62% rename from tests/expected/offset-bounds-check/sub_ptr.rs rename to tests/expected/offset-bounds-check/offset_from_unsigned.rs index 7ddfa96d94f8..f5b11a741403 100644 --- a/tests/expected/offset-bounds-check/sub_ptr.rs +++ b/tests/expected/offset-bounds-check/offset_from_unsigned.rs @@ -1,47 +1,47 @@ // 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); @@ -49,22 +49,22 @@ fn check_sub_ptr_negative_result() { #[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); } diff --git a/tests/kani/PointerOffset/offset_from_vec.rs b/tests/kani/PointerOffset/offset_from_vec.rs index 482b4905df3c..29865e2c8f81 100644 --- a/tests/kani/PointerOffset/offset_from_vec.rs +++ b/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); } }