diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 654a7f2b6861..bd103fe4e45e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -7,9 +7,7 @@ use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; use crate::codegen_cprover_gotoc::{GotocCtx, utils}; use crate::intrinsics::Intrinsic; use crate::unwrap_or_return_codegen_unimplemented_stmt; -use cbmc::goto_program::{ - ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type, -}; +use cbmc::goto_program::{BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type}; use rustc_middle::ty::TypingEnv; use rustc_middle::ty::layout::ValidityRequirement; use rustc_smir::rustc_internal; @@ -425,10 +423,6 @@ impl GotocCtx<'_> { Intrinsic::PowIF64 => codegen_simple_intrinsic!(Powi), Intrinsic::PrefAlignOf => codegen_intrinsic_const!(), Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), - Intrinsic::PtrOffsetFrom => self.codegen_ptr_offset_from(fargs, place, loc), - Intrinsic::PtrOffsetFromUnsigned => { - self.codegen_ptr_offset_from_unsigned(fargs, place, loc) - } Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc), Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf), @@ -546,7 +540,10 @@ impl GotocCtx<'_> { assert!(self.place_ty_stable(place).kind().is_unit()); self.codegen_write_bytes(fargs, farg_types, loc) } - Intrinsic::SizeOfVal | Intrinsic::MinAlignOfVal => { + Intrinsic::PtrOffsetFrom + | Intrinsic::PtrOffsetFromUnsigned + | Intrinsic::SizeOfVal + | Intrinsic::MinAlignOfVal => { unreachable!("Intrinsic `{}` is handled before codegen", intrinsic_str) } // Unimplemented @@ -1025,77 +1022,6 @@ impl GotocCtx<'_> { self.codegen_expr_to_place_stable(p, dst_ptr, loc) } - /// ptr_offset_from returns the offset between two pointers - /// - fn codegen_ptr_offset_from(&mut self, fargs: Vec, p: &Place, loc: Location) -> Stmt { - let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs); - - // Check that computing `offset` in bytes would not overflow an `isize` - // These checks may allow a wrapping-around behavior in CBMC: - // https://github.com/model-checking/kani/issues/1150 - let overflow_check = self.codegen_assert_assume( - offset_overflow.overflowed.not(), - PropertyClass::ArithmeticOverflow, - "attempt to compute offset in bytes which would overflow an `isize`", - loc, - ); - - let offset_expr = self.codegen_expr_to_place_stable(p, offset_expr, loc); - Stmt::block(vec![overflow_check, offset_expr], loc) - } - - /// `ptr_offset_from_unsigned` returns the offset between two pointers where the order is known. - /// The logic is similar to `ptr_offset_from` but the return value is a `usize`. - /// See for more details - fn codegen_ptr_offset_from_unsigned( - &mut self, - fargs: Vec, - p: &Place, - loc: Location, - ) -> Stmt { - let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs); - - // Check that computing `offset` in bytes would not overflow an `isize` - // These checks may allow a wrapping-around behavior in CBMC: - // https://github.com/model-checking/kani/issues/1150 - let overflow_check = self.codegen_assert_assume( - offset_overflow.overflowed.not(), - PropertyClass::ArithmeticOverflow, - "attempt to compute offset in bytes which would overflow an `isize`", - loc, - ); - - let non_negative_check = self.codegen_assert_assume( - offset_overflow.result.is_non_negative(), - PropertyClass::SafetyCheck, - "attempt to compute unsigned offset with negative distance", - loc, - ); - - let offset_expr = - self.codegen_expr_to_place_stable(p, offset_expr.cast_to(Type::size_t()), loc); - Stmt::block(vec![overflow_check, non_negative_check, offset_expr], loc) - } - - /// Both `ptr_offset_from` and `ptr_offset_from_unsigned` return the offset between two pointers. - /// This function implements the common logic between them. - fn codegen_ptr_offset_from_expr( - &mut self, - mut fargs: Vec, - ) -> (Expr, ArithmeticOverflowResult) { - let dst_ptr = fargs.remove(0); - let src_ptr = fargs.remove(0); - - // Compute the offset with standard substraction using `isize` - let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t()); - let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t()); - let offset_overflow = cast_dst_ptr.sub_overflow(cast_src_ptr); - - // Re-compute the offset with standard substraction (no casts this time) - let ptr_offset_expr = dst_ptr.sub(src_ptr); - (ptr_offset_expr, offset_overflow) - } - /// A transmute is a bitcast from the argument type to the return type. /// /// diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 38522fae837f..8d1ab5ef939d 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -83,6 +83,10 @@ pub enum KaniModel { IsSlicePtrInitialized, #[strum(serialize = "OffsetModel")] Offset, + #[strum(serialize = "PtrOffsetFromModel")] + PtrOffsetFrom, + #[strum(serialize = "PtrSubPtrModel")] + PtrSubPtr, #[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 ad4238574d63..79238e423e62 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -167,6 +167,8 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> { let model = match intrinsic { Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal], Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal], + Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom], + Intrinsic::PtrOffsetFromUnsigned => self.models[&KaniModel::PtrSubPtr], // The rest is handled in codegen. _ => { return self.super_terminator(term); diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 5c10d08badb6..78ee9dd8ea02 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -61,7 +61,6 @@ static CBMC_ALT_DESCRIPTIONS: Lazy = Lazy::new(|| { ("NaN on /", Some("NaN on division")), ("NaN on *", Some("NaN on multiplication")), ]); - map.insert("pointer", vec![("same object violation", None)]); map.insert("pointer_arithmetic", vec![ ("pointer relation: deallocated dynamic object", None), ("pointer relation: dead object", None), diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index 121be62fd499..f95e1acc4899 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -45,6 +45,57 @@ macro_rules! generate_models { } } + /// Implements core::intrinsics::ptr_offset_from with safety checks in place. + /// + /// From original documentation: + /// + /// # Safety + /// + /// If any of the following conditions are violated, the result is Undefined Behavior: + /// + /// * `self` and `origin` must either + /// + /// * point to the same address, or + /// * both be *derived from* a pointer to the same allocated object, + /// and the memory range between + /// the two pointers must be in bounds of that object. + /// + /// * The distance between the pointers, in bytes, must be an exact multiple + /// of the size of `T`. + /// + /// # Panics + /// + /// This function panics if `T` is a Zero-Sized Type ("ZST"). + #[kanitool::fn_marker = "PtrOffsetFromModel"] + pub unsafe fn ptr_offset_from(ptr1: *const T, ptr2: *const T) -> isize { + // This is not a safety condition. + kani::assert(core::mem::size_of::() > 0, "Cannot compute offset of a ZST"); + if ptr1 == ptr2 { + 0 + } else { + kani::safety_check( + kani::mem::same_allocation_internal(ptr1, ptr2), + "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 t_size = size_of::() as isize; + kani::safety_check( + offset_bytes % t_size == 0, + "Expected the distance between the pointers, in bytes, to be a + multiple of the size of `T`", + ); + offset_bytes / t_size + } + } + + #[kanitool::fn_marker = "PtrSubPtrModel"] + pub unsafe fn ptr_sub_ptr(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 + } + /// An offset model that checks UB. #[kanitool::fn_marker = "OffsetModel"] pub fn offset, O: ToISize>(ptr: P, offset: O) -> P { diff --git a/tests/expected/arbitrary/ptrs/pointer_inbounds.rs b/tests/expected/arbitrary/ptrs/pointer_inbounds.rs index 36e4abeff48b..aac5a57d30e5 100644 --- a/tests/expected/arbitrary/ptrs/pointer_inbounds.rs +++ b/tests/expected/arbitrary/ptrs/pointer_inbounds.rs @@ -9,8 +9,6 @@ //! Kani will detect the usage of MaybeUninit and fail the verification. extern crate kani; -use kani::PointerGenerator; - #[kani::proof] fn check_inbounds() { let mut generator = kani::pointer_generator::(); @@ -48,9 +46,9 @@ fn check_overlap() { kani::cover!(ptr_1 == ptr_2, "Same"); kani::cover!(ptr_1 == unsafe { ptr_2.byte_add(1) }, "Overlap"); - let distance = unsafe { ptr_1.offset_from(ptr_2) }; + let distance = unsafe { ptr_1.byte_offset_from(ptr_2) }; kani::cover!(distance > 0, "Greater"); kani::cover!(distance < 0, "Smaller"); - assert!(distance >= -4 && distance <= 4, "Expected a maximum distance of 4 elements"); + assert!(distance >= -8 && distance <= 8, "Expected a maximum distance of 8 bytes"); } diff --git a/tests/expected/intrinsics/offset-same-object/expected b/tests/expected/intrinsics/offset-same-object/expected index bfb930e2bf03..0d267dddfaae 100644 --- a/tests/expected/intrinsics/offset-same-object/expected +++ b/tests/expected/intrinsics/offset-same-object/expected @@ -1,2 +1 @@ -FAILURE\ -"same object violation" \ No newline at end of file +Failed Checks: Offset result and original pointer should point to the same allocation diff --git a/tests/expected/intrinsics/ptr_offset_from_unsigned/expected b/tests/expected/intrinsics/ptr_offset_from_unsigned/expected index 8a893dea24be..9daa67d4f541 100644 --- a/tests/expected/intrinsics/ptr_offset_from_unsigned/expected +++ b/tests/expected/intrinsics/ptr_offset_from_unsigned/expected @@ -1 +1 @@ -Failed Checks: attempt to compute unsigned offset with negative distance +Failed Checks: Expected non-negative distance between pointers diff --git a/tests/expected/offset-bounds-check/offset_from.expected b/tests/expected/offset-bounds-check/offset_from.expected new file mode 100644 index 000000000000..66ebdd24aed1 --- /dev/null +++ b/tests/expected/offset-bounds-check/offset_from.expected @@ -0,0 +1,18 @@ +Checking harness check_offset_from_same_dangling... +VERIFICATION:- SUCCESSFUL + +Checking harness check_offset_from_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_offset_from_diff_alloc... +Failed Checks: Offset result and original pointer should point to the same allocation +VERIFICATION:- FAILED + +Checking harness check_offset_from_oob_ptr... +Failed Checks: Offset result and original pointer should point to the same allocation +VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected) + +Verification failed for - check_offset_from_diff_alloc +Verification failed for - check_offset_from_oob_ptr +Complete - 2 successfully verified harnesses, 2 failures, 4 total. diff --git a/tests/expected/offset-bounds-check/offset_from.rs b/tests/expected/offset-bounds-check/offset_from.rs new file mode 100644 index 000000000000..7ce3edcb3657 --- /dev/null +++ b/tests/expected/offset-bounds-check/offset_from.rs @@ -0,0 +1,47 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani offset operations correctly detect out-of-bound access. + +/// Verification should fail because safety violation is not a regular panic. +#[kani::proof] +#[kani::should_panic] +fn check_offset_from_oob_ptr() { + 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.offset_from(ptr) }; +} + +#[kani::proof] +fn check_offset_from_diff_alloc() { + let val1 = 10u128; + let val2 = 0u128; + let ptr1: *const u128 = &val1; + let ptr2: *const u128 = &val2; + // SAFETY: This is not safe! + let offset = unsafe { ptr1.offset_from(ptr2) }; + assert!(offset != 0); +} + +#[kani::proof] +#[kani::should_panic] +fn check_offset_from_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.offset_from(ptr2) }; +} + +#[kani::proof] +fn check_offset_from_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.offset_from(ptr_oob_2) }; + assert_eq!(offset, 0); +} diff --git a/tests/expected/offset-bounds-check/sub_ptr.expected b/tests/expected/offset-bounds-check/sub_ptr.expected new file mode 100644 index 000000000000..611fe2e565c7 --- /dev/null +++ b/tests/expected/offset-bounds-check/sub_ptr.expected @@ -0,0 +1,29 @@ +Checking harness check_sub_ptr_same_dangling... +VERIFICATION:- SUCCESSFUL + +Checking harness check_sub_ptr_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... +Failed Checks: Expected non-negative distance between pointers +VERIFICATION:- FAILED + +Checking harness check_sub_ptr_diff_alloc... +Failed Checks: Offset result and original pointer should point to the same allocation +VERIFICATION:- FAILED + +Checking harness check_sub_ptr_oob_ptr... +Failed Checks: Offset result and original pointer should point to the same allocation +VERIFICATION:- FAILED + +Checking harness check_sub_ptr_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 +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/sub_ptr.rs new file mode 100644 index 000000000000..7ddfa96d94f8 --- /dev/null +++ b/tests/expected/offset-bounds-check/sub_ptr.rs @@ -0,0 +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. + +#![feature(ptr_sub_ptr)] + +#[kani::proof] +fn check_sub_ptr_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) }; +} + +#[kani::proof] +fn check_sub_ptr_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) }; +} + +#[kani::proof] +fn check_sub_ptr_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) }; +} + +#[kani::proof] +fn check_sub_ptr_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) }; + + // SAFETY: This is not safe! + let offset_not_ok = unsafe { ptr_first.sub_ptr(ptr_last) }; + + // Just use the result. + assert!(offset_ok != offset_not_ok); +} + +#[kani::proof] +#[kani::should_panic] +fn check_sub_ptr_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) }; +} + +#[kani::proof] +fn check_sub_ptr_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) }; + assert_eq!(offset, 0); +} diff --git a/tests/expected/offset-from-distance-check/expected b/tests/expected/offset-from-distance-check/expected new file mode 100644 index 000000000000..d88ef6daeceb --- /dev/null +++ b/tests/expected/offset-from-distance-check/expected @@ -0,0 +1,3 @@ +Failed Checks: Expected the distance between the pointers, in bytes, to be a + multiple of the size of `T` +VERIFICATION:- FAILED \ No newline at end of file diff --git a/tests/expected/offset-from-distance-check/main.rs b/tests/expected/offset-from-distance-check/main.rs new file mode 100644 index 000000000000..2c7471fb4fe8 --- /dev/null +++ b/tests/expected/offset-from-distance-check/main.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z mem-predicates +//! Check that Kani detects UB for offset_from when the distance between the pointers is not a multiple of size_of:: +extern crate kani; + +#[kani::proof] +fn check_offset_from_distance_ub() { + let mut generator = kani::pointer_generator::(); + let ptr_1 = generator.any_in_bounds::().ptr; + let ptr_2 = generator.any_in_bounds::().ptr; + + // offset_from is only safe if the distance between the pointers in bytes is a multiple of size_of::, + // which holds if either both ptr_1 and ptr_2 are aligned or neither are. + // However, any_in_bounds makes no guarantees about alignment, so the above condition may not hold and verification should fail. + unsafe { ptr_1.offset_from(ptr_2) }; +} diff --git a/tests/expected/offset-wraps-around/expected b/tests/expected/offset-wraps-around/expected index 2fedc9da1a89..3ad0fbdad6e7 100644 --- a/tests/expected/offset-wraps-around/expected +++ b/tests/expected/offset-wraps-around/expected @@ -5,7 +5,7 @@ Checking harness harness_without_ub... VERIFICATION:- SUCCESSFUL Checking harness original_harness... -Failed Checks: assertion failed: high_offset == wrapped_offset.try_into().unwrap() +Failed Checks: Offset result and original pointer should point to the same allocation VERIFICATION:- FAILED Verification failed for - original_harness diff --git a/tests/kani/PointerOffset/offset_from_vec.rs b/tests/kani/PointerOffset/offset_from_vec.rs new file mode 100644 index 000000000000..482b4905df3c --- /dev/null +++ b/tests/kani/PointerOffset/offset_from_vec.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that offset_from_ptr works for vector and types with size that are not power of two. +#![feature(ptr_sub_ptr)] + +#[kani::proof] +#[kani::unwind(5)] +fn offset_from_vec() { + let v1 = vec![vec![1], vec![2]]; + let it = v1.into_iter(); + assert_eq!(it.size_hint().0, 2); +} + +#[kani::proof] +fn offset_non_power_two() { + let mut v = vec![[0u64; 3], [2u64; 3]]; + unsafe { + 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); + } +}