Repository navigation
Make ranges jump address space gaps #618
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Changes from all commits
3625aef
5009eca
66a12ae
ce84e00
62ace8a
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -208,10 +208,6 @@ impl<S: PageSize> Page<S> { | |
| } | ||
|
|
||
| // FIXME: Move this into the `Step` impl, once `Step` is stabilized. | ||
| #[cfg(any( | ||
| all(feature = "instructions", target_arch = "x86_64"), | ||
| feature = "step_trait" | ||
| ))] | ||
| pub(crate) fn forward_checked_impl(start: Self, count: usize) -> Option<Self> { | ||
| let count = u64::try_from(count).ok()?.checked_mul(S::SIZE)?; | ||
| let start_address = VirtAddr::forward_checked_u64(start.start_address, count)?; | ||
|
|
@@ -220,6 +216,16 @@ impl<S: PageSize> Page<S> { | |
| size: PhantomData, | ||
| }) | ||
| } | ||
|
|
||
| // FIXME: Move this into the `Step` impl, once `Step` is stabilized. | ||
| pub(crate) fn backward_checked_impl(start: Self, count: usize) -> Option<Self> { | ||
| let count = u64::try_from(count).ok()?.checked_mul(S::SIZE)?; | ||
| let start_address = VirtAddr::backward_checked_u64(start.start_address, count)?; | ||
| Some(Self { | ||
| start_address, | ||
| size: PhantomData, | ||
| }) | ||
| } | ||
| } | ||
|
|
||
| impl<S: NotGiantPageSize> Page<S> { | ||
|
|
@@ -351,14 +357,7 @@ impl<S: PageSize> Step for Page<S> { | |
| } | ||
|
|
||
| fn backward_checked(start: Self, count: usize) -> Option<Self> { | ||
| use core::convert::TryFrom; | ||
|
|
||
| let count = u64::try_from(count).ok()?.checked_mul(S::SIZE)?; | ||
| let start_address = VirtAddr::backward_checked_u64(start.start_address, count)?; | ||
| Some(Self { | ||
| start_address, | ||
| size: PhantomData, | ||
| }) | ||
| Self::backward_checked_impl(start, count) | ||
| } | ||
|
|
||
| fn forward_overflowing(start: Self, count: usize) -> (Self, bool) { | ||
|
|
@@ -430,7 +429,7 @@ impl<S: PageSize> Iterator for PageRangeIter<S> { | |
| fn next(&mut self) -> Option<Self::Item> { | ||
| if self.0.start < self.0.end { | ||
| let page = self.0.start; | ||
| self.0.start += 1; | ||
| self.0.start = Page::forward_checked_impl(self.0.start, 1)?; | ||
| Some(page) | ||
| } else { | ||
| None | ||
|
|
@@ -483,7 +482,7 @@ impl<S: PageSize> DoubleEndedIterator for PageRangeIter<S> { | |
| #[inline] | ||
| fn next_back(&mut self) -> Option<Self::Item> { | ||
| if self.0.start < self.0.end { | ||
| self.0.end -= 1; | ||
| self.0.end = Page::backward_checked_impl(self.0.end, 1)?; | ||
| Some(self.0.end) | ||
| } else { | ||
| None | ||
|
|
@@ -605,9 +604,9 @@ impl<S: PageSize> Iterator for PageRangeInclusiveIter<S> { | |
| // So instead, in that case we decrement end rather than incrementing start. | ||
| let max_page_addr = VirtAddr::new(u64::MAX) - (S::SIZE - 1); | ||
| if self.0.start.start_address() < max_page_addr { | ||
| self.0.start += 1; | ||
| self.0.start = Page::forward_checked_impl(self.0.start, 1)?; | ||
| } else { | ||
| self.0.end -= 1; | ||
| self.0.end = Page::backward_checked_impl(self.0.end, 1)?; | ||
| } | ||
| Some(page) | ||
| } else { | ||
|
|
@@ -665,9 +664,9 @@ impl<S: PageSize> DoubleEndedIterator for PageRangeInclusiveIter<S> { | |
|
|
||
| // If the start of the inclusive range is 0, decrementing end until | ||
| // it is smaller than the start will cause an integer underflow. | ||
| // So instead, in that case we increment start rather than decrementing end. | ||
| if self.0.end.start_address().as_u64() != 0 { | ||
| self.0.end -= 1; | ||
| // In that case we increment start rather than decrementing end. | ||
| if let Some(end) = Page::backward_checked_impl(self.0.end, 1) { | ||
| self.0.end = end; | ||
| } else { | ||
| self.0.start += 1; | ||
| } | ||
|
|
@@ -799,79 +798,81 @@ mod tests { | |
| } | ||
|
|
||
| #[test] | ||
| #[should_panic = "attempt to add with overflow or resulted in non-canonical virtual address"] | ||
| fn test_page_range_next_jumping_gap_panics() { | ||
| fn test_page_range_next_jumping_gap() { | ||
| let start = 0x7fff_ffff_f000; | ||
| let end = 0xffff_8000_0000_0000; | ||
| let start = VirtAddr::new(start); | ||
| let end = VirtAddr::new(end); | ||
| let start = Page::<Size4KiB>::from_start_address(start).unwrap(); | ||
| let end = Page::from_start_address(end).unwrap(); | ||
| Page::range(start, end).into_iter().next(); | ||
| assert_eq!(Page::range(start, end).into_iter().next(), Some(start)); | ||
| } | ||
|
|
||
| // TODO: This probably shouldn't panic, but we can't fix this without a breaking change. | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Please add this behavior change as a breaking change to the release notes. |
||
| #[test] | ||
| #[should_panic = "attempt to subtract with overflow or resulted in non-canonical virtual address"] | ||
| fn test_page_range_next_back_jumping_gap_panics() { | ||
| fn test_page_range_next_back_jumping_gap() { | ||
| let start = 0x7fff_ffff_f000; | ||
| let end = 0xffff_8000_0000_0000; | ||
| let start = VirtAddr::new(start); | ||
| let end = VirtAddr::new(end); | ||
| let start = Page::<Size4KiB>::from_start_address(start).unwrap(); | ||
| let end = Page::from_start_address(end).unwrap(); | ||
| Page::range(start, end).into_iter().next_back(); | ||
| assert_eq!(Page::range(start, end).into_iter().next_back(), Some(start)); | ||
| } | ||
|
|
||
| #[test] | ||
| #[should_panic = "attempt to add with overflow or resulted in non-canonical virtual address"] | ||
| fn test_page_range_inclusive_next_not_jumping_gap_panics() { | ||
| fn test_page_range_inclusive_next_not_jumping_gap() { | ||
| let start = 0x7fff_ffff_f000; | ||
| let end = 0x7fff_ffff_f000; | ||
| let start = VirtAddr::new(start); | ||
| let end = VirtAddr::new(end); | ||
| let start = Page::<Size4KiB>::from_start_address(start).unwrap(); | ||
| let end = Page::from_start_address(end).unwrap(); | ||
| Page::range_inclusive(start, end).into_iter().next(); | ||
| assert_eq!( | ||
| Page::range_inclusive(start, end).into_iter().next(), | ||
| Some(start) | ||
| ); | ||
|
Comment on lines
+830
to
+833
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We should add similar asserts to the remaining tests that formerly panicked. |
||
| } | ||
|
|
||
| #[test] | ||
| #[should_panic = "attempt to subtract with overflow or resulted in non-canonical virtual address"] | ||
| fn test_page_range_inclusive_next_back_not_jumping_gap_panics() { | ||
| fn test_page_range_inclusive_next_back_not_jumping_gap() { | ||
| let start = 0x7fff_ffff_f000; | ||
| let end = 0xffff_8000_0000_0000; | ||
| let start = VirtAddr::new(start); | ||
| let end = VirtAddr::new(end); | ||
| let start = Page::<Size4KiB>::from_start_address(start).unwrap(); | ||
| let end = Page::from_start_address(end).unwrap(); | ||
| Page::range_inclusive(start, end).into_iter().next_back(); | ||
| assert_eq!( | ||
| Page::range_inclusive(start, end).into_iter().next_back(), | ||
| Some(end) | ||
| ); | ||
| } | ||
|
|
||
| // TODO: This probably shouldn't panic, but we can't fix this without a breaking change. | ||
| #[test] | ||
| #[should_panic = "attempt to add with overflow or resulted in non-canonical virtual address"] | ||
| fn test_page_range_inclusive_next_jumping_gap_panics() { | ||
| fn test_page_range_inclusive_next_jumping_gap() { | ||
| let start = 0x7fff_ffff_f000; | ||
| let end = 0x7fff_ffff_f000; | ||
| let start = VirtAddr::new(start); | ||
| let end = VirtAddr::new(end); | ||
| let start = Page::<Size4KiB>::from_start_address(start).unwrap(); | ||
| let end = Page::from_start_address(end).unwrap(); | ||
| Page::range_inclusive(start, end).into_iter().next(); | ||
| Page::range_inclusive(start, end).into_iter().next(); | ||
| assert_eq!( | ||
| Page::range_inclusive(start, end).into_iter().next(), | ||
| Some(start) | ||
| ); | ||
| } | ||
|
|
||
| #[test] | ||
| #[should_panic = "attempt to subtract with overflow or resulted in non-canonical virtual address"] | ||
| fn test_page_range_inclusive_next_back_jumping_gap_panics() { | ||
| fn test_page_range_inclusive_next_back_jumping_gap() { | ||
| let start = 0xffff_8000_0000_0000; | ||
| let end = 0xffff_8000_0000_0000; | ||
| let start = VirtAddr::new(start); | ||
| let end = VirtAddr::new(end); | ||
| let start = Page::<Size4KiB>::from_start_address(start).unwrap(); | ||
| let end = Page::from_start_address(end).unwrap(); | ||
| Page::range_inclusive(start, end).into_iter().next_back(); | ||
| Page::range_inclusive(start, end).into_iter().next_back(); | ||
| assert_eq!( | ||
| Page::range_inclusive(start, end).into_iter().next_back(), | ||
| Some(end) | ||
| ); | ||
| } | ||
|
|
||
| #[test] | ||
|
|
@@ -1016,25 +1017,12 @@ mod tests { | |
| mod proofs { | ||
| use super::*; | ||
|
|
||
| fn page_range_next_harness(should_panic_mode: bool) { | ||
| #[kani::proof] | ||
| fn page_range_next() { | ||
| let start = kani::any::<Page<Size4KiB>>(); | ||
| let end = kani::any::<Page<Size4KiB>>(); | ||
|
|
||
| // If the code is expected to panic, only run it in `#[should_panic]` | ||
| // mode. | ||
| let should_panic = start.start_address().as_u64() != 0x7fff_ffff_e000 | ||
| || start.start_address().as_u64() != 0x7fff_ffff_f000; | ||
| kani::assume(should_panic == should_panic_mode); | ||
|
|
||
| if should_panic { | ||
| // Calling `next` should panic. | ||
| let mut our_range_iter = Page::range(start, end).into_iter(); | ||
| our_range_iter.next(); | ||
| our_range_iter.next(); | ||
| return; | ||
| } | ||
|
|
||
| // Otherwise the results should match what `Range` returns. | ||
| // The results should match what `Range` returns. | ||
| let mut our_range_iter = Page::range(start, end).into_iter(); | ||
| let mut native_range = start..end; | ||
| // The first assert checks that we're returning the correct value. | ||
|
|
@@ -1044,35 +1032,11 @@ mod proofs { | |
| } | ||
|
|
||
| #[kani::proof] | ||
| fn page_range_next() { | ||
| page_range_next_harness(false); | ||
| } | ||
|
|
||
| #[kani::proof] | ||
| #[kani::should_panic] | ||
| fn page_range_next_panic() { | ||
| page_range_next_harness(true); | ||
| } | ||
|
|
||
| fn page_range_next_back_harness(should_panic_mode: bool) { | ||
| fn page_range_next_back_harness() { | ||
| let start = kani::any::<Page<Size4KiB>>(); | ||
| let end = kani::any::<Page<Size4KiB>>(); | ||
|
|
||
| // If the code is expected to panic, only run it in `#[should_panic]` | ||
| // mode. | ||
| let should_panic = start.start_address().as_u64() != 0xffff_8000_0000_0000 | ||
| || start.start_address().as_u64() != 0xffff_8000_0000_1000; | ||
| kani::assume(should_panic == should_panic_mode); | ||
|
|
||
| if should_panic { | ||
| // Calling `next_back` should panic. | ||
| let mut our_range_iter = Page::range(start, end).into_iter(); | ||
| our_range_iter.next_back(); | ||
| our_range_iter.next_back(); | ||
| return; | ||
| } | ||
|
|
||
| // Otherwise the results should match what `Range` returns. | ||
| // The results should match what `Range` returns. | ||
| let mut our_range_iter = Page::range(start, end).into_iter(); | ||
| let mut native_range = start..end; | ||
| // The first assert checks that we're returning the correct value. | ||
|
|
@@ -1082,35 +1046,11 @@ mod proofs { | |
| } | ||
|
|
||
| #[kani::proof] | ||
| fn page_range_next_back() { | ||
| page_range_next_back_harness(false); | ||
| } | ||
|
|
||
| #[kani::proof] | ||
| #[kani::should_panic] | ||
| fn page_range_next_back_panic() { | ||
| page_range_next_back_harness(true); | ||
| } | ||
|
|
||
| fn page_range_inclusive_next_harness(should_panic_mode: bool) { | ||
| fn page_range_inclusive_next_harness() { | ||
| let start = kani::any::<Page<Size4KiB>>(); | ||
| let end = kani::any::<Page<Size4KiB>>(); | ||
|
|
||
| // If the code is expected to panic, only run it in `#[should_panic]` | ||
| // mode. | ||
| let should_panic = start.start_address().as_u64() != 0x7fff_ffff_e000 | ||
| || start.start_address().as_u64() != 0x7fff_ffff_f000; | ||
| kani::assume(should_panic == should_panic_mode); | ||
|
|
||
| if should_panic { | ||
| // Calling `next` should panic. | ||
| let mut our_range_iter = Page::range_inclusive(start, end).into_iter(); | ||
| our_range_iter.next(); | ||
| our_range_iter.next(); | ||
| return; | ||
| } | ||
|
|
||
| // Otherwise the results should match what `Range` returns. | ||
| // The results should match what `Range` returns. | ||
| let mut our_range_iter = Page::range_inclusive(start, end).into_iter(); | ||
| let mut native_range = start..=end; | ||
| // The first assert checks that we're returning the correct value. | ||
|
|
@@ -1120,35 +1060,11 @@ mod proofs { | |
| } | ||
|
|
||
| #[kani::proof] | ||
| fn page_range_inclusive_next() { | ||
| page_range_inclusive_next_harness(false); | ||
| } | ||
|
|
||
| #[kani::proof] | ||
| #[kani::should_panic] | ||
| fn page_range_inclusive_next_panic() { | ||
| page_range_inclusive_next_harness(true); | ||
| } | ||
|
|
||
| fn page_range_inclusive_next_back_harness(should_panic_mode: bool) { | ||
| fn page_range_inclusive_next_back() { | ||
| let start = kani::any::<Page<Size4KiB>>(); | ||
| let end = kani::any::<Page<Size4KiB>>(); | ||
|
|
||
| // If the code is expected to panic, only run it in `#[should_panic]` | ||
| // mode. | ||
| let should_panic = start.start_address().as_u64() != 0xffff_8000_0000_0000 | ||
| || start.start_address().as_u64() != 0xffff_8000_0000_1000; | ||
| kani::assume(should_panic == should_panic_mode); | ||
|
|
||
| if should_panic { | ||
| // Calling `next_back` should panic. | ||
| let mut our_range_iter = Page::range_inclusive(start, end).into_iter(); | ||
| our_range_iter.next_back(); | ||
| our_range_iter.next_back(); | ||
| return; | ||
| } | ||
|
|
||
| // Otherwise the results should match what `Range` returns. | ||
| // The results should match what `Range` returns. | ||
| let mut our_range_iter = Page::range_inclusive(start, end).into_iter(); | ||
| let mut native_range = start..=end; | ||
| // The first assert checks that we're returning the correct value. | ||
|
|
@@ -1157,17 +1073,6 @@ mod proofs { | |
| assert_eq!(our_range_iter.next_back(), native_range.next_back()); | ||
| } | ||
|
|
||
| #[kani::proof] | ||
| fn page_range_inclusive_next_back() { | ||
| page_range_inclusive_next_back_harness(false); | ||
| } | ||
|
|
||
| #[kani::proof] | ||
| #[kani::should_panic] | ||
| fn page_range_inclusive_next_back_panic() { | ||
| page_range_inclusive_next_back_harness(true); | ||
| } | ||
|
|
||
| fn page_range_nth_harness(should_panic_mode: bool) { | ||
| let start = kani::any::<Page>(); | ||
| let end = kani::any::<Page>(); | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Let's replace the implementation of
backward_checkedforPage'sStepwith a call to this function.