Skip to content

Commit fa16327

Browse files
authored
Merge branch 'main' into verifast-raw-vec
2 parents feee434 + 8e9f2b7 commit fa16327

File tree

34 files changed

+582
-71
lines changed

34 files changed

+582
-71
lines changed

library/alloc/src/collections/linked_list.rs

Lines changed: 50 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -825,7 +825,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
825825
unsafe { self.tail.as_mut().map(|node| &mut node.as_mut().element) }
826826
}
827827

828-
/// Adds an element first in the list.
828+
/// Adds an element to the front of the list.
829829
///
830830
/// This operation should compute in *O*(1) time.
831831
///
@@ -844,11 +844,34 @@ impl<T, A: Allocator> LinkedList<T, A> {
844844
/// ```
845845
#[stable(feature = "rust1", since = "1.0.0")]
846846
pub fn push_front(&mut self, elt: T) {
847+
let _ = self.push_front_mut(elt);
848+
}
849+
850+
/// Adds an element to the front of the list, returning a reference to it.
851+
///
852+
/// This operation should compute in *O*(1) time.
853+
///
854+
/// # Examples
855+
///
856+
/// ```
857+
/// #![feature(push_mut)]
858+
/// use std::collections::LinkedList;
859+
///
860+
/// let mut dl = LinkedList::from([1, 2, 3]);
861+
///
862+
/// let ptr = dl.push_front_mut(2);
863+
/// *ptr += 4;
864+
/// assert_eq!(dl.front().unwrap(), &6);
865+
/// ```
866+
#[unstable(feature = "push_mut", issue = "135974")]
867+
#[must_use = "if you don't need a reference to the value, use `LinkedList::push_front` instead"]
868+
pub fn push_front_mut(&mut self, elt: T) -> &mut T {
847869
let node = Box::new_in(Node::new(elt), &self.alloc);
848-
let node_ptr = NonNull::from(Box::leak(node));
870+
let mut node_ptr = NonNull::from(Box::leak(node));
849871
// SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked
850872
unsafe {
851873
self.push_front_node(node_ptr);
874+
&mut node_ptr.as_mut().element
852875
}
853876
}
854877

@@ -876,7 +899,7 @@ impl<T, A: Allocator> LinkedList<T, A> {
876899
self.pop_front_node().map(Node::into_element)
877900
}
878901

879-
/// Appends an element to the back of a list.
902+
/// Adds an element to the back of the list.
880903
///
881904
/// This operation should compute in *O*(1) time.
882905
///
@@ -893,11 +916,34 @@ impl<T, A: Allocator> LinkedList<T, A> {
893916
#[stable(feature = "rust1", since = "1.0.0")]
894917
#[rustc_confusables("push", "append")]
895918
pub fn push_back(&mut self, elt: T) {
919+
let _ = self.push_back_mut(elt);
920+
}
921+
922+
/// Adds an element to the back of the list, returning a reference to it.
923+
///
924+
/// This operation should compute in *O*(1) time.
925+
///
926+
/// # Examples
927+
///
928+
/// ```
929+
/// #![feature(push_mut)]
930+
/// use std::collections::LinkedList;
931+
///
932+
/// let mut dl = LinkedList::from([1, 2, 3]);
933+
///
934+
/// let ptr = dl.push_back_mut(2);
935+
/// *ptr += 4;
936+
/// assert_eq!(dl.back().unwrap(), &6);
937+
/// ```
938+
#[unstable(feature = "push_mut", issue = "135974")]
939+
#[must_use = "if you don't need a reference to the value, use `LinkedList::push_back` instead"]
940+
pub fn push_back_mut(&mut self, elt: T) -> &mut T {
896941
let node = Box::new_in(Node::new(elt), &self.alloc);
897-
let node_ptr = NonNull::from(Box::leak(node));
942+
let mut node_ptr = NonNull::from(Box::leak(node));
898943
// SAFETY: node_ptr is a unique pointer to a node we boxed with self.alloc and leaked
899944
unsafe {
900945
self.push_back_node(node_ptr);
946+
&mut node_ptr.as_mut().element
901947
}
902948
}
903949

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,12 @@
11
use core::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
2+
#[cfg(kani)]
3+
use core::kani;
24
use core::num::NonZero;
35
use core::ops::Try;
46
use core::{fmt, mem, slice};
57

8+
use safety::requires;
9+
610
/// An iterator over the elements of a `VecDeque`.
711
///
812
/// This `struct` is created by the [`iter`] method on [`super::VecDeque`]. See its
@@ -144,6 +148,8 @@ impl<'a, T> Iterator for Iter<'a, T> {
144148
}
145149

146150
#[inline]
151+
#[requires(idx < self.len())]
152+
#[cfg_attr(kani, kani::modifies(self))]
147153
unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
148154
// Safety: The TrustedRandomAccess contract requires that callers only pass an index
149155
// that is in bounds.

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,12 @@
11
use core::iter::{FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce};
2+
#[cfg(kani)]
3+
use core::kani;
24
use core::num::NonZero;
35
use core::ops::Try;
46
use core::{fmt, mem, slice};
57

8+
use safety::requires;
9+
610
/// A mutable iterator over the elements of a `VecDeque`.
711
///
812
/// This `struct` is created by the [`iter_mut`] method on [`super::VecDeque`]. See its
@@ -208,6 +212,8 @@ impl<'a, T> Iterator for IterMut<'a, T> {
208212
}
209213

210214
#[inline]
215+
#[requires(idx < self.len())]
216+
#[cfg_attr(kani, kani::modifies(self))]
211217
unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
212218
// Safety: The TrustedRandomAccess contract requires that callers only pass an index
213219
// that is in bounds.

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

Lines changed: 85 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -185,11 +185,16 @@ impl<T, A: Allocator> VecDeque<T, A> {
185185
unsafe { ptr::read(self.ptr().add(off)) }
186186
}
187187

188-
/// Writes an element into the buffer, moving it.
188+
/// Writes an element into the buffer, moving it and returning a pointer to it.
189+
/// # Safety
190+
///
191+
/// May only be called if `off < self.capacity()`.
189192
#[inline]
190-
unsafe fn buffer_write(&mut self, off: usize, value: T) {
193+
unsafe fn buffer_write(&mut self, off: usize, value: T) -> &mut T {
191194
unsafe {
192-
ptr::write(self.ptr().add(off), value);
195+
let ptr = self.ptr().add(off);
196+
ptr::write(ptr, value);
197+
&mut *ptr
193198
}
194199
}
195200

@@ -1891,16 +1896,34 @@ impl<T, A: Allocator> VecDeque<T, A> {
18911896
#[stable(feature = "rust1", since = "1.0.0")]
18921897
#[track_caller]
18931898
pub fn push_front(&mut self, value: T) {
1899+
let _ = self.push_front_mut(value);
1900+
}
1901+
1902+
/// Prepends an element to the deque, returning a reference to it.
1903+
///
1904+
/// # Examples
1905+
///
1906+
/// ```
1907+
/// #![feature(push_mut)]
1908+
/// use std::collections::VecDeque;
1909+
///
1910+
/// let mut d = VecDeque::from([1, 2, 3]);
1911+
/// let x = d.push_front_mut(8);
1912+
/// *x -= 1;
1913+
/// assert_eq!(d.front(), Some(&7));
1914+
/// ```
1915+
#[unstable(feature = "push_mut", issue = "135974")]
1916+
#[track_caller]
1917+
#[must_use = "if you don't need a reference to the value, use `VecDeque::push_front` instead"]
1918+
pub fn push_front_mut(&mut self, value: T) -> &mut T {
18941919
if self.is_full() {
18951920
self.grow();
18961921
}
18971922

18981923
self.head = self.wrap_sub(self.head, 1);
18991924
self.len += 1;
1900-
1901-
unsafe {
1902-
self.buffer_write(self.head, value);
1903-
}
1925+
// SAFETY: We know that self.head is within range of the deque.
1926+
unsafe { self.buffer_write(self.head, value) }
19041927
}
19051928

19061929
/// Appends an element to the back of the deque.
@@ -1919,12 +1942,33 @@ impl<T, A: Allocator> VecDeque<T, A> {
19191942
#[rustc_confusables("push", "put", "append")]
19201943
#[track_caller]
19211944
pub fn push_back(&mut self, value: T) {
1945+
let _ = self.push_back_mut(value);
1946+
}
1947+
1948+
/// Appends an element to the back of the deque, returning a reference to it.
1949+
///
1950+
/// # Examples
1951+
///
1952+
/// ```
1953+
/// #![feature(push_mut)]
1954+
/// use std::collections::VecDeque;
1955+
///
1956+
/// let mut d = VecDeque::from([1, 2, 3]);
1957+
/// let x = d.push_back_mut(9);
1958+
/// *x += 1;
1959+
/// assert_eq!(d.back(), Some(&10));
1960+
/// ```
1961+
#[unstable(feature = "push_mut", issue = "135974")]
1962+
#[track_caller]
1963+
#[must_use = "if you don't need a reference to the value, use `VecDeque::push_back` instead"]
1964+
pub fn push_back_mut(&mut self, value: T) -> &mut T {
19221965
if self.is_full() {
19231966
self.grow();
19241967
}
19251968

1926-
unsafe { self.buffer_write(self.to_physical_idx(self.len), value) }
1969+
let len = self.len;
19271970
self.len += 1;
1971+
unsafe { self.buffer_write(self.to_physical_idx(len), value) }
19281972
}
19291973

19301974
#[inline]
@@ -2010,7 +2054,7 @@ impl<T, A: Allocator> VecDeque<T, A> {
20102054
///
20112055
/// # Panics
20122056
///
2013-
/// Panics if `index` is strictly greater than deque's length
2057+
/// Panics if `index` is strictly greater than the deque's length.
20142058
///
20152059
/// # Examples
20162060
///
@@ -2032,7 +2076,37 @@ impl<T, A: Allocator> VecDeque<T, A> {
20322076
#[stable(feature = "deque_extras_15", since = "1.5.0")]
20332077
#[track_caller]
20342078
pub fn insert(&mut self, index: usize, value: T) {
2079+
let _ = self.insert_mut(index, value);
2080+
}
2081+
2082+
/// Inserts an element at `index` within the deque, shifting all elements
2083+
/// with indices greater than or equal to `index` towards the back, and
2084+
/// returning a reference to it.
2085+
///
2086+
/// Element at index 0 is the front of the queue.
2087+
///
2088+
/// # Panics
2089+
///
2090+
/// Panics if `index` is strictly greater than the deque's length.
2091+
///
2092+
/// # Examples
2093+
///
2094+
/// ```
2095+
/// #![feature(push_mut)]
2096+
/// use std::collections::VecDeque;
2097+
///
2098+
/// let mut vec_deque = VecDeque::from([1, 2, 3]);
2099+
///
2100+
/// let x = vec_deque.insert_mut(1, 5);
2101+
/// *x += 7;
2102+
/// assert_eq!(vec_deque, &[1, 12, 2, 3]);
2103+
/// ```
2104+
#[unstable(feature = "push_mut", issue = "135974")]
2105+
#[track_caller]
2106+
#[must_use = "if you don't need a reference to the value, use `VecDeque::insert` instead"]
2107+
pub fn insert_mut(&mut self, index: usize, value: T) -> &mut T {
20352108
assert!(index <= self.len(), "index out of bounds");
2109+
20362110
if self.is_full() {
20372111
self.grow();
20382112
}
@@ -2045,16 +2119,16 @@ impl<T, A: Allocator> VecDeque<T, A> {
20452119
unsafe {
20462120
// see `remove()` for explanation why this wrap_copy() call is safe.
20472121
self.wrap_copy(self.to_physical_idx(index), self.to_physical_idx(index + 1), k);
2048-
self.buffer_write(self.to_physical_idx(index), value);
20492122
self.len += 1;
2123+
self.buffer_write(self.to_physical_idx(index), value)
20502124
}
20512125
} else {
20522126
let old_head = self.head;
20532127
self.head = self.wrap_sub(self.head, 1);
20542128
unsafe {
20552129
self.wrap_copy(old_head, self.head, index);
2056-
self.buffer_write(self.to_physical_idx(index), value);
20572130
self.len += 1;
2131+
self.buffer_write(self.to_physical_idx(index), value)
20582132
}
20592133
}
20602134
}

library/alloc/src/vec/into_iter.rs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ use core::iter::{
22
FusedIterator, InPlaceIterable, SourceIter, TrustedFused, TrustedLen,
33
TrustedRandomAccessNoCoerce,
44
};
5+
#[cfg(kani)]
6+
use core::kani;
57
use core::marker::PhantomData;
68
use core::mem::{ManuallyDrop, MaybeUninit, SizedTypeProperties};
79
use core::num::NonZero;
@@ -11,6 +13,8 @@ use core::ptr::{self, NonNull};
1113
use core::slice::{self};
1214
use core::{array, fmt};
1315

16+
use safety::requires;
17+
1418
#[cfg(not(no_global_oom_handling))]
1519
use super::AsVecIntoIter;
1620
use crate::alloc::{Allocator, Global};
@@ -354,6 +358,8 @@ impl<T, A: Allocator> Iterator for IntoIter<T, A> {
354358
R::from_output(accum)
355359
}
356360

361+
#[requires(i < self.len())]
362+
#[cfg_attr(kani, kani::modifies(self))]
357363
unsafe fn __iterator_get_unchecked(&mut self, i: usize) -> Self::Item
358364
where
359365
Self: TrustedRandomAccessNoCoerce,

0 commit comments

Comments
 (0)