From f933e70d5af2c0bb4d8e8c35556ac5408929c660 Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 11 Dec 2023 23:59:59 -0600 Subject: [PATCH 1/2] crux-mir: Avoid pointer arithmetic in vec IntoIter --- crux-mir/lib/Patches.md | 5 +++++ crux-mir/lib/alloc/src/vec/into_iter.rs | 17 ++++++++++++----- crux-mir/lib/alloc/src/vec/mod.rs | 1 + 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/crux-mir/lib/Patches.md b/crux-mir/lib/Patches.md index 4a86a00b5..a7abc99be 100644 --- a/crux-mir/lib/Patches.md +++ b/crux-mir/lib/Patches.md @@ -57,6 +57,11 @@ identify all of the code that was changed in each patch. in sync with `ptr` and `end`, and avoids the need for pointer arithmetic. +* Avoid pointer arithmetic in `vec` `IntoIter` (last applied: December 11, 2023) + + The same problem as above exists for `vec::into_iter::IntoIter::size_hint`, + and we fix it in the same way by adding a `len` field to `IntoIter`. + * Implement `str::as_bytes` via `crucible_identity_transmute` (last applied: May 16, 2023) This is necessary to avoid a gnarly use of `transmute`. diff --git a/crux-mir/lib/alloc/src/vec/into_iter.rs b/crux-mir/lib/alloc/src/vec/into_iter.rs index 37966007e..58cf07a5e 100644 --- a/crux-mir/lib/alloc/src/vec/into_iter.rs +++ b/crux-mir/lib/alloc/src/vec/into_iter.rs @@ -43,6 +43,7 @@ pub struct IntoIter< pub(super) end: *const T, // If T is a ZST, this is actually ptr+len. This encoding is picked so that // ptr == end is a quick test for the Iterator being empty, that works // for both ZST and non-ZST. + pub(super) len: usize, } #[stable(feature = "vec_intoiter_debug", since = "1.13.0")] @@ -124,6 +125,7 @@ impl IntoIter { self.buf = unsafe { NonNull::new_unchecked(RawVec::NEW.ptr()) }; self.ptr = self.buf.as_ptr(); self.end = self.buf.as_ptr(); + self.len = 0; // Dropping the remaining elements can panic, so this needs to be // done only after updating the other fields. @@ -137,6 +139,7 @@ impl IntoIter { // For th ZST case, it is crucial that we mutate `end` here, not `ptr`. // `ptr` must stay aligned, while `end` may be unaligned. self.end = self.ptr; + self.len = 0; } #[cfg(not(no_global_oom_handling))] @@ -191,12 +194,14 @@ impl Iterator for IntoIter { // `ptr` has to stay where it is to remain aligned, so we reduce the length by 1 by // reducing the `end`. self.end = self.end.wrapping_byte_sub(1); + self.len -= 1; // Make up a value of this ZST. Some(unsafe { mem::zeroed() }) } else { let old = self.ptr; self.ptr = unsafe { self.ptr.add(1) }; + self.len -= 1; Some(unsafe { ptr::read(old) }) } @@ -204,11 +209,7 @@ impl Iterator for IntoIter { #[inline] fn size_hint(&self) -> (usize, Option) { - let exact = if T::IS_ZST { - self.end.addr().wrapping_sub(self.ptr.addr()) - } else { - unsafe { self.end.sub_ptr(self.ptr) } - }; + let exact = self.len; (exact, Some(exact)) } @@ -223,6 +224,7 @@ impl Iterator for IntoIter { // SAFETY: the min() above ensures that step_size is in bounds self.ptr = unsafe { self.ptr.add(step_size) }; } + self.len -= step_size; // SAFETY: the min() above ensures that step_size is in bounds unsafe { ptr::drop_in_place(to_drop); @@ -252,6 +254,7 @@ impl Iterator for IntoIter { } self.end = self.end.wrapping_byte_sub(N); + self.len -= N; // Safety: ditto return Ok(unsafe { raw_ary.transpose().assume_init() }); } @@ -271,6 +274,7 @@ impl Iterator for IntoIter { return unsafe { ptr::copy_nonoverlapping(self.ptr, raw_ary.as_mut_ptr() as *mut T, N); self.ptr = self.ptr.add(N); + self.len -= N; Ok(raw_ary.transpose().assume_init()) }; } @@ -302,11 +306,13 @@ impl DoubleEndedIterator for IntoIter { } else if T::IS_ZST { // See above for why 'ptr.offset' isn't used self.end = self.end.wrapping_byte_sub(1); + self.len -= 1; // Make up a value of this ZST. Some(unsafe { mem::zeroed() }) } else { self.end = unsafe { self.end.sub(1) }; + self.len -= 1; Some(unsafe { ptr::read(self.end) }) } @@ -322,6 +328,7 @@ impl DoubleEndedIterator for IntoIter { // SAFETY: same as for advance_by() self.end = unsafe { self.end.sub(step_size) }; } + self.len -= step_size; let to_drop = ptr::slice_from_raw_parts_mut(self.end as *mut T, step_size); // SAFETY: same as for advance_by() unsafe { diff --git a/crux-mir/lib/alloc/src/vec/mod.rs b/crux-mir/lib/alloc/src/vec/mod.rs index 3e1f1dd50..066743b99 100644 --- a/crux-mir/lib/alloc/src/vec/mod.rs +++ b/crux-mir/lib/alloc/src/vec/mod.rs @@ -2794,6 +2794,7 @@ impl IntoIterator for Vec { alloc, ptr: begin, end, + len: me.len(), } } } From c8318d0b94a2ae9eb6a4f7f005873d1cc0a70975 Mon Sep 17 00:00:00 2001 From: Bretton Date: Wed, 20 Dec 2023 05:42:34 +0800 Subject: [PATCH 2/2] crux-mir: Add test for vec into_iter --- crux-mir/test/conc_eval/vec/into_iter.rs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 crux-mir/test/conc_eval/vec/into_iter.rs diff --git a/crux-mir/test/conc_eval/vec/into_iter.rs b/crux-mir/test/conc_eval/vec/into_iter.rs new file mode 100644 index 000000000..d46274149 --- /dev/null +++ b/crux-mir/test/conc_eval/vec/into_iter.rs @@ -0,0 +1,20 @@ +#![cfg_attr(not(with_main), no_std)] +// Test iterator for 0-length vec + +#[cfg(not(with_main))] extern crate std; +#[cfg(not(with_main))] use std::vec; + +pub fn f(count: u32) -> u32 { + let mut v1 = vec![]; + (0..count).for_each(|i| v1.push(i)); + let mut sum = 0; + for i in v1 { + sum += i; + } + sum +} + +pub static ARG: u32 = 0; + +#[cfg(with_main)] pub fn main() { println!("{:?}", f(ARG)); } +#[cfg(not(with_main))] #[cfg_attr(crux, crux::test)] fn crux_test() -> u32 { f(ARG) }