From f4c677ce3794f4d8c7fa63f7c73a9236eeb8d6a5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 4 Aug 2026 11:34:49 +0000 Subject: [PATCH] Do not dereference in slice_from_raw_parts postcondition NonNull::slice_from_raw_parts is a safe function with no validity requirements on `data`: per its documentation, it is safe to construct the pointer, and only its use is subject to safety conditions. Its postcondition however evaluated `unsafe { result.as_ref() }.len()`, creating a reference to the pointed-to memory just to read the slice length - undefined behavior when `data` is dangling or misaligned, and a failing check when the contract is evaluated in such a context. This surfaces with dependency contracts asserted (the Kani default since model-checking/kani#3802): ptr::non_null::verify::non_null_check_as_uninit_slice_mut constructs, legitimately, a NonNull slice pointer whose span may exceed the backing allocation; evaluating slice_from_raw_parts' postcondition then fails with "misaligned pointer to reference cast" / "dereference failure: pointer invalid" inside NonNull::as_ref. CI currently masks this with --no-assert-contracts. Read the length from the wide-pointer metadata via NonNull::len instead, which involves no dereference (and no unsafe code) and is the property the clause is about in the first place. The dereferencing clause was introduced with the original contracts in 07318dfc34a ("Contracts and harnesses for `dangling`, `from_raw_parts`, `slice_from_raw_parts`, `to_raw_parts` in NonNull" #127). Verified (Kani 152c6a8c + CBMC 6.10.0): non_null_check_as_uninit_slice_mut, non_null_check_slice_from_raw_parts, non_null_check_as_uninit_slice and non_null_check_len pass both with and without --no-assert-contracts (the first previously failed with contracts asserted). Co-authored-by: Kiro --- library/core/src/ptr/non_null.rs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 775034399717d..dac339518469d 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1590,9 +1590,14 @@ impl NonNull<[T]> { #[rustc_const_stable(feature = "const_slice_from_raw_parts_mut", since = "1.83.0")] #[must_use] #[inline] + // `result.len()` reads the length from the wide-pointer metadata without + // creating a reference: `slice_from_raw_parts` is a safe function with no + // validity requirements on `data`, so the postcondition must not + // dereference the resulting pointer (`unsafe { result.as_ref() }.len()`, + // as used previously, is UB for dangling or misaligned `data`). #[ensures(|result| !result.pointer.is_null() && result.pointer as *const T == data.pointer - && unsafe { result.as_ref() }.len() == len)] + && result.len() == len)] pub const fn slice_from_raw_parts(data: NonNull, len: usize) -> Self { // SAFETY: `data` is a `NonNull` pointer which is necessarily non-null unsafe { Self::new_unchecked(super::slice_from_raw_parts_mut(data.as_ptr(), len)) }