Merge branch 'main' into add-result-contract

.github/workflows/kani.yml

@@ -9,6 +9,7 @@ on:
  paths:
  - 'library/**'
  - '.github/workflows/kani.yml'
+ - 'scripts/check_kani.sh'
 
 defaults:
  run:
@@ -30,32 +31,8 @@ jobs:
  - name: Checkout Library
  uses: actions/checkout@v4
  with:
- path: verify-rust-std
+ path: head
  submodules: true
 
- # We currently build Kani from a branch that tracks a rustc version compatible with this library version.
- - name: Checkout `Kani`
- uses: actions/checkout@v4
- with:
- repository: model-checking/kani
- path: kani
- ref: features/verify-rust-std
-
- - name: Setup Dependencies
- working-directory: kani
- run: |
- ./scripts/setup/${{ matrix.base }}/install_deps.sh
-
- - name: Build `Kani`
- working-directory: kani
- run: |
- cargo build-dev --release
- echo "$(pwd)/scripts" >> $GITHUB_PATH
-
- - name: Run tests
- working-directory: verify-rust-std
- env:
- RUST_BACKTRACE: 1
- run: |
- kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
- -Z mem-predicates -Z ptr-to-ref-cast-checks
+ - name: Run Kani Script
+ run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head

.github/workflows/rustc.yml

@@ -11,6 +11,7 @@ on:
  - 'library/**'
  - 'rust-toolchain.toml'
  - '.github/workflows/rustc.yml'
+ - 'scripts/check_rustc.sh'
 
 defaults:
  run:
@@ -29,35 +30,5 @@ jobs:
  with:
  path: head
 
- - name: Checkout `upstream/master`
- uses: actions/checkout@v4
- with:
- repository: rust-lang/rust
- path: upstream
- fetch-depth: 0
- submodules: true
-
- # Run rustc twice in case the toolchain needs to be installed.
- # Retrieve the commit id from the `rustc --version`. Output looks like:
- # `rustc 1.80.0-nightly (84b40fc90 2024-05-27)`
- - name: Checkout matching commit
- run: |
- cd head
- rustc --version
- COMMIT_ID=$(rustc --version | sed -e "s/.*(\(.*\) .*/\1/")
- cd ../upstream
- git checkout ${COMMIT_ID}
-
- - name: Copy Library
- run: |
- rm -rf upstream/library
- cp -r head/library upstream
-
- - name: Run tests
- working-directory: upstream
- env:
- # Avoid error due to unexpected `cfg`.
- RUSTFLAGS: "--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))"
- run: |
- ./configure --set=llvm.download-ci-llvm=true
- ./x test --stage 0 library/std
+ - name: Run rustc script
+ run: bash ./head/scripts/check_rustc.sh ${{github.workspace}}/head

doc/src/SUMMARY.md

@@ -16,4 +16,5 @@
  - [Core Transmutation](./challenges/0001-core-transmutation.md)
  - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md)
  - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
+ - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
  - [Inductive data type](./challenges/0005-linked-list.md)

doc/src/challenges/0004-btree-node.md

@@ -0,0 +1,68 @@
+# Challenge 4: Memory safety of BTreeMap's `btree::node` module
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25)
+- **Start date:** *2024-07-01*
+- **End date:** *2024-12-10*
+
+-------------------
+
+
+## Goal
+
+Verify the memory safety of the [`alloc::collections::btree::node` module](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/btree/node.rs).
+This is one of the main modules used for implementing the `BTreeMap` collection, and it includes a lot of unsafe code.
+
+### Success Criteria
+
+The memory safety of all public functions (especially safe ones) containing unsafe code must be verified, e.g.:
+
+1. `LeafNode::new`
+1. `NodeRef::as_internal_mut`
+1. `NodeRef::len`
+1. `NodeRef::ascend`
+1. `NodeRef::first_edge`
+1. `NodeRef::last_edge`
+1. `NodeRef::first_kv`
+1. `NodeRef::last_kv`
+1. `NodeRef::into_leaf`
+1. `NodeRef::keys`
+1. `NodeRef::as_leaf_mut`
+1. `NodeRef::into_leaf_mut`
+1. `NodeRef::as_leaf_dying`
+1. `NodeRef::pop_internal_level`
+1. `NodeRef::push`
+1. `Handle::left_edge`
+1. `Handle::right_edge`
+1. `Handle::left_kv`
+1. `Handle::right_kv`
+1. `Handle::descend`
+1. `Handle::into_kv`
+1. `Handle::key_mut`
+1. `Handle::into_val_mut`
+1. `Handle::into_kv_mut`
+1. `Handle::into_kv_valmut`
+1. `Handle::kv_mut`
+
+Verification must be unbounded for functions that use recursion or contain loops, e.g.
+
+1. `NodeRef::new_internal`
+1. `Handle::insert_recursing`
+1. `BalancingContext::do_merge`
+1. `BalancingContext::merge_tracking_child_edge`
+1. `BalancingContext::steal_left`
+1. `BalancingContext::steal_right`
+1. `BalancingContext::bulk_steal_left`
+1. `BalancingContext::bulk_steal_right`
+
+### List of UBs
+
+All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.

library/alloc/Cargo.toml

@@ -20,6 +20,10 @@ rand_xorshift = "0.3.0"
 name = "alloctests"
 path = "tests/lib.rs"
 
+[[test]]
+name = "vec_deque_alloc_error"
+path = "tests/vec_deque_alloc_error.rs"
+
 [[bench]]
 name = "allocbenches"
 path = "benches/lib.rs"
@@ -43,9 +47,6 @@ optimize_for_size = ["core/optimize_for_size"]
 
 [lints.rust.unexpected_cfgs]
 level = "warn"
-# x.py uses beta cargo, so `check-cfg` entries do not yet take effect
-# for rust-lang/rust. But for users of `-Zbuild-std` it does.
-# The unused warning is waiting for rust-lang/cargo#13925 to reach beta.
 check-cfg = [
  'cfg(bootstrap)',
  'cfg(no_global_oom_handling)',

library/alloc/src/alloc.rs

@@ -424,29 +424,3 @@ pub mod __alloc_error_handler {
  }
  }
 }
-
-#[cfg(not(no_global_oom_handling))]
-/// Specialize clones into pre-allocated, uninitialized memory.
-/// Used by `Box::clone` and `Rc`/`Arc::make_mut`.
-pub(crate) trait WriteCloneIntoRaw: Sized {
- unsafe fn write_clone_into_raw(&self, target: *mut Self);
-}
-
-#[cfg(not(no_global_oom_handling))]
-impl<T: Clone> WriteCloneIntoRaw for T {
- #[inline]
- default unsafe fn write_clone_into_raw(&self, target: *mut Self) {
- // Having allocated *first* may allow the optimizer to create
- // the cloned value in-place, skipping the local and move.
- unsafe { target.write(self.clone()) };
- }
-}
-
-#[cfg(not(no_global_oom_handling))]
-impl<T: Copy> WriteCloneIntoRaw for T {
- #[inline]
- unsafe fn write_clone_into_raw(&self, target: *mut Self) {
- // We can always copy in-place, without ever involving a local value.
- unsafe { target.copy_from_nonoverlapping(self, 1) };
- }
-}

library/alloc/src/boxed.rs

@@ -145,8 +145,7 @@
 //! to `into_iter()` for boxed slices will defer to the slice implementation on editions before
 //! 2024:
 //!
-#![cfg_attr(bootstrap, doc = "```rust,edition2021,ignore")]
-#![cfg_attr(not(bootstrap), doc = "```rust,edition2021")]
+//! ```rust,edition2021
 //! // Rust 2015, 2018, and 2021:
 //!
 //! # #![allow(boxed_slice_into_iter)] // override our `deny(warnings)`
@@ -189,6 +188,8 @@
 use core::any::Any;
 use core::async_iter::AsyncIterator;
 use core::borrow;
+#[cfg(not(no_global_oom_handling))]
+use core::clone::CloneToUninit;
 use core::cmp::Ordering;
 use core::error::Error;
 use core::fmt;
@@ -208,7 +209,7 @@ use core::slice;
 use core::task::{Context, Poll};
 
 #[cfg(not(no_global_oom_handling))]
-use crate::alloc::{handle_alloc_error, WriteCloneIntoRaw};
+use crate::alloc::handle_alloc_error;
 use crate::alloc::{AllocError, Allocator, Global, Layout};
 #[cfg(not(no_global_oom_handling))]
 use crate::borrow::Cow;
@@ -1212,6 +1213,9 @@ impl<T: ?Sized, A: Allocator> Box<T, A> {
  /// let static_ref: &'static mut usize = Box::leak(x);
  /// *static_ref += 1;
  /// assert_eq!(*static_ref, 42);
+ /// # // FIXME(https://github.com/rust-lang/miri/issues/3670):
+ /// # // use -Zmiri-disable-leak-check instead of unleaking in tests meant to leak.
+ /// # drop(unsafe { Box::from_raw(static_ref) });
  /// ```
  ///
  /// Unsized data:
@@ -1221,6 +1225,9 @@ impl<T: ?Sized, A: Allocator> Box<T, A> {
  /// let static_ref = Box::leak(x);
  /// static_ref[0] = 4;
  /// assert_eq!(*static_ref, [4, 2, 3]);
+ /// # // FIXME(https://github.com/rust-lang/miri/issues/3670):
+ /// # // use -Zmiri-disable-leak-check instead of unleaking in tests meant to leak.
+ /// # drop(unsafe { Box::from_raw(static_ref) });
  /// ```
  #[stable(feature = "box_leak", since = "1.26.0")]
  #[inline]
@@ -1347,7 +1354,7 @@ impl<T: Clone, A: Allocator + Clone> Clone for Box<T, A> {
  // Pre-allocate memory to allow writing the cloned value directly.
  let mut boxed = Self::new_uninit_in(self.1.clone());
  unsafe {
- (**self).write_clone_into_raw(boxed.as_mut_ptr());
+ (**self).clone_to_uninit(boxed.as_mut_ptr());
  boxed.assume_init()
  }
  }
@@ -2123,23 +2130,23 @@ impl<I> FromIterator<I> for Box<[I]> {
 
 /// This implementation is required to make sure that the `Box<[I]>: IntoIterator`
 /// implementation doesn't overlap with `IntoIterator for T where T: Iterator` blanket.
-#[stable(feature = "boxed_slice_into_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_slice_into_iter", since = "1.80.0")]
 impl<I, A: Allocator> !Iterator for Box<[I], A> {}
 
 /// This implementation is required to make sure that the `&Box<[I]>: IntoIterator`
 /// implementation doesn't overlap with `IntoIterator for T where T: Iterator` blanket.
-#[stable(feature = "boxed_slice_into_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_slice_into_iter", since = "1.80.0")]
 impl<'a, I, A: Allocator> !Iterator for &'a Box<[I], A> {}
 
 /// This implementation is required to make sure that the `&mut Box<[I]>: IntoIterator`
 /// implementation doesn't overlap with `IntoIterator for T where T: Iterator` blanket.
-#[stable(feature = "boxed_slice_into_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_slice_into_iter", since = "1.80.0")]
 impl<'a, I, A: Allocator> !Iterator for &'a mut Box<[I], A> {}
 
 // Note: the `#[rustc_skip_during_method_dispatch(boxed_slice)]` on `trait IntoIterator`
 // hides this implementation from explicit `.into_iter()` calls on editions < 2024,
 // so those calls will still resolve to the slice implementation, by reference.
-#[stable(feature = "boxed_slice_into_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_slice_into_iter", since = "1.80.0")]
 impl<I, A: Allocator> IntoIterator for Box<[I], A> {
  type IntoIter = vec::IntoIter<I, A>;
  type Item = I;
@@ -2148,7 +2155,7 @@ impl<I, A: Allocator> IntoIterator for Box<[I], A> {
  }
 }
 
-#[stable(feature = "boxed_slice_into_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_slice_into_iter", since = "1.80.0")]
 impl<'a, I, A: Allocator> IntoIterator for &'a Box<[I], A> {
  type IntoIter = slice::Iter<'a, I>;
  type Item = &'a I;
@@ -2157,7 +2164,7 @@ impl<'a, I, A: Allocator> IntoIterator for &'a Box<[I], A> {
  }
 }
 
-#[stable(feature = "boxed_slice_into_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_slice_into_iter", since = "1.80.0")]
 impl<'a, I, A: Allocator> IntoIterator for &'a mut Box<[I], A> {
  type IntoIter = slice::IterMut<'a, I>;
  type Item = &'a mut I;
@@ -2167,47 +2174,47 @@ impl<'a, I, A: Allocator> IntoIterator for &'a mut Box<[I], A> {
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "boxed_str_from_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_str_from_iter", since = "1.80.0")]
 impl FromIterator<char> for Box<str> {
  fn from_iter<T: IntoIterator<Item = char>>(iter: T) -> Self {
  String::from_iter(iter).into_boxed_str()
  }
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "boxed_str_from_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_str_from_iter", since = "1.80.0")]
 impl<'a> FromIterator<&'a char> for Box<str> {
  fn from_iter<T: IntoIterator<Item = &'a char>>(iter: T) -> Self {
  String::from_iter(iter).into_boxed_str()
  }
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "boxed_str_from_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_str_from_iter", since = "1.80.0")]
 impl<'a> FromIterator<&'a str> for Box<str> {
  fn from_iter<T: IntoIterator<Item = &'a str>>(iter: T) -> Self {
  String::from_iter(iter).into_boxed_str()
  }
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "boxed_str_from_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_str_from_iter", since = "1.80.0")]
 impl FromIterator<String> for Box<str> {
  fn from_iter<T: IntoIterator<Item = String>>(iter: T) -> Self {
  String::from_iter(iter).into_boxed_str()
  }
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "boxed_str_from_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_str_from_iter", since = "1.80.0")]
 impl<A: Allocator> FromIterator<Box<str, A>> for Box<str> {
  fn from_iter<T: IntoIterator<Item = Box<str, A>>>(iter: T) -> Self {
  String::from_iter(iter).into_boxed_str()
  }
 }
 
 #[cfg(not(no_global_oom_handling))]
-#[stable(feature = "boxed_str_from_iter", since = "CURRENT_RUSTC_VERSION")]
+#[stable(feature = "boxed_str_from_iter", since = "1.80.0")]
 impl<'a> FromIterator<Cow<'a, str>> for Box<str> {
  fn from_iter<T: IntoIterator<Item = Cow<'a, str>>>(iter: T) -> Self {
  String::from_iter(iter).into_boxed_str()
@@ -2373,7 +2380,7 @@ impl dyn Error + Send {
  let err: Box<dyn Error> = self;
  <dyn Error>::downcast(err).map_err(|s| unsafe {
  // Reapply the `Send` marker.
- Box::from_raw(Box::into_raw(s) as *mut (dyn Error + Send))
+ mem::transmute::<Box<dyn Error>, Box<dyn Error + Send>>(s)
  })
  }
 }
@@ -2386,8 +2393,8 @@ impl dyn Error + Send + Sync {
  pub fn downcast<T: Error + 'static>(self: Box<Self>) -> Result<Box<T>, Box<Self>> {
  let err: Box<dyn Error> = self;
  <dyn Error>::downcast(err).map_err(|s| unsafe {
- // Reapply the `Send + Sync` marker.
- Box::from_raw(Box::into_raw(s) as *mut (dyn Error + Send + Sync))
+ // Reapply the `Send + Sync` markers.
+ mem::transmute::<Box<dyn Error>, Box<dyn Error + Send + Sync>>(s)
  })
  }
 }