Skip to content

Commit b12bb9b

Browse files
committed
Merge branch 'main' into verifast-linked-list
Also upgrades VeriFast to 25.07.
2 parents e9fd0e4 + 517e11e commit b12bb9b

File tree

55 files changed

+1140
-278
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

55 files changed

+1140
-278
lines changed

.github/workflows/verifast-negative.yml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,16 +30,16 @@ jobs:
3030
- name: Install VeriFast
3131
run: |
3232
cd ~
33-
curl -OL https://github.com/verifast/verifast/releases/download/25.06/verifast-25.06-linux.tar.gz
34-
# https://github.com/verifast/verifast/attestations/7473259
35-
echo '7081408d99853620a79fbfc3767f367d6f6ccfdaf26a63b1f30a382489aacb5a verifast-25.06-linux.tar.gz' | shasum -a 256 -c
36-
tar xf verifast-25.06-linux.tar.gz
33+
curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
34+
# https://github.com/verifast/verifast/attestations/8998468
35+
echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b verifast-25.07-linux.tar.gz' | shasum -a 256 -c
36+
tar xf verifast-25.07-linux.tar.gz
3737
3838
- name: Install the Rust toolchain used by VeriFast
39-
run: rustup toolchain install nightly-2024-11-23
39+
run: rustup toolchain install nightly-2025-04-09
4040

4141
- name: Run VeriFast Verification
4242
run: |
43-
export PATH=~/verifast-25.06/bin:$PATH
43+
export PATH=~/verifast-25.07/bin:$PATH
4444
cd verifast-proofs
4545
bash check-verifast-proofs-negative.sh

.github/workflows/verifast.yml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -27,17 +27,17 @@ jobs:
2727
- name: Install VeriFast
2828
run: |
2929
cd ~
30-
curl -OL https://github.com/verifast/verifast/releases/download/25.06/verifast-25.06-linux.tar.gz
31-
# https://github.com/verifast/verifast/attestations/7473259
32-
echo '7081408d99853620a79fbfc3767f367d6f6ccfdaf26a63b1f30a382489aacb5a verifast-25.06-linux.tar.gz' | shasum -a 256 -c
33-
tar xf verifast-25.06-linux.tar.gz
30+
curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
31+
# https://github.com/verifast/verifast/attestations/8998468
32+
echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b verifast-25.07-linux.tar.gz' | shasum -a 256 -c
33+
tar xf verifast-25.07-linux.tar.gz
3434
3535
- name: Install the Rust toolchain used by VeriFast
36-
run: rustup toolchain install nightly-2024-11-23
36+
run: rustup toolchain install nightly-2025-04-09
3737

3838
- name: Run VeriFast Verification
3939
run: |
40-
export PATH=~/verifast-25.06/bin:$PATH
40+
export PATH=~/verifast-25.07/bin:$PATH
4141
cd verifast-proofs
4242
bash check-verifast-proofs.sh
4343

library/Cargo.lock

Lines changed: 9 additions & 14 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

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/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
}

0 commit comments

Comments
 (0)