diff --git a/library/alloc/src/collections/linked_list.rs b/library/alloc/src/collections/linked_list.rs index 70c344e49b76a..31dfe73fc7992 100644 --- a/library/alloc/src/collections/linked_list.rs +++ b/library/alloc/src/collections/linked_list.rs @@ -825,7 +825,7 @@ impl LinkedList { unsafe { self.tail.as_mut().map(|node| &mut node.as_mut().element) } } - /// Adds an element first in the list. + /// Adds an element to the front of the list. /// /// This operation should compute in *O*(1) time. /// @@ -844,11 +844,34 @@ impl LinkedList { /// ``` #[stable(feature = "rust1", since = "1.0.0")] pub fn push_front(&mut self, elt: T) { + let _ = self.push_front_mut(elt); + } + + /// Adds an element to the front of the list, returning a reference to it. + /// + /// This operation should compute in *O*(1) time. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::LinkedList; + /// + /// let mut dl = LinkedList::from([1, 2, 3]); + /// + /// let ptr = dl.push_front_mut(2); + /// *ptr += 4; + /// assert_eq!(dl.front().unwrap(), &6); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[must_use = "if you don't need a reference to the value, use `LinkedList::push_front` instead"] + pub fn push_front_mut(&mut self, elt: T) -> &mut T { let node = Box::new_in(Node::new(elt), &self.alloc); - let node_ptr = NonNull::from(Box::leak(node)); + let mut node_ptr = NonNull::from(Box::leak(node)); // SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked unsafe { self.push_front_node(node_ptr); + &mut node_ptr.as_mut().element } } @@ -876,7 +899,7 @@ impl LinkedList { self.pop_front_node().map(Node::into_element) } - /// Appends an element to the back of a list. + /// Adds an element to the back of the list. /// /// This operation should compute in *O*(1) time. /// @@ -893,11 +916,34 @@ impl LinkedList { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_confusables("push", "append")] pub fn push_back(&mut self, elt: T) { + let _ = self.push_back_mut(elt); + } + + /// Adds an element to the back of the list, returning a reference to it. + /// + /// This operation should compute in *O*(1) time. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::LinkedList; + /// + /// let mut dl = LinkedList::from([1, 2, 3]); + /// + /// let ptr = dl.push_back_mut(2); + /// *ptr += 4; + /// assert_eq!(dl.back().unwrap(), &6); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[must_use = "if you don't need a reference to the value, use `LinkedList::push_back` instead"] + pub fn push_back_mut(&mut self, elt: T) -> &mut T { let node = Box::new_in(Node::new(elt), &self.alloc); - let node_ptr = NonNull::from(Box::leak(node)); + let mut node_ptr = NonNull::from(Box::leak(node)); // SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked unsafe { self.push_back_node(node_ptr); + &mut node_ptr.as_mut().element } } diff --git a/library/alloc/src/collections/vec_deque/mod.rs b/library/alloc/src/collections/vec_deque/mod.rs index 208f0da6fa830..9d78149a41347 100644 --- a/library/alloc/src/collections/vec_deque/mod.rs +++ b/library/alloc/src/collections/vec_deque/mod.rs @@ -185,11 +185,16 @@ impl VecDeque { unsafe { ptr::read(self.ptr().add(off)) } } - /// Writes an element into the buffer, moving it. + /// Writes an element into the buffer, moving it and returning a pointer to it. + /// # Safety + /// + /// May only be called if `off < self.capacity()`. #[inline] - unsafe fn buffer_write(&mut self, off: usize, value: T) { + unsafe fn buffer_write(&mut self, off: usize, value: T) -> &mut T { unsafe { - ptr::write(self.ptr().add(off), value); + let ptr = self.ptr().add(off); + ptr::write(ptr, value); + &mut *ptr } } @@ -1891,16 +1896,34 @@ impl VecDeque { #[stable(feature = "rust1", since = "1.0.0")] #[track_caller] pub fn push_front(&mut self, value: T) { + let _ = self.push_front_mut(value); + } + + /// Prepends an element to the deque, returning a reference to it. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::VecDeque; + /// + /// let mut d = VecDeque::from([1, 2, 3]); + /// let x = d.push_front_mut(8); + /// *x -= 1; + /// assert_eq!(d.front(), Some(&7)); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[track_caller] + #[must_use = "if you don't need a reference to the value, use `VecDeque::push_front` instead"] + pub fn push_front_mut(&mut self, value: T) -> &mut T { if self.is_full() { self.grow(); } self.head = self.wrap_sub(self.head, 1); self.len += 1; - - unsafe { - self.buffer_write(self.head, value); - } + // SAFETY: We know that self.head is within range of the deque. + unsafe { self.buffer_write(self.head, value) } } /// Appends an element to the back of the deque. @@ -1919,12 +1942,33 @@ impl VecDeque { #[rustc_confusables("push", "put", "append")] #[track_caller] pub fn push_back(&mut self, value: T) { + let _ = self.push_back_mut(value); + } + + /// Appends an element to the back of the deque, returning a reference to it. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::VecDeque; + /// + /// let mut d = VecDeque::from([1, 2, 3]); + /// let x = d.push_back_mut(9); + /// *x += 1; + /// assert_eq!(d.back(), Some(&10)); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[track_caller] + #[must_use = "if you don't need a reference to the value, use `VecDeque::push_back` instead"] + pub fn push_back_mut(&mut self, value: T) -> &mut T { if self.is_full() { self.grow(); } - unsafe { self.buffer_write(self.to_physical_idx(self.len), value) } + let len = self.len; self.len += 1; + unsafe { self.buffer_write(self.to_physical_idx(len), value) } } #[inline] @@ -2010,7 +2054,7 @@ impl VecDeque { /// /// # Panics /// - /// Panics if `index` is strictly greater than deque's length + /// Panics if `index` is strictly greater than the deque's length. /// /// # Examples /// @@ -2032,7 +2076,37 @@ impl VecDeque { #[stable(feature = "deque_extras_15", since = "1.5.0")] #[track_caller] pub fn insert(&mut self, index: usize, value: T) { + let _ = self.insert_mut(index, value); + } + + /// Inserts an element at `index` within the deque, shifting all elements + /// with indices greater than or equal to `index` towards the back, and + /// returning a reference to it. + /// + /// Element at index 0 is the front of the queue. + /// + /// # Panics + /// + /// Panics if `index` is strictly greater than the deque's length. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::VecDeque; + /// + /// let mut vec_deque = VecDeque::from([1, 2, 3]); + /// + /// let x = vec_deque.insert_mut(1, 5); + /// *x += 7; + /// assert_eq!(vec_deque, &[1, 12, 2, 3]); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[track_caller] + #[must_use = "if you don't need a reference to the value, use `VecDeque::insert` instead"] + pub fn insert_mut(&mut self, index: usize, value: T) -> &mut T { assert!(index <= self.len(), "index out of bounds"); + if self.is_full() { self.grow(); } @@ -2045,16 +2119,16 @@ impl VecDeque { unsafe { // see `remove()` for explanation why this wrap_copy() call is safe. self.wrap_copy(self.to_physical_idx(index), self.to_physical_idx(index + 1), k); - self.buffer_write(self.to_physical_idx(index), value); self.len += 1; + self.buffer_write(self.to_physical_idx(index), value) } } else { let old_head = self.head; self.head = self.wrap_sub(self.head, 1); unsafe { self.wrap_copy(old_head, self.head, index); - self.buffer_write(self.to_physical_idx(index), value); self.len += 1; + self.buffer_write(self.to_physical_idx(index), value) } } } diff --git a/library/alloc/src/vec/mod.rs b/library/alloc/src/vec/mod.rs index d69b31da8c27f..65db56710b51b 100644 --- a/library/alloc/src/vec/mod.rs +++ b/library/alloc/src/vec/mod.rs @@ -2046,6 +2046,38 @@ impl Vec { #[stable(feature = "rust1", since = "1.0.0")] #[track_caller] pub fn insert(&mut self, index: usize, element: T) { + let _ = self.insert_mut(index, element); + } + + /// Inserts an element at position `index` within the vector, shifting all + /// elements after it to the right, and returning a reference to the new + /// element. + /// + /// # Panics + /// + /// Panics if `index > len`. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// let mut vec = vec![1, 3, 5, 9]; + /// let x = vec.insert_mut(3, 6); + /// *x += 1; + /// assert_eq!(vec, [1, 3, 5, 7, 9]); + /// ``` + /// + /// # Time complexity + /// + /// Takes *O*([`Vec::len`]) time. All items after the insertion index must be + /// shifted to the right. In the worst case, all elements are shifted when + /// the insertion index is 0. + #[cfg(not(no_global_oom_handling))] + #[inline] + #[unstable(feature = "push_mut", issue = "135974")] + #[track_caller] + #[must_use = "if you don't need a reference to the value, use `Vec::insert` instead"] + pub fn insert_mut(&mut self, index: usize, element: T) -> &mut T { #[cold] #[cfg_attr(not(feature = "panic_immediate_abort"), inline(never))] #[track_caller] @@ -2067,8 +2099,8 @@ impl Vec { unsafe { // infallible // The spot to put the new value + let p = self.as_mut_ptr().add(index); { - let p = self.as_mut_ptr().add(index); if index < len { // Shift everything over to make space. (Duplicating the // `index`th element into two consecutive places.) @@ -2079,6 +2111,7 @@ impl Vec { ptr::write(p, element); } self.set_len(len + 1); + &mut *p } } @@ -2486,18 +2519,7 @@ impl Vec { #[rustc_confusables("push_back", "put", "append")] #[track_caller] pub fn push(&mut self, value: T) { - // Inform codegen that the length does not change across grow_one(). - let len = self.len; - // This will panic or abort if we would allocate > isize::MAX bytes - // or if the length increment would overflow for zero-sized types. - if len == self.buf.capacity() { - self.buf.grow_one(); - } - unsafe { - let end = self.as_mut_ptr().add(len); - ptr::write(end, value); - self.len = len + 1; - } + let _ = self.push_mut(value); } /// Appends an element if there is sufficient spare capacity, otherwise an error is returned @@ -2538,6 +2560,77 @@ impl Vec { #[inline] #[unstable(feature = "vec_push_within_capacity", issue = "100486")] pub fn push_within_capacity(&mut self, value: T) -> Result<(), T> { + self.push_mut_within_capacity(value).map(|_| ()) + } + + /// Appends an element to the back of a collection, returning a reference to it. + /// + /// # Panics + /// + /// Panics if the new capacity exceeds `isize::MAX` _bytes_. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// + /// + /// let mut vec = vec![1, 2]; + /// let last = vec.push_mut(3); + /// assert_eq!(*last, 3); + /// assert_eq!(vec, [1, 2, 3]); + /// + /// let last = vec.push_mut(3); + /// *last += 1; + /// assert_eq!(vec, [1, 2, 3, 4]); + /// ``` + /// + /// # Time complexity + /// + /// Takes amortized *O*(1) time. If the vector's length would exceed its + /// capacity after the push, *O*(*capacity*) time is taken to copy the + /// vector's elements to a larger allocation. This expensive operation is + /// offset by the *capacity* *O*(1) insertions it allows. + #[cfg(not(no_global_oom_handling))] + #[inline] + #[unstable(feature = "push_mut", issue = "135974")] + #[track_caller] + #[must_use = "if you don't need a reference to the value, use `Vec::push` instead"] + pub fn push_mut(&mut self, value: T) -> &mut T { + // Inform codegen that the length does not change across grow_one(). + let len = self.len; + // This will panic or abort if we would allocate > isize::MAX bytes + // or if the length increment would overflow for zero-sized types. + if len == self.buf.capacity() { + self.buf.grow_one(); + } + unsafe { + let end = self.as_mut_ptr().add(len); + ptr::write(end, value); + self.len = len + 1; + // SAFETY: We just wrote a value to the pointer that will live the lifetime of the reference. + &mut *end + } + } + + /// Appends an element and returns a reference to it if there is sufficient spare capacity, + /// otherwise an error is returned with the element. + /// + /// Unlike [`push_mut`] this method will not reallocate when there's insufficient capacity. + /// The caller should use [`reserve`] or [`try_reserve`] to ensure that there is enough capacity. + /// + /// [`push_mut`]: Vec::push_mut + /// [`reserve`]: Vec::reserve + /// [`try_reserve`]: Vec::try_reserve + /// + /// # Time complexity + /// + /// Takes *O*(1) time. + #[unstable(feature = "push_mut", issue = "135974")] + // #[unstable(feature = "vec_push_within_capacity", issue = "100486")] + #[inline] + #[must_use = "if you don't need a reference to the value, use `Vec::push_within_capacity` instead"] + pub fn push_mut_within_capacity(&mut self, value: T) -> Result<&mut T, T> { if self.len == self.buf.capacity() { return Err(value); } @@ -2545,8 +2638,9 @@ impl Vec { let end = self.as_mut_ptr().add(self.len); ptr::write(end, value); self.len += 1; + // SAFETY: We just wrote a value to the pointer that will live the lifetime of the reference. + Ok(&mut *end) } - Ok(()) } /// Removes the last element from a vector and returns it, or [`None`] if it diff --git a/library/std_detect/src/detect/arch/riscv.rs b/library/std_detect/src/detect/arch/riscv.rs index b86190d7bbf0c..1d21b1d485589 100644 --- a/library/std_detect/src/detect/arch/riscv.rs +++ b/library/std_detect/src/detect/arch/riscv.rs @@ -73,6 +73,7 @@ features! { /// * Zihintpause: `"zihintpause"` /// * Zihpm: `"zihpm"` /// * Zimop: `"zimop"` + /// * Zabha: `"zabha"` /// * Zacas: `"zacas"` /// * Zawrs: `"zawrs"` /// * Zfa: `"zfa"` @@ -195,6 +196,8 @@ features! { /// "Zaamo" Extension for Atomic Memory Operations @FEATURE: #[unstable(feature = "stdarch_riscv_feature_detection", issue = "111192")] zawrs: "zawrs"; /// "Zawrs" Extension for Wait-on-Reservation-Set Instructions + @FEATURE: #[unstable(feature = "stdarch_riscv_feature_detection", issue = "111192")] zabha: "zabha"; + /// "Zabha" Extension for Byte and Halfword Atomic Memory Operations @FEATURE: #[unstable(feature = "stdarch_riscv_feature_detection", issue = "111192")] zacas: "zacas"; /// "Zacas" Extension for Atomic Compare-and-Swap (CAS) Instructions @FEATURE: #[unstable(feature = "stdarch_riscv_feature_detection", issue = "111192")] zam: "zam"; diff --git a/library/std_detect/src/detect/os/linux/riscv.rs b/library/std_detect/src/detect/os/linux/riscv.rs index dbb3664890e56..18f9f68ec67ef 100644 --- a/library/std_detect/src/detect/os/linux/riscv.rs +++ b/library/std_detect/src/detect/os/linux/riscv.rs @@ -10,13 +10,13 @@ use super::super::riscv::imply_features; use super::auxvec; use crate::detect::{Feature, bit, cache}; -// See +// See // for runtime status query constants. const PR_RISCV_V_GET_CONTROL: libc::c_int = 70; const PR_RISCV_V_VSTATE_CTRL_ON: libc::c_int = 2; const PR_RISCV_V_VSTATE_CTRL_CUR_MASK: libc::c_int = 3; -// See +// See // for riscv_hwprobe struct and hardware probing constants. #[repr(C)] @@ -98,6 +98,7 @@ const RISCV_HWPROBE_EXT_ZVFBFWMA: u64 = 1 << 54; const RISCV_HWPROBE_EXT_ZICBOM: u64 = 1 << 55; const RISCV_HWPROBE_EXT_ZAAMO: u64 = 1 << 56; const RISCV_HWPROBE_EXT_ZALRSC: u64 = 1 << 57; +const RISCV_HWPROBE_EXT_ZABHA: u64 = 1 << 58; const RISCV_HWPROBE_KEY_CPUPERF_0: i64 = 5; const RISCV_HWPROBE_MISALIGNED_FAST: u64 = 3; @@ -138,7 +139,7 @@ pub(crate) fn detect_features() -> cache::Initializer { // Use auxiliary vector to enable single-letter ISA extensions. // The values are part of the platform-specific [asm/hwcap.h][hwcap] // - // [hwcap]: https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/arch/riscv/include/uapi/asm/hwcap.h?h=v6.15 + // [hwcap]: https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/arch/riscv/include/uapi/asm/hwcap.h?h=v6.16 let auxv = auxvec::auxv().expect("read auxvec"); // should not fail on RISC-V platform let mut has_i = bit::test(auxv.hwcap, (b'i' - b'a').into()); #[allow(clippy::eq_op)] @@ -233,6 +234,7 @@ pub(crate) fn detect_features() -> cache::Initializer { enable_feature(Feature::zalrsc, test(RISCV_HWPROBE_EXT_ZALRSC)); enable_feature(Feature::zaamo, test(RISCV_HWPROBE_EXT_ZAAMO)); enable_feature(Feature::zawrs, test(RISCV_HWPROBE_EXT_ZAWRS)); + enable_feature(Feature::zabha, test(RISCV_HWPROBE_EXT_ZABHA)); enable_feature(Feature::zacas, test(RISCV_HWPROBE_EXT_ZACAS)); enable_feature(Feature::ztso, test(RISCV_HWPROBE_EXT_ZTSO)); diff --git a/library/std_detect/src/detect/os/riscv.rs b/library/std_detect/src/detect/os/riscv.rs index dc9a4036d86a1..c6acbd3525bd3 100644 --- a/library/std_detect/src/detect/os/riscv.rs +++ b/library/std_detect/src/detect/os/riscv.rs @@ -90,7 +90,7 @@ pub(crate) fn imply_features(mut value: cache::Initializer) -> cache::Initialize group!(zks == zbkb & zbkc & zbkx & zksed & zksh); group!(zk == zkn & zkr & zkt); - imply!(zacas => zaamo); + imply!(zabha | zacas => zaamo); group!(a == zalrsc & zaamo); group!(b == zba & zbb & zbs); diff --git a/library/std_detect/tests/cpu-detection.rs b/library/std_detect/tests/cpu-detection.rs index 5ad32d83237ce..0c4fa57f2b465 100644 --- a/library/std_detect/tests/cpu-detection.rs +++ b/library/std_detect/tests/cpu-detection.rs @@ -242,6 +242,7 @@ fn riscv_linux() { println!("zalrsc: {}", is_riscv_feature_detected!("zalrsc")); println!("zaamo: {}", is_riscv_feature_detected!("zaamo")); println!("zawrs: {}", is_riscv_feature_detected!("zawrs")); + println!("zabha: {}", is_riscv_feature_detected!("zabha")); println!("zacas: {}", is_riscv_feature_detected!("zacas")); println!("zam: {}", is_riscv_feature_detected!("zam")); println!("ztso: {}", is_riscv_feature_detected!("ztso")); diff --git a/library/test/src/lib.rs b/library/test/src/lib.rs index 7f56d1e362698..1190bb56b97a0 100644 --- a/library/test/src/lib.rs +++ b/library/test/src/lib.rs @@ -89,8 +89,8 @@ use options::RunStrategy; use test_result::*; use time::TestExecTime; -// Process exit code to be used to indicate test failures. -const ERROR_EXIT_CODE: i32 = 101; +/// Process exit code to be used to indicate test failures. +pub const ERROR_EXIT_CODE: i32 = 101; const SECONDARY_TEST_INVOKER_VAR: &str = "__RUST_TEST_INVOKE"; const SECONDARY_TEST_BENCH_BENCHMARKS_VAR: &str = "__RUST_TEST_BENCH_BENCHMARKS"; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 23c9fac486534..b3b889ccf7063 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # standard library we currently track. [toolchain] -channel = "nightly-2025-07-31" +channel = "nightly-2025-08-01" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/scripts/kani-std-analysis/log_parser.py b/scripts/kani-std-analysis/log_parser.py index f9103fa892a0f..32b7c7f9c1c03 100755 --- a/scripts/kani-std-analysis/log_parser.py +++ b/scripts/kani-std-analysis/log_parser.py @@ -137,7 +137,7 @@ def read_kani_list(kani_list_file, scanner_data): } elif len(fn_info.keys()) > 1: crates = list(fn_info.keys()) - target_safenesses = [e['target_safenesses'] + target_safenesses = [e['target_safeness'] for _, e in fn_info.items()] public_targets = [e['public_target'] for _, e in fn_info.items()] @@ -185,7 +185,7 @@ def read_kani_list(kani_list_file, scanner_data): if fn_info is not None: if len(fn_info.keys()) > 1: crates = list(fn_info.keys()) - target_safenesses = [e['target_safenesses'] + target_safenesses = [e['target_safeness'] for _, e in fn_info.items()] public_targets = [e['public_target'] for _, e in fn_info.items()] @@ -236,14 +236,19 @@ def init_entry( if crate is None: print(f'No autoharness info for {harness}', file=sys.stderr) else: - if autoharness_info.get(crate) is None: - print(f'No autoharness info for {crate}', - file=sys.stderr) + if isinstance(crate, list): + crate_list = crate else: - if autoharness_info[crate][harness] != 'ok': - print(f'Unexpected autoharness info for {harness} in {crate}', + crate_list = [crate] + for c in crate_list: + if autoharness_info.get(c) is None: + print(f'No autoharness info for {c}', file=sys.stderr) - del autoharness_info[crate][harness] + else: + if autoharness_info[c][harness] != 'ok': + print(f'Unexpected autoharness info for {harness} in {c}', + file=sys.stderr) + del autoharness_info[c][harness] autoharness_result = 'ok' else: fn = harness_map_entry['function'] @@ -304,7 +309,7 @@ def create_autoharness_result( } elif len(fn_info.keys()) > 1: crates = list(fn_info.keys()) - target_safenesses = [e['target_safenesses'] + target_safenesses = [e['target_safeness'] for _, e in fn_info.items()] public_targets = [e['public_target'] for _, e in fn_info.items()] @@ -505,7 +510,7 @@ def parse_log_lines( del active_threads[thread_id] thread_id = None elif property_match := property_pattern.match(line): - assert thread_id is not None + assert thread_id is not None, f'No known thread id at line {i}' active_threads[thread_id]['n_failed_properties'] = int( property_match.group(1)) active_threads[thread_id]['n_total_properties'] = int( diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 7714a813cc0bb..f774a96f12ca8 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -182,7 +182,7 @@ get_kani_path() { # then update EXPECTED_JSON_FILE_VERSION. get_harnesses() { local kani_path="$1" - "$kani_path" list -Z list $unstable_args ./library --std --format json + "$kani_path" list $unstable_args ./library --std --format json local json_file_version=$(jq -r '.["file-version"]' "$WORK_DIR/kani-list.json") if [[ $json_file_version != $EXPECTED_JSON_FILE_VERSION ]]; then echo "Error: The JSON file-version in kani-list.json does not equal $EXPECTED_JSON_FILE_VERSION" @@ -313,17 +313,17 @@ main() { elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." if [[ "$with_autoharness" == "true" ]]; then - "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format markdown + "$kani_path" autoharness -Z autoharness --list $unstable_args --std ./library --format markdown else - "$kani_path" list -Z list $unstable_args ./library --std --format markdown + "$kani_path" list $unstable_args ./library --std --format markdown fi elif [[ "$run_command" == "metrics" ]]; then local current_dir=$(pwd) echo "Running Kani list command..." if [[ "$with_autoharness" == "true" ]]; then - "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format json + "$kani_path" autoharness -Z autoharness --list $unstable_args --std ./library --format json else - "$kani_path" list -Z list $unstable_args ./library --std --format json + "$kani_path" list $unstable_args ./library --std --format json fi pushd scripts/kani-std-analysis echo "Running Kani's std-analysis command..." diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml index a50a4f9395213..9b03a8a4dacf7 100644 --- a/tool_config/kani-version.toml +++ b/tool_config/kani-version.toml @@ -2,4 +2,4 @@ # incompatible with the verify-std repo. [kani] -commit = "f76e668b5f86daad11e51d78ab10998426da943b" +commit = "53a7a3b516c5cbe504378d4a208d07d49b5aa4ec" diff --git a/verifast-proofs/alloc/collections/linked_list.rs-negative/original/linked_list.rs b/verifast-proofs/alloc/collections/linked_list.rs-negative/original/linked_list.rs index 70c344e49b76a..31dfe73fc7992 100644 --- a/verifast-proofs/alloc/collections/linked_list.rs-negative/original/linked_list.rs +++ b/verifast-proofs/alloc/collections/linked_list.rs-negative/original/linked_list.rs @@ -825,7 +825,7 @@ impl LinkedList { unsafe { self.tail.as_mut().map(|node| &mut node.as_mut().element) } } - /// Adds an element first in the list. + /// Adds an element to the front of the list. /// /// This operation should compute in *O*(1) time. /// @@ -844,11 +844,34 @@ impl LinkedList { /// ``` #[stable(feature = "rust1", since = "1.0.0")] pub fn push_front(&mut self, elt: T) { + let _ = self.push_front_mut(elt); + } + + /// Adds an element to the front of the list, returning a reference to it. + /// + /// This operation should compute in *O*(1) time. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::LinkedList; + /// + /// let mut dl = LinkedList::from([1, 2, 3]); + /// + /// let ptr = dl.push_front_mut(2); + /// *ptr += 4; + /// assert_eq!(dl.front().unwrap(), &6); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[must_use = "if you don't need a reference to the value, use `LinkedList::push_front` instead"] + pub fn push_front_mut(&mut self, elt: T) -> &mut T { let node = Box::new_in(Node::new(elt), &self.alloc); - let node_ptr = NonNull::from(Box::leak(node)); + let mut node_ptr = NonNull::from(Box::leak(node)); // SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked unsafe { self.push_front_node(node_ptr); + &mut node_ptr.as_mut().element } } @@ -876,7 +899,7 @@ impl LinkedList { self.pop_front_node().map(Node::into_element) } - /// Appends an element to the back of a list. + /// Adds an element to the back of the list. /// /// This operation should compute in *O*(1) time. /// @@ -893,11 +916,34 @@ impl LinkedList { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_confusables("push", "append")] pub fn push_back(&mut self, elt: T) { + let _ = self.push_back_mut(elt); + } + + /// Adds an element to the back of the list, returning a reference to it. + /// + /// This operation should compute in *O*(1) time. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::LinkedList; + /// + /// let mut dl = LinkedList::from([1, 2, 3]); + /// + /// let ptr = dl.push_back_mut(2); + /// *ptr += 4; + /// assert_eq!(dl.back().unwrap(), &6); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[must_use = "if you don't need a reference to the value, use `LinkedList::push_back` instead"] + pub fn push_back_mut(&mut self, elt: T) -> &mut T { let node = Box::new_in(Node::new(elt), &self.alloc); - let node_ptr = NonNull::from(Box::leak(node)); + let mut node_ptr = NonNull::from(Box::leak(node)); // SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked unsafe { self.push_back_node(node_ptr); + &mut node_ptr.as_mut().element } } diff --git a/verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs b/verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs index 80eaadddd2e31..cd6c1c552696d 100644 --- a/verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs +++ b/verifast-proofs/alloc/collections/linked_list.rs-negative/verified/linked_list.rs @@ -990,7 +990,7 @@ impl LinkedList { unsafe { self.tail.as_mut().map(|node| &mut node.as_mut().element) } } - /// Adds an element first in the list. + /// Adds an element to the front of the list. /// /// This operation should compute in *O*(1) time. /// @@ -1009,11 +1009,34 @@ impl LinkedList { /// ``` #[stable(feature = "rust1", since = "1.0.0")] pub fn push_front(&mut self, elt: T) { + let _ = self.push_front_mut(elt); + } + + /// Adds an element to the front of the list, returning a reference to it. + /// + /// This operation should compute in *O*(1) time. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::LinkedList; + /// + /// let mut dl = LinkedList::from([1, 2, 3]); + /// + /// let ptr = dl.push_front_mut(2); + /// *ptr += 4; + /// assert_eq!(dl.front().unwrap(), &6); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[must_use = "if you don't need a reference to the value, use `LinkedList::push_front` instead"] + pub fn push_front_mut(&mut self, elt: T) -> &mut T { let node = Box::new_in(Node::new(elt), &self.alloc); - let node_ptr = NonNull::from(Box::leak(node)); + let mut node_ptr = NonNull::from(Box::leak(node)); // SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked unsafe { self.push_front_node(node_ptr); + &mut node_ptr.as_mut().element } } @@ -1041,7 +1064,7 @@ impl LinkedList { self.pop_front_node().map(Node::into_element) } - /// Appends an element to the back of a list. + /// Adds an element to the back of the list. /// /// This operation should compute in *O*(1) time. /// @@ -1058,11 +1081,34 @@ impl LinkedList { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_confusables("push", "append")] pub fn push_back(&mut self, elt: T) { + let _ = self.push_back_mut(elt); + } + + /// Adds an element to the back of the list, returning a reference to it. + /// + /// This operation should compute in *O*(1) time. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::LinkedList; + /// + /// let mut dl = LinkedList::from([1, 2, 3]); + /// + /// let ptr = dl.push_back_mut(2); + /// *ptr += 4; + /// assert_eq!(dl.back().unwrap(), &6); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[must_use = "if you don't need a reference to the value, use `LinkedList::push_back` instead"] + pub fn push_back_mut(&mut self, elt: T) -> &mut T { let node = Box::new_in(Node::new(elt), &self.alloc); - let node_ptr = NonNull::from(Box::leak(node)); + let mut node_ptr = NonNull::from(Box::leak(node)); // SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked unsafe { self.push_back_node(node_ptr); + &mut node_ptr.as_mut().element } } diff --git a/verifast-proofs/alloc/collections/linked_list.rs/original/linked_list.rs b/verifast-proofs/alloc/collections/linked_list.rs/original/linked_list.rs index 70c344e49b76a..31dfe73fc7992 100644 --- a/verifast-proofs/alloc/collections/linked_list.rs/original/linked_list.rs +++ b/verifast-proofs/alloc/collections/linked_list.rs/original/linked_list.rs @@ -825,7 +825,7 @@ impl LinkedList { unsafe { self.tail.as_mut().map(|node| &mut node.as_mut().element) } } - /// Adds an element first in the list. + /// Adds an element to the front of the list. /// /// This operation should compute in *O*(1) time. /// @@ -844,11 +844,34 @@ impl LinkedList { /// ``` #[stable(feature = "rust1", since = "1.0.0")] pub fn push_front(&mut self, elt: T) { + let _ = self.push_front_mut(elt); + } + + /// Adds an element to the front of the list, returning a reference to it. + /// + /// This operation should compute in *O*(1) time. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::LinkedList; + /// + /// let mut dl = LinkedList::from([1, 2, 3]); + /// + /// let ptr = dl.push_front_mut(2); + /// *ptr += 4; + /// assert_eq!(dl.front().unwrap(), &6); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[must_use = "if you don't need a reference to the value, use `LinkedList::push_front` instead"] + pub fn push_front_mut(&mut self, elt: T) -> &mut T { let node = Box::new_in(Node::new(elt), &self.alloc); - let node_ptr = NonNull::from(Box::leak(node)); + let mut node_ptr = NonNull::from(Box::leak(node)); // SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked unsafe { self.push_front_node(node_ptr); + &mut node_ptr.as_mut().element } } @@ -876,7 +899,7 @@ impl LinkedList { self.pop_front_node().map(Node::into_element) } - /// Appends an element to the back of a list. + /// Adds an element to the back of the list. /// /// This operation should compute in *O*(1) time. /// @@ -893,11 +916,34 @@ impl LinkedList { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_confusables("push", "append")] pub fn push_back(&mut self, elt: T) { + let _ = self.push_back_mut(elt); + } + + /// Adds an element to the back of the list, returning a reference to it. + /// + /// This operation should compute in *O*(1) time. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::LinkedList; + /// + /// let mut dl = LinkedList::from([1, 2, 3]); + /// + /// let ptr = dl.push_back_mut(2); + /// *ptr += 4; + /// assert_eq!(dl.back().unwrap(), &6); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[must_use = "if you don't need a reference to the value, use `LinkedList::push_back` instead"] + pub fn push_back_mut(&mut self, elt: T) -> &mut T { let node = Box::new_in(Node::new(elt), &self.alloc); - let node_ptr = NonNull::from(Box::leak(node)); + let mut node_ptr = NonNull::from(Box::leak(node)); // SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked unsafe { self.push_back_node(node_ptr); + &mut node_ptr.as_mut().element } } diff --git a/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs b/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs index 8613e9b456571..286e12d9bf40f 100644 --- a/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs +++ b/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs @@ -990,7 +990,7 @@ impl LinkedList { unsafe { self.tail.as_mut().map(|node| &mut node.as_mut().element) } } - /// Adds an element first in the list. + /// Adds an element to the front of the list. /// /// This operation should compute in *O*(1) time. /// @@ -1009,11 +1009,34 @@ impl LinkedList { /// ``` #[stable(feature = "rust1", since = "1.0.0")] pub fn push_front(&mut self, elt: T) { + let _ = self.push_front_mut(elt); + } + + /// Adds an element to the front of the list, returning a reference to it. + /// + /// This operation should compute in *O*(1) time. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::LinkedList; + /// + /// let mut dl = LinkedList::from([1, 2, 3]); + /// + /// let ptr = dl.push_front_mut(2); + /// *ptr += 4; + /// assert_eq!(dl.front().unwrap(), &6); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[must_use = "if you don't need a reference to the value, use `LinkedList::push_front` instead"] + pub fn push_front_mut(&mut self, elt: T) -> &mut T { let node = Box::new_in(Node::new(elt), &self.alloc); - let node_ptr = NonNull::from(Box::leak(node)); + let mut node_ptr = NonNull::from(Box::leak(node)); // SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked unsafe { self.push_front_node(node_ptr); + &mut node_ptr.as_mut().element } } @@ -1041,7 +1064,7 @@ impl LinkedList { self.pop_front_node().map(Node::into_element) } - /// Appends an element to the back of a list. + /// Adds an element to the back of the list. /// /// This operation should compute in *O*(1) time. /// @@ -1058,11 +1081,34 @@ impl LinkedList { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_confusables("push", "append")] pub fn push_back(&mut self, elt: T) { + let _ = self.push_back_mut(elt); + } + + /// Adds an element to the back of the list, returning a reference to it. + /// + /// This operation should compute in *O*(1) time. + /// + /// # Examples + /// + /// ``` + /// #![feature(push_mut)] + /// use std::collections::LinkedList; + /// + /// let mut dl = LinkedList::from([1, 2, 3]); + /// + /// let ptr = dl.push_back_mut(2); + /// *ptr += 4; + /// assert_eq!(dl.back().unwrap(), &6); + /// ``` + #[unstable(feature = "push_mut", issue = "135974")] + #[must_use = "if you don't need a reference to the value, use `LinkedList::push_back` instead"] + pub fn push_back_mut(&mut self, elt: T) -> &mut T { let node = Box::new_in(Node::new(elt), &self.alloc); - let node_ptr = NonNull::from(Box::leak(node)); + let mut node_ptr = NonNull::from(Box::leak(node)); // SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked unsafe { self.push_back_node(node_ptr); + &mut node_ptr.as_mut().element } }