From 034b88343907eab303245644ed85db69de48f3e1 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Mon, 24 Mar 2025 15:54:05 -0700 Subject: [PATCH 1/6] add documentation for use of isize::MAX --- library/kani_core/src/mem.rs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 1ab8a5ead993..738d8661005f 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -129,7 +129,10 @@ macro_rules! kani_mem { /// Compute the size of the val pointed to if it is safe to do so. /// - /// Return `None` if an overflow would occur, or if alignment is not power of two. + /// Returns `None` if: + /// - An overflow occurs during the size computation. + /// - The pointer’s alignment is not a power of two. + /// - The computed size exceeds `isize::MAX` (the maximum safe Rust allocation size). /// TODO: Optimize this if T is sized. #[kanitool::fn_marker = "CheckedSizeOfIntrinsic"] pub fn checked_size_of_raw(ptr: *const T) -> Option { @@ -164,8 +167,15 @@ macro_rules! kani_mem { } /// Checks that `ptr` points to an allocation that can hold data of size calculated from `T`. - /// /// This will panic if `ptr` points to an invalid `non_null` + /// Returns `false` if: + /// - The computed size overflows. + /// - The computed size exceeds `isize::MAX`. + /// - The pointer is null (except for zero-sized types). + /// - The pointer references unallocated memory. + /// + /// This function aligns with Rust's memory safety requirements, which restrict valid allocations + /// to sizes no larger than `isize::MAX`. fn is_inbounds(ptr: *const T) -> bool { // If size overflows, then pointer cannot be inbounds. let Some(sz) = checked_size_of_raw(ptr) else { return false }; From f0751511c7ebd6d9188e06918259e28855dd80c3 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Mon, 24 Mar 2025 18:15:38 -0700 Subject: [PATCH 2/6] add quick test and fix doc spacing --- library/kani_core/src/mem.rs | 8 +++++++- .../MemPredicates/ptr_size_validity.expected | 1 + .../MemPredicates/ptr_size_validity.rs | 20 +++++++++++++++++++ 3 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 tests/expected/MemPredicates/ptr_size_validity.expected create mode 100644 tests/expected/MemPredicates/ptr_size_validity.rs diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 738d8661005f..cff445335a24 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -167,6 +167,7 @@ macro_rules! kani_mem { } /// Checks that `ptr` points to an allocation that can hold data of size calculated from `T`. + /// /// This will panic if `ptr` points to an invalid `non_null` /// Returns `false` if: /// - The computed size overflows. @@ -176,7 +177,12 @@ macro_rules! kani_mem { /// /// This function aligns with Rust's memory safety requirements, which restrict valid allocations /// to sizes no larger than `isize::MAX`. - fn is_inbounds(ptr: *const T) -> bool { + #[crate::kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" + )] + pub fn is_inbounds(ptr: *const T) -> bool { // If size overflows, then pointer cannot be inbounds. let Some(sz) = checked_size_of_raw(ptr) else { return false }; if sz == 0 { diff --git a/tests/expected/MemPredicates/ptr_size_validity.expected b/tests/expected/MemPredicates/ptr_size_validity.expected new file mode 100644 index 000000000000..aa71ac4c4795 --- /dev/null +++ b/tests/expected/MemPredicates/ptr_size_validity.expected @@ -0,0 +1 @@ +Complete - 1 successfully verified harnesses, 0 failures, 1 total. \ No newline at end of file diff --git a/tests/expected/MemPredicates/ptr_size_validity.rs b/tests/expected/MemPredicates/ptr_size_validity.rs new file mode 100644 index 000000000000..abf6a20d5b4a --- /dev/null +++ b/tests/expected/MemPredicates/ptr_size_validity.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z mem-predicates +#![feature(ptr_metadata)] + +extern crate kani; + +mod size { + use super::*; + + #[kani::proof] + fn verify_checked_size_of_raw_exceeds_isize_max() { + let len_exceeding_isize_max = (isize::MAX as usize) + 1; + let data_ptr: *const [u8] = core::ptr::from_raw_parts(core::ptr::null::(), len_exceeding_isize_max); + + let size = kani::mem::checked_size_of_raw(data_ptr); + + assert!(size.is_none()); + } +} \ No newline at end of file From c0ec0e48964bd45e799cce1aacfd1e78ae0f2874 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Mon, 24 Mar 2025 18:16:53 -0700 Subject: [PATCH 3/6] remove extra feature --- library/kani_core/src/mem.rs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index cff445335a24..6f2e6eb75c8d 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -177,11 +177,6 @@ macro_rules! kani_mem { /// /// This function aligns with Rust's memory safety requirements, which restrict valid allocations /// to sizes no larger than `isize::MAX`. - #[crate::kani::unstable_feature( - feature = "mem-predicates", - issue = 2690, - reason = "experimental memory predicate API" - )] pub fn is_inbounds(ptr: *const T) -> bool { // If size overflows, then pointer cannot be inbounds. let Some(sz) = checked_size_of_raw(ptr) else { return false }; From b22688ace20ee40cf26e864d690c1cf1d9d29144 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Mon, 24 Mar 2025 18:19:36 -0700 Subject: [PATCH 4/6] remove extra feature-1 --- library/kani_core/src/mem.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 6f2e6eb75c8d..903252bad636 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -177,7 +177,7 @@ macro_rules! kani_mem { /// /// This function aligns with Rust's memory safety requirements, which restrict valid allocations /// to sizes no larger than `isize::MAX`. - pub fn is_inbounds(ptr: *const T) -> bool { + fn is_inbounds(ptr: *const T) -> bool { // If size overflows, then pointer cannot be inbounds. let Some(sz) = checked_size_of_raw(ptr) else { return false }; if sz == 0 { From 81cd4038fb7c4673f99d6ff1497a7aaf4915bef4 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Mon, 24 Mar 2025 18:50:32 -0700 Subject: [PATCH 5/6] formatting --- library/kani_core/src/mem.rs | 2 +- tests/expected/MemPredicates/ptr_size_validity.rs | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 903252bad636..d431625a350b 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -167,7 +167,7 @@ macro_rules! kani_mem { } /// Checks that `ptr` points to an allocation that can hold data of size calculated from `T`. - /// + /// /// This will panic if `ptr` points to an invalid `non_null` /// Returns `false` if: /// - The computed size overflows. diff --git a/tests/expected/MemPredicates/ptr_size_validity.rs b/tests/expected/MemPredicates/ptr_size_validity.rs index abf6a20d5b4a..a8c9d6b0c2fd 100644 --- a/tests/expected/MemPredicates/ptr_size_validity.rs +++ b/tests/expected/MemPredicates/ptr_size_validity.rs @@ -5,13 +5,14 @@ extern crate kani; -mod size { +mod size { use super::*; #[kani::proof] fn verify_checked_size_of_raw_exceeds_isize_max() { let len_exceeding_isize_max = (isize::MAX as usize) + 1; - let data_ptr: *const [u8] = core::ptr::from_raw_parts(core::ptr::null::(), len_exceeding_isize_max); + let data_ptr: *const [u8] = + core::ptr::from_raw_parts(core::ptr::null::(), len_exceeding_isize_max); let size = kani::mem::checked_size_of_raw(data_ptr); From 25c63ab0c6c5bb1c1af2384c9f935ebc95155c76 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Tue, 25 Mar 2025 12:13:19 -0700 Subject: [PATCH 6/6] formatting checks --- tests/expected/MemPredicates/ptr_size_validity.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/expected/MemPredicates/ptr_size_validity.rs b/tests/expected/MemPredicates/ptr_size_validity.rs index a8c9d6b0c2fd..dabca4186b4f 100644 --- a/tests/expected/MemPredicates/ptr_size_validity.rs +++ b/tests/expected/MemPredicates/ptr_size_validity.rs @@ -5,17 +5,17 @@ extern crate kani; -mod size { +mod size { use super::*; #[kani::proof] fn verify_checked_size_of_raw_exceeds_isize_max() { let len_exceeding_isize_max = (isize::MAX as usize) + 1; - let data_ptr: *const [u8] = + let data_ptr: *const [u8] = core::ptr::from_raw_parts(core::ptr::null::(), len_exceeding_isize_max); let size = kani::mem::checked_size_of_raw(data_ptr); assert!(size.is_none()); } -} \ No newline at end of file +}