More LLM-generated pre-condition

Author: Fedor Ryabinin

library/alloc/src/boxed/convert.rs

@@ -1,3 +1,12 @@
+#![feature(ub_checks)]
+use safety::{ensures,requires};
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+use core::kani;
+#[allow(unused_imports)]
+#[unstable(feature = "ub_checks", issue = "none")]
+use core::ub_checks::*;
+
 use core::any::Any;
 use core::error::Error;
 use core::mem;
@@ -275,6 +284,7 @@ impl<T, const N: usize> From<[T; N]> for Box<[T]> {
 /// # Safety
 ///
 /// `boxed_slice.len()` must be exactly `N`.
+#[requires(boxed_slice.len() == N)]
 unsafe fn boxed_slice_as_array_unchecked<T, A: Allocator, const N: usize>(
     boxed_slice: Box<[T], A>,
 ) -> Box<[T; N], A> {
@@ -391,6 +401,7 @@ impl<A: Allocator> Box<dyn Any, A> {
     /// [`downcast`]: Self::downcast
     #[inline]
     #[unstable(feature = "downcast_unchecked", issue = "90850")]
+    #[requires(self.is::<T>())]
     pub unsafe fn downcast_unchecked<T: Any>(self) -> Box<T, A> {
         debug_assert!(self.is::<T>());
         unsafe {
@@ -450,6 +461,7 @@ impl<A: Allocator> Box<dyn Any + Send, A> {
     /// [`downcast`]: Self::downcast
     #[inline]
     #[unstable(feature = "downcast_unchecked", issue = "90850")]
+    #[requires(self.is::<T>())]
     pub unsafe fn downcast_unchecked<T: Any>(self) -> Box<T, A> {
         debug_assert!(self.is::<T>());
         unsafe {
@@ -509,6 +521,7 @@ impl<A: Allocator> Box<dyn Any + Send + Sync, A> {
     /// [`downcast`]: Self::downcast
     #[inline]
     #[unstable(feature = "downcast_unchecked", issue = "90850")]
+    #[requires(self.is::<T>())]
     pub unsafe fn downcast_unchecked<T: Any>(self) -> Box<T, A> {
         debug_assert!(self.is::<T>());
         unsafe {

library/alloc/src/collections/vec_deque/drain.rs

@@ -1,3 +1,12 @@
+#![feature(ub_checks)]
+use safety::{ensures,requires};
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+use core::kani;
+#[allow(unused_imports)]
+#[unstable(feature = "ub_checks", issue = "none")]
+use core::ub_checks::*;
+
 use core::iter::FusedIterator;
 use core::marker::PhantomData;
 use core::mem::{self, SizedTypeProperties};
@@ -34,6 +43,10 @@ pub struct Drain<
 }
 
 impl<'a, T, A: Allocator> Drain<'a, T, A> {
+    #[requires(drain_start <= deque.len())]
+    #[requires(drain_len <= deque.len())]
+    #[requires(drain_start + drain_len <= deque.len())]
+    #[cfg_attr(kani, kani::modifies(deque))]
     pub(super) unsafe fn new(
         deque: &'a mut VecDeque<T, A>,
         drain_start: usize,
@@ -53,6 +66,8 @@ impl<'a, T, A: Allocator> Drain<'a, T, A> {
 
     // Only returns pointers to the slices, as that's all we need
     // to drop them. May only be called if `self.remaining != 0`.
+    #[requires(self.remaining != 0)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn as_slices(&self) -> (*mut [T], *mut [T]) {
         unsafe {
             let deque = self.deque.as_ref();

library/alloc/src/str.rs

@@ -2,11 +2,20 @@
 //!
 //! *[See also the `str` primitive type](str).*
 
+#![feature(ub_checks)]
 #![stable(feature = "rust1", since = "1.0.0")]
 // Many of the usings in this module are only used in the test configuration.
 // It's cleaner to just turn off the unused_imports warning than to fix them.
 #![allow(unused_imports)]
 
+use safety::{ensures,requires};
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+use core::kani;
+#[allow(unused_imports)]
+#[unstable(feature = "ub_checks", issue = "none")]
+use core::ub_checks::*;
+
 use core::borrow::{Borrow, BorrowMut};
 use core::iter::FusedIterator;
 use core::mem::MaybeUninit;
@@ -615,6 +624,7 @@ impl str {
 #[stable(feature = "str_box_extras", since = "1.20.0")]
 #[must_use]
 #[inline]
+#[requires(core::str::from_utf8(&v).is_ok())]
 pub unsafe fn from_boxed_utf8_unchecked(v: Box<[u8]>) -> Box<str> {
     unsafe { Box::from_raw(Box::into_raw(v) as *mut str) }
 }
@@ -712,3 +722,27 @@ unsafe fn replace_ascii(utf8_bytes: &[u8], from: u8, to: u8) -> String {
     // SAFETY: We replaced ascii with ascii on valid utf8 strings.
     unsafe { String::from_utf8_unchecked(result) }
 }
+#[cfg(kani)]
+mod verify {
+    use super::*;
+    #[kani::proof_for_contract(from_boxed_utf8_unchecked)]
+    fn from_boxed_utf8_unchecked_contract() {
+        // Create a small array of valid UTF-8 bytes (ASCII "hello")
+        let valid_utf8_bytes = [b'h', b'e', b'l', b'l', b'o'];
+
+        // Create a Box<[u8]> from the array
+        let boxed_bytes = Box::new(valid_utf8_bytes);
+
+        // Call the function being verified
+        let _boxed_str = unsafe { from_boxed_utf8_unchecked(boxed_bytes) };
+
+        // Create another array with non-ASCII but valid UTF-8 sequence
+        // UTF-8 encoding of "helloé"
+        let valid_utf8_bytes_2 = [b'h', b'e', b'l', b'l', b'o', 0xC3, 0xA9];
+
+        let boxed_bytes_2 = Box::new(valid_utf8_bytes_2);
+
+        // Call the function being verified
+        let _boxed_str_2 = unsafe { from_boxed_utf8_unchecked(boxed_bytes_2) };
+    }
+}

library/alloc/src/task.rs

@@ -1,3 +1,4 @@
+#![feature(ub_checks)]
 #![stable(feature = "wake_trait", since = "1.51.0")]
 
 //! Types and Traits for working with asynchronous tasks.
@@ -7,6 +8,14 @@
 //! This may be detected at compile time using
 //! `#[cfg(target_has_atomic = "ptr")]`.
 
+use safety::{ensures,requires};
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+use core::kani;
+#[allow(unused_imports)]
+#[unstable(feature = "ub_checks", issue = "none")]
+use core::ub_checks::*;
+
 use core::mem::ManuallyDrop;
 #[cfg(target_has_atomic = "ptr")]
 use core::task::Waker;
@@ -145,6 +154,7 @@ fn raw_waker<W: Wake + Send + Sync + 'static>(waker: Arc<W>) -> RawWaker {
     // the vtable pointers, rather than comparing all four function pointers
     // within the vtables.
     #[inline(always)]
+    #[requires(waker != core::ptr::null())]
     unsafe fn clone_waker<W: Wake + Send + Sync + 'static>(waker: *const ()) -> RawWaker {
         unsafe { Arc::increment_strong_count(waker as *const W) };
         RawWaker::new(
@@ -154,18 +164,21 @@ fn raw_waker<W: Wake + Send + Sync + 'static>(waker: Arc<W>) -> RawWaker {
     }
 
     // Wake by value, moving the Arc into the Wake::wake function
+    #[requires(waker != core::ptr::null())]
     unsafe fn wake<W: Wake + Send + Sync + 'static>(waker: *const ()) {
         let waker = unsafe { Arc::from_raw(waker as *const W) };
         <W as Wake>::wake(waker);
     }
 
     // Wake by reference, wrap the waker in ManuallyDrop to avoid dropping it
+    #[requires(waker != core::ptr::null())]
     unsafe fn wake_by_ref<W: Wake + Send + Sync + 'static>(waker: *const ()) {
         let waker = unsafe { ManuallyDrop::new(Arc::from_raw(waker as *const W)) };
         <W as Wake>::wake_by_ref(&waker);
     }
 
     // Decrement the reference count of the Arc on drop
+    #[requires(waker != core::ptr::null())]
     unsafe fn drop_waker<W: Wake + Send + Sync + 'static>(waker: *const ()) {
         unsafe { Arc::decrement_strong_count(waker as *const W) };
     }
@@ -318,6 +331,7 @@ fn local_raw_waker<W: LocalWake + 'static>(waker: Rc<W>) -> RawWaker {
     // Refer to the comment on raw_waker's clone_waker regarding why this is
     // always inline.
     #[inline(always)]
+    #[requires(waker != core::ptr::null())]
     unsafe fn clone_waker<W: LocalWake + 'static>(waker: *const ()) -> RawWaker {
         unsafe { Rc::increment_strong_count(waker as *const W) };
         RawWaker::new(
@@ -327,18 +341,21 @@ fn local_raw_waker<W: LocalWake + 'static>(waker: Rc<W>) -> RawWaker {
     }
 
     // Wake by value, moving the Rc into the LocalWake::wake function
+    #[requires(waker != core::ptr::null())]
     unsafe fn wake<W: LocalWake + 'static>(waker: *const ()) {
         let waker = unsafe { Rc::from_raw(waker as *const W) };
         <W as LocalWake>::wake(waker);
     }
 
     // Wake by reference, wrap the waker in ManuallyDrop to avoid dropping it
+    #[requires(waker != core::ptr::null())]
     unsafe fn wake_by_ref<W: LocalWake + 'static>(waker: *const ()) {
         let waker = unsafe { ManuallyDrop::new(Rc::from_raw(waker as *const W)) };
         <W as LocalWake>::wake_by_ref(&waker);
     }
 
     // Decrement the reference count of the Rc on drop
+    #[requires(waker != core::ptr::null())]
     unsafe fn drop_waker<W: LocalWake + 'static>(waker: *const ()) {
         unsafe { Rc::decrement_strong_count(waker as *const W) };
     }

library/alloc/src/vec/spec_from_elem.rs

@@ -1,3 +1,14 @@
+#![feature(ub_checks)]
+use core::ub_checks::Invariant;
+
+use safety::{ensures,requires};
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+use core::kani;
+#[allow(unused_imports)]
+#[unstable(feature = "ub_checks", issue = "none")]
+use core::ub_checks::*;
+
 use core::ptr;
 
 use super::{IsZero, Vec};
@@ -34,6 +45,7 @@ impl<T: Clone + IsZero> SpecFromElem for T {
 impl SpecFromElem for i8 {
     #[inline]
     #[track_caller]
+    #[requires(n <= isize::MAX as usize)]
     fn from_elem<A: Allocator>(elem: i8, n: usize, alloc: A) -> Vec<i8, A> {
         if elem == 0 {
             return Vec { buf: RawVec::with_capacity_zeroed_in(n, alloc), len: n };
@@ -50,6 +62,7 @@ impl SpecFromElem for i8 {
 impl SpecFromElem for u8 {
     #[inline]
     #[track_caller]
+    #[requires(n <= isize::MAX as usize)]
     fn from_elem<A: Allocator>(elem: u8, n: usize, alloc: A) -> Vec<u8, A> {
         if elem == 0 {
             return Vec { buf: RawVec::with_capacity_zeroed_in(n, alloc), len: n };
@@ -67,6 +80,7 @@ impl SpecFromElem for u8 {
 // but the latter cannot be detected currently
 impl SpecFromElem for () {
     #[inline]
+    #[requires(n <= isize::MAX as usize)]
     fn from_elem<A: Allocator>(_elem: (), n: usize, alloc: A) -> Vec<(), A> {
         let mut v = Vec::with_capacity_in(n, alloc);
         // SAFETY: the capacity has just been set to `n`
@@ -77,3 +91,10 @@ impl SpecFromElem for () {
         v
     }
 }
+
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<T, A: Allocator> Invariant for Vec<T, A> {
+    fn is_safe(&self) -> bool {
+        self.len <= self.buf.capacity()
+    }
+}

library/alloctests/benches/vec_deque.rs

@@ -1,3 +1,14 @@
+#![feature(ub_checks)]
+use core::ub_checks::Invariant;
+
+use safety::{ensures,requires};
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+use core::kani;
+#[allow(unused_imports)]
+#[unstable(feature = "ub_checks", issue = "none")]
+use core::ub_checks::*;
+
 use std::collections::{VecDeque, vec_deque};
 use std::mem;
 
@@ -57,6 +68,8 @@ fn bench_try_fold(b: &mut Bencher) {
 
 /// does the memory bookkeeping to reuse the buffer of the Vec between iterations.
 /// `setup` must not modify its argument's length or capacity. `g` must not move out of its argument.
+#[requires(v.len() <= isize::MAX as usize)]
+#[requires(can_dereference(v.as_ptr()))]
 fn into_iter_helper<
     T: Copy,
     F: FnOnce(&mut VecDeque<T>),
@@ -265,3 +278,10 @@ fn bench_extend_chained_bytes(b: &mut Bencher) {
         ring.extend(black_box(input1.iter().chain(input2.iter())));
     });
 }
+
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<T> Invariant for Vec<T> {
+    fn is_safe(&self) -> bool {
+        self.len() <= self.capacity()
+    }
+}

library/alloctests/tests/sort/ffi_types.rs

@@ -1,3 +1,5 @@
+use core::ub_checks::Invariant;
+
 use std::cmp::Ordering;
 
 // Very large stack value.
@@ -80,3 +82,10 @@ impl Ord for F128 {
         unsafe { this_div.partial_cmp(&other_div).unwrap_unchecked() }
     }
 }
+
+#[unstable(feature = "ub_checks", issue = "none")]
+impl Invariant for F128 {
+    fn is_safe(&self) -> bool {
+        self.x.is_normal() && self.y.is_normal()
+    }
+}

library/alloctests/tests/vec.rs

@@ -1,3 +1,5 @@
+use core::ub_checks::Invariant;
+
 use core::alloc::{Allocator, Layout};
 use core::num::NonZero;
 use core::ptr::NonNull;
@@ -2704,3 +2706,10 @@ fn vec_null_ptr_roundtrip() {
     let new = roundtripped.with_addr(ptr.addr());
     unsafe { new.read() };
 }
+
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<T> Invariant for Vec<T> {
+    fn is_safe(&self) -> bool {
+        self.len() <= self.capacity()
+    }
+}

library/alloctests/tests/vec_deque.rs

@@ -1,3 +1,14 @@
+#![feature(ub_checks)]
+use core::ub_checks::Invariant;
+
+use safety::{ensures,requires};
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+use core::kani;
+#[allow(unused_imports)]
+#[unstable(feature = "ub_checks", issue = "none")]
+use core::ub_checks::*;
+
 use core::num::NonZero;
 use std::assert_matches::assert_matches;
 use std::collections::TryReserveErrorKind::*;
@@ -1074,6 +1085,9 @@ fn test_append_double_drop() {
 
 #[test]
 #[should_panic]
+#[requires(v.capacity() == usize::MAX)]
+#[requires(core::mem::size_of::<()>() == 0)]
+#[requires(can_write(v.as_mut_ptr()))]
 fn test_append_zst_capacity_overflow() {
     let mut v = Vec::with_capacity(usize::MAX);
     // note: using resize instead of set_len here would
@@ -1849,3 +1863,10 @@ fn test_truncate_front() {
     v.truncate_front(5);
     assert_eq!(v.as_slices(), ([2, 3, 4, 5, 6].as_slice(), [].as_slice()));
 }
+
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<T> Invariant for VecDeque<T> {
+    fn is_safe(&self) -> bool {
+        self.len() <= self.capacity()
+    }
+}