Skip to content

Commit 1317b89

Browse files
btjbtj
authored
Update RawVec proof (#489)
Updates the VeriFast proofs By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 793ad85 commit 1317b89

File tree

3 files changed

+8
-86
lines changed

3 files changed

+8
-86
lines changed

‎verifast-proofs/alloc/raw_vec/mod.rs/original/raw_vec.rs

Lines changed: 3 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ impl RawVecInner<Global> {
155155
}
156156

157157
// Tiny Vecs are dumb. Skip to:
158-
// - 8 if the element size is 1, because any heap allocators is likely
158+
// - 8 if the element size is 1, because any heap allocator is likely
159159
// to round up a request of less than 8 bytes to at least 8 bytes.
160160
// - 4 if elements are moderate-sized (<= 1 KiB).
161161
// - 1 otherwise, to avoid wasting too much space for very short Vecs.
@@ -468,10 +468,6 @@ impl<A: Allocator> RawVecInner<A> {
468468
return Ok(Self::new_in(alloc, elem_layout.alignment()));
469469
}
470470

471-
if let Err(err) = alloc_guard(layout.size()) {
472-
return Err(err);
473-
}
474-
475471
let result = match init {
476472
AllocInit::Uninitialized => alloc.allocate(layout),
477473
#[cfg(not(no_global_oom_handling))]
@@ -662,7 +658,7 @@ impl<A: Allocator> RawVecInner<A> {
662658
let new_layout = layout_array(cap, elem_layout)?;
663659

664660
let ptr = finish_grow(new_layout, self.current_memory(elem_layout), &mut self.alloc)?;
665-
// SAFETY: finish_grow would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
661+
// SAFETY: layout_array would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
666662

667663
unsafe { self.set_ptr_and_cap(ptr, cap) };
668664
Ok(())
@@ -684,7 +680,7 @@ impl<A: Allocator> RawVecInner<A> {
684680
let new_layout = layout_array(cap, elem_layout)?;
685681

686682
let ptr = finish_grow(new_layout, self.current_memory(elem_layout), &mut self.alloc)?;
687-
// SAFETY: finish_grow would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
683+
// SAFETY: layout_array would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
688684
unsafe {
689685
self.set_ptr_and_cap(ptr, cap);
690686
}
@@ -771,8 +767,6 @@ fn finish_grow<A>(
771767
where
772768
A: Allocator,
773769
{
774-
alloc_guard(new_layout.size())?;
775-
776770
let memory = if let Some((ptr, old_layout)) = current_memory {
777771
debug_assert_eq!(old_layout.align(), new_layout.align());
778772
unsafe {
@@ -799,23 +793,6 @@ fn handle_error(e: TryReserveError) -> ! {
799793
}
800794
}
801795

802-
// We need to guarantee the following:
803-
// * We don't ever allocate `> isize::MAX` byte-size objects.
804-
// * We don't overflow `usize::MAX` and actually allocate too little.
805-
//
806-
// On 64-bit we just need to check for overflow since trying to allocate
807-
// `> isize::MAX` bytes will surely fail. On 32-bit and 16-bit we need to add
808-
// an extra guard for this in case we're running on a platform which can use
809-
// all 4GB in user-space, e.g., PAE or x32.
810-
#[inline]
811-
fn alloc_guard(alloc_size: usize) -> Result<(), TryReserveError> {
812-
if usize::BITS < 64 && alloc_size > isize::MAX as usize {
813-
Err(CapacityOverflow.into())
814-
} else {
815-
Ok(())
816-
}
817-
}
818-
819796
#[inline]
820797
fn layout_array(cap: usize, elem_layout: Layout) -> Result<Layout, TryReserveError> {
821798
elem_layout.repeat(cap).map(|(layout, _pad)| layout).map_err(|_| CapacityOverflow.into())

‎verifast-proofs/alloc/raw_vec/mod.rs/verified/raw_vec.rs

Lines changed: 2 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -1134,11 +1134,6 @@ impl<A: Allocator> RawVecInner<A> {
11341134
return Ok(r);
11351135
}
11361136

1137-
if let Err(err) = alloc_guard(layout.size()) {
1138-
//@ std::alloc::Allocator_to_own(alloc);
1139-
return Err(err);
1140-
}
1141-
11421137
let result = match init {
11431138
AllocInit::Uninitialized => {
11441139
let r;
@@ -1638,7 +1633,7 @@ impl<A: Allocator> RawVecInner<A> {
16381633
core::ops::FromResidual::from_residual(residual)
16391634
}
16401635
core::ops::ControlFlow::Continue(ptr) => {
1641-
// SAFETY: finish_grow would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
1636+
// SAFETY: layout_array would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
16421637
unsafe {
16431638
self.set_ptr_and_cap(ptr, cap);
16441639
//@ let self1 = *self;
@@ -1737,7 +1732,7 @@ impl<A: Allocator> RawVecInner<A> {
17371732
core::ops::FromResidual::from_residual(residual)
17381733
}
17391734
core::ops::ControlFlow::Continue(ptr) => {
1740-
// SAFETY: finish_grow would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
1735+
// SAFETY: layout_array would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
17411736
unsafe {
17421737
//@ assert Layout::size_(new_layout) == Layout::size_(elem_layout) * cap;
17431738
//@ mul_mono_l(1, Layout::size_(elem_layout), cap);
@@ -2086,33 +2081,6 @@ fn handle_error(e: TryReserveError) -> !
20862081
}
20872082
}
20882083

2089-
// We need to guarantee the following:
2090-
// * We don't ever allocate `> isize::MAX` byte-size objects.
2091-
// * We don't overflow `usize::MAX` and actually allocate too little.
2092-
//
2093-
// On 64-bit we just need to check for overflow since trying to allocate
2094-
// `> isize::MAX` bytes will surely fail. On 32-bit and 16-bit we need to add
2095-
// an extra guard for this in case we're running on a platform which can use
2096-
// all 4GB in user-space, e.g., PAE or x32.
2097-
#[inline]
2098-
fn alloc_guard(alloc_size: usize) -> Result<(), TryReserveError>
2099-
//@ req thread_token(currentThread);
2100-
/*@
2101-
ens thread_token(currentThread) &*&
2102-
match result {
2103-
Result::Ok(dummy) => true,
2104-
Result::Err(err) => <std::collections::TryReserveError>.own(currentThread, err)
2105-
};
2106-
@*/
2107-
//@ safety_proof { assume(false); }
2108-
{
2109-
if usize::BITS < 64 && alloc_size > isize::MAX as usize { //~allow_dead_code
2110-
Err(CapacityOverflow.into()) //~allow_dead_code
2111-
} else {
2112-
Ok(())
2113-
}
2114-
}
2115-
21162084
#[inline]
21172085
fn layout_array(cap: usize, elem_layout: Layout) -> Result<Layout, TryReserveError>
21182086
//@ req thread_token(currentThread) &*& Layout::size_(elem_layout) % Layout::align_(elem_layout) == 0;

‎verifast-proofs/alloc/raw_vec/mod.rs/with-directives/raw_vec.rs

Lines changed: 3 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ impl RawVecInner<Global> {
155155
}
156156

157157
// Tiny Vecs are dumb. Skip to:
158-
// - 8 if the element size is 1, because any heap allocators is likely
158+
// - 8 if the element size is 1, because any heap allocator is likely
159159
// to round up a request of less than 8 bytes to at least 8 bytes.
160160
// - 4 if elements are moderate-sized (<= 1 KiB).
161161
// - 1 otherwise, to avoid wasting too much space for very short Vecs.
@@ -468,10 +468,6 @@ impl<A: Allocator> RawVecInner<A> {
468468
return Ok(Self::new_in(alloc, elem_layout.alignment()));
469469
}
470470

471-
if let Err(err) = alloc_guard(layout.size()) {
472-
return Err(err);
473-
}
474-
475471
let result = match init {
476472
AllocInit::Uninitialized => alloc.allocate(layout),
477473
#[cfg(not(no_global_oom_handling))]
@@ -662,7 +658,7 @@ impl<A: Allocator> RawVecInner<A> {
662658
let new_layout = layout_array(cap, elem_layout)?;
663659

664660
let ptr = finish_grow(new_layout, self.current_memory(elem_layout), &mut self.alloc)?;
665-
// SAFETY: finish_grow would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
661+
// SAFETY: layout_array would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
666662

667663
unsafe { self.set_ptr_and_cap(ptr, cap) };
668664
Ok(())
@@ -684,7 +680,7 @@ impl<A: Allocator> RawVecInner<A> {
684680
let new_layout = layout_array(cap, elem_layout)?;
685681

686682
let ptr = finish_grow(new_layout, self.current_memory(elem_layout), &mut self.alloc)?;
687-
// SAFETY: finish_grow would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
683+
// SAFETY: layout_array would have resulted in a capacity overflow if we tried to allocate more than `isize::MAX` items
688684
unsafe {
689685
self.set_ptr_and_cap(ptr, cap);
690686
}
@@ -771,8 +767,6 @@ fn finish_grow<A>(
771767
where
772768
A: Allocator,
773769
{
774-
alloc_guard(new_layout.size())?;
775-
776770
let memory = if let Some((ptr, old_layout)) = current_memory {
777771
debug_assert_eq!(old_layout.align(), new_layout.align());
778772
unsafe {
@@ -799,23 +793,6 @@ fn handle_error(e: TryReserveError) -> ! {
799793
}
800794
}
801795

802-
// We need to guarantee the following:
803-
// * We don't ever allocate `> isize::MAX` byte-size objects.
804-
// * We don't overflow `usize::MAX` and actually allocate too little.
805-
//
806-
// On 64-bit we just need to check for overflow since trying to allocate
807-
// `> isize::MAX` bytes will surely fail. On 32-bit and 16-bit we need to add
808-
// an extra guard for this in case we're running on a platform which can use
809-
// all 4GB in user-space, e.g., PAE or x32.
810-
#[inline]
811-
fn alloc_guard(alloc_size: usize) -> Result<(), TryReserveError> {
812-
if usize::BITS < 64 && alloc_size > isize::MAX as usize {
813-
Err(CapacityOverflow.into())
814-
} else {
815-
Ok(())
816-
}
817-
}
818-
819796
#[inline]
820797
fn layout_array(cap: usize, elem_layout: Layout) -> Result<Layout, TryReserveError> {
821798
elem_layout.repeat(cap).map(|(layout, _pad)| layout).map_err(|_| CapacityOverflow.into())

0 commit comments

Comments
 (0)