x86_64/structures/paging/
frame.rs

1//! Abstractions for default-sized and huge physical memory frames.
2
3use super::page::AddressNotAligned;
4use crate::structures::paging::page::{PageSize, Size4KiB};
5use crate::PhysAddr;
6use core::convert::TryFrom;
7use core::fmt;
8use core::marker::PhantomData;
9use core::ops::{Add, AddAssign, Sub, SubAssign};
10
11/// A physical memory frame.
12#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
13#[repr(C)]
14pub struct PhysFrame<S: PageSize = Size4KiB> {
15    // TODO: Make private when our minimum supported stable Rust version is 1.61
16    pub(crate) start_address: PhysAddr,
17    size: PhantomData<S>,
18}
19
20impl<S: PageSize> PhysFrame<S> {
21    /// Returns the frame that starts at the given virtual address.
22    ///
23    /// Returns an error if the address is not correctly aligned (i.e. is not a valid frame start).
24    #[inline]
25    #[rustversion::attr(since(1.61), const)]
26    pub fn from_start_address(address: PhysAddr) -> Result<Self, AddressNotAligned> {
27        if !address.is_aligned_u64(S::SIZE) {
28            return Err(AddressNotAligned);
29        }
30
31        // SAFETY: correct address alignment is checked above
32        Ok(unsafe { PhysFrame::from_start_address_unchecked(address) })
33    }
34
35    /// Returns the frame that starts at the given virtual address.
36    ///
37    /// ## Safety
38    ///
39    /// The address must be correctly aligned.
40    #[inline]
41    #[rustversion::attr(since(1.61), const)]
42    pub unsafe fn from_start_address_unchecked(start_address: PhysAddr) -> Self {
43        PhysFrame {
44            start_address,
45            size: PhantomData,
46        }
47    }
48
49    /// Returns the frame by a physical frame number.
50    ///
51    /// ```
52    /// use x86_64::{PhysAddr, structures::paging::{PhysFrame, Size4KiB}};
53    ///
54    /// assert_eq!(PhysFrame::<Size4KiB>::from_pfn(0x123), PhysFrame::<Size4KiB>::containing_address(PhysAddr::new(0x123000)));
55    /// ```
56    ///
57    /// # Panics
58    ///
59    /// This function will panic if the resulting address is not valid.
60    #[inline]
61    #[rustversion::attr(
62        since(1.61),
63        dep_const_fn::const_fn(cfg(not(feature = "memory_encryption")))
64    )]
65    pub fn from_pfn(pfn: u64) -> Self {
66        match Self::try_from_pfn(pfn) {
67            Ok(frame) => frame,
68            Err(_) => panic!("PFNs must not have any bits in the range 40 to 64 set"),
69        }
70    }
71
72    /// Returns the frame by a physical frame number.
73    ///
74    /// ```
75    /// use x86_64::{PhysAddr, structures::paging::{PhysFrame, Size4KiB}};
76    ///
77    /// assert_eq!(PhysFrame::<Size4KiB>::try_from_pfn(0x123), Ok(PhysFrame::<Size4KiB>::containing_address(PhysAddr::new(0x123000))));
78    /// ```
79    ///
80    /// # Error
81    ///
82    /// This function will return an error if the resulting address is not valid.
83    #[inline]
84    #[rustversion::attr(
85        since(1.61),
86        dep_const_fn::const_fn(cfg(not(feature = "memory_encryption")))
87    )]
88    pub fn try_from_pfn(pfn: u64) -> Result<Self, PfnNotValid> {
89        let addr_raw = if let Some(addr_raw) = pfn.checked_mul(S::SIZE) {
90            addr_raw
91        } else {
92            return Err(PfnNotValid(pfn));
93        };
94        let addr = if let Ok(addr) = PhysAddr::try_new(addr_raw) {
95            addr
96        } else {
97            return Err(PfnNotValid(pfn));
98        };
99        Ok(PhysFrame {
100            start_address: addr,
101            size: PhantomData,
102        })
103    }
104
105    /// Returns the frame by a physical frame number.
106    ///
107    /// # Safety
108    ///
109    /// The resulting address must be valid.
110    #[inline]
111    #[rustversion::attr(since(1.61), const)]
112    pub unsafe fn from_pfn_unchecked(pfn: u64) -> Self {
113        PhysFrame {
114            start_address: unsafe { PhysAddr::new_unsafe(pfn * S::SIZE) },
115            size: PhantomData,
116        }
117    }
118
119    /// Returns the frame that contains the given physical address.
120    #[inline]
121    #[rustversion::attr(since(1.61), const)]
122    pub fn containing_address(address: PhysAddr) -> Self {
123        PhysFrame {
124            start_address: address.align_down_u64(S::SIZE),
125            size: PhantomData,
126        }
127    }
128
129    /// Returns the start address of the frame.
130    #[inline]
131    #[rustversion::attr(since(1.61), const)]
132    pub fn start_address(self) -> PhysAddr {
133        self.start_address
134    }
135
136    /// Returns the size the frame (4KB, 2MB or 1GB).
137    #[inline]
138    #[rustversion::attr(since(1.61), const)]
139    pub fn size(self) -> u64 {
140        S::SIZE
141    }
142
143    /// Returns the PFN of the current frame.
144    ///
145    /// The PFN is defined to be the address divided by the page size.
146    ///
147    /// ```
148    /// use x86_64::{PhysAddr, structures::paging::{PhysFrame, Size1GiB, Size2MiB, Size4KiB}};
149    ///
150    /// assert_eq!(PhysFrame::<Size4KiB>::containing_address(PhysAddr::new(0x123000)).pfn(), 0x123);
151    ///
152    /// // Note that this means that the PFN for the same address will be
153    /// // different for different page sizes.
154    /// assert_eq!(PhysFrame::<Size4KiB>::containing_address(PhysAddr::new(0xC000_0000)).pfn(), 0xC0000);
155    /// assert_eq!(PhysFrame::<Size2MiB>::containing_address(PhysAddr::new(0xC000_0000)).pfn(), 0x600);
156    /// assert_eq!(PhysFrame::<Size1GiB>::containing_address(PhysAddr::new(0xC000_0000)).pfn(), 0x3);
157    /// ```
158    #[inline]
159    #[rustversion::attr(since(1.61), const)]
160    pub fn pfn(self) -> u64 {
161        self.start_address.as_u64() / S::SIZE
162    }
163
164    /// Returns a range of frames, exclusive `end`.
165    #[inline]
166    #[rustversion::attr(since(1.61), const)]
167    pub fn range(start: PhysFrame<S>, end: PhysFrame<S>) -> PhysFrameRange<S> {
168        PhysFrameRange { start, end }
169    }
170
171    /// Returns a range of frames, inclusive `end`.
172    #[inline]
173    #[rustversion::attr(since(1.61), const)]
174    pub fn range_inclusive(start: PhysFrame<S>, end: PhysFrame<S>) -> PhysFrameRangeInclusive<S> {
175        PhysFrameRangeInclusive { start, end }
176    }
177}
178
179impl<S: PageSize> fmt::Debug for PhysFrame<S> {
180    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
181        f.write_fmt(format_args!(
182            "PhysFrame[{}]({:#x})",
183            S::DEBUG_STR,
184            self.start_address().as_u64()
185        ))
186    }
187}
188
189impl<S: PageSize> Add<u64> for PhysFrame<S> {
190    type Output = Self;
191    #[inline]
192    fn add(self, rhs: u64) -> Self::Output {
193        PhysFrame::containing_address(self.start_address() + rhs * S::SIZE)
194    }
195}
196
197impl<S: PageSize> AddAssign<u64> for PhysFrame<S> {
198    #[inline]
199    fn add_assign(&mut self, rhs: u64) {
200        *self = *self + rhs;
201    }
202}
203
204impl<S: PageSize> Sub<u64> for PhysFrame<S> {
205    type Output = Self;
206    #[inline]
207    fn sub(self, rhs: u64) -> Self::Output {
208        PhysFrame::containing_address(self.start_address() - rhs * S::SIZE)
209    }
210}
211
212impl<S: PageSize> SubAssign<u64> for PhysFrame<S> {
213    #[inline]
214    fn sub_assign(&mut self, rhs: u64) {
215        *self = *self - rhs;
216    }
217}
218
219impl<S: PageSize> Sub<PhysFrame<S>> for PhysFrame<S> {
220    type Output = u64;
221    #[inline]
222    fn sub(self, rhs: PhysFrame<S>) -> Self::Output {
223        (self.start_address - rhs.start_address) / S::SIZE
224    }
225}
226
227/// An range of physical memory frames, exclusive the upper bound.
228#[derive(Clone, Copy, PartialEq, Eq, Hash)]
229#[repr(C)]
230pub struct PhysFrameRange<S: PageSize = Size4KiB> {
231    /// The start of the range, inclusive.
232    pub start: PhysFrame<S>,
233    /// The end of the range, exclusive.
234    pub end: PhysFrame<S>,
235}
236
237impl<S: PageSize> PhysFrameRange<S> {
238    /// Returns whether the range contains no frames.
239    #[inline]
240    pub fn is_empty(&self) -> bool {
241        self.start >= self.end
242    }
243
244    /// Returns the number of frames in the range.
245    #[inline]
246    pub fn len(&self) -> u64 {
247        if !self.is_empty() {
248            self.end - self.start
249        } else {
250            0
251        }
252    }
253
254    /// Returns the size in bytes of all frames within the range.
255    #[inline]
256    pub fn size(&self) -> u64 {
257        S::SIZE * self.len()
258    }
259}
260
261impl<S: PageSize> Iterator for PhysFrameRange<S> {
262    type Item = PhysFrame<S>;
263
264    #[inline]
265    fn next(&mut self) -> Option<Self::Item> {
266        if self.start < self.end {
267            let frame = self.start;
268            self.start += 1;
269            Some(frame)
270        } else {
271            None
272        }
273    }
274
275    fn nth(&mut self, n: usize) -> Option<Self::Item> {
276        if self.is_empty() {
277            return None;
278        }
279
280        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
281        // `self.len()` is guaranteed to be smaller than the real value and
282        // `u64::MAX` anyway, so it doesn't make a difference.
283        let n = u64::try_from(n).unwrap_or(u64::MAX);
284
285        // Handling `n >= self.len()` is a bit more complicated because we
286        // can't just add `n` to `self.start` (it might overflow). Handle this
287        // by doing two steps, `self.len()-1` and `1`. This should return
288        // `None`.
289        if n >= self.len() {
290            self.nth(self.len() as usize - 1)?;
291            return self.next();
292        }
293
294        self.start += n;
295        self.next()
296    }
297
298    fn size_hint(&self) -> (usize, Option<usize>) {
299        let len = self.len();
300        usize::try_from(len)
301            .map(|len| (len, Some(len)))
302            .unwrap_or((usize::MAX, None))
303    }
304}
305
306impl<S: PageSize> DoubleEndedIterator for PhysFrameRange<S> {
307    #[inline]
308    fn next_back(&mut self) -> Option<Self::Item> {
309        if self.start < self.end {
310            self.end -= 1;
311            Some(self.end)
312        } else {
313            None
314        }
315    }
316
317    fn nth_back(&mut self, n: usize) -> Option<Self::Item> {
318        if self.is_empty() {
319            return None;
320        }
321
322        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
323        // `self.len()` is guaranteed to be smaller than the real value and
324        // `u64::MAX` anyway, so it doesn't make a difference.
325        let n = u64::try_from(n).unwrap_or(u64::MAX);
326
327        // Handling `n >= self.len()` is a bit more complicated because we
328        // can't just subtract `n` to `self.end` (it might overflow). Handle
329        // this by doing two steps, `self.len()-1` and `1`. This should return
330        // `None`.
331        if n >= self.len() {
332            self.nth_back(self.len() as usize - 1)?;
333            return self.next_back();
334        }
335
336        self.end -= n;
337        self.next_back()
338    }
339}
340
341impl<S: PageSize> fmt::Debug for PhysFrameRange<S> {
342    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
343        f.debug_struct("PhysFrameRange")
344            .field("start", &self.start)
345            .field("end", &self.end)
346            .finish()
347    }
348}
349
350/// A passed `u64` was not a valid physical address.
351///
352/// This means that bits 40 to 64 were not all null.
353///
354/// Contains the invalid PFN.
355#[derive(Debug, Clone, Copy, PartialEq, Eq)]
356#[repr(transparent)]
357pub struct PfnNotValid(pub u64);
358
359// Implementation of display
360impl fmt::Display for PfnNotValid {
361    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
362        f.debug_tuple("PhysAddrNotValid")
363            .field(&format_args!("{:#x}", self.0))
364            .finish()
365    }
366}
367
368/// An range of physical memory frames, inclusive the upper bound.
369#[derive(Clone, Copy, PartialEq, Eq, Hash)]
370#[repr(C)]
371pub struct PhysFrameRangeInclusive<S: PageSize = Size4KiB> {
372    /// The start of the range, inclusive.
373    pub start: PhysFrame<S>,
374    /// The start of the range, inclusive.
375    pub end: PhysFrame<S>,
376}
377
378impl<S: PageSize> PhysFrameRangeInclusive<S> {
379    /// Returns whether the range contains no frames.
380    #[inline]
381    pub fn is_empty(&self) -> bool {
382        self.start > self.end
383    }
384
385    /// Returns the number of frames in the range.
386    #[inline]
387    pub fn len(&self) -> u64 {
388        if !self.is_empty() {
389            self.end - self.start + 1
390        } else {
391            0
392        }
393    }
394
395    /// Returns the size in bytes of all frames within the range.
396    #[inline]
397    pub fn size(&self) -> u64 {
398        S::SIZE * self.len()
399    }
400}
401
402impl<S: PageSize> Iterator for PhysFrameRangeInclusive<S> {
403    type Item = PhysFrame<S>;
404
405    #[inline]
406    fn next(&mut self) -> Option<Self::Item> {
407        if self.start <= self.end {
408            let frame = self.start;
409
410            // If the end of the inclusive range is the maximum page possible for size S,
411            // incrementing start until it is greater than the end will cause an integer overflow.
412            // So instead, in that case we decrement end rather than incrementing start.
413            let max_frame_addr = PhysAddr::new_truncate(u64::MAX) - (S::SIZE - 1);
414            if self.start.start_address() < max_frame_addr {
415                self.start += 1;
416            } else {
417                self.end -= 1;
418            }
419            Some(frame)
420        } else {
421            None
422        }
423    }
424
425    fn nth(&mut self, n: usize) -> Option<Self::Item> {
426        if self.is_empty() {
427            return None;
428        }
429
430        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
431        // `self.len()` is guaranteed to be smaller than the real value and
432        // `u64::MAX` anyway, so it doesn't make a difference.
433        let n = u64::try_from(n).unwrap_or(u64::MAX);
434
435        // Handling `n >= self.len()` is a bit more complicated because we
436        // can't just add `n` to `self.start` (it might overflow). Handle this
437        // by doing two steps, `self.len()-1` and `1`. This should return
438        // `None`.
439        if n >= self.len() {
440            self.nth(self.len() as usize - 1)?;
441            return self.next();
442        }
443
444        self.start += n;
445        self.next()
446    }
447
448    fn size_hint(&self) -> (usize, Option<usize>) {
449        let len = self.len();
450        usize::try_from(len)
451            .map(|len| (len, Some(len)))
452            .unwrap_or((usize::MAX, None))
453    }
454}
455
456impl<S: PageSize> DoubleEndedIterator for PhysFrameRangeInclusive<S> {
457    #[inline]
458    fn next_back(&mut self) -> Option<Self::Item> {
459        if self.start <= self.end {
460            let frame = self.end;
461
462            // If the start of the inclusive range is 0, decrementing end until
463            // it is smaller than the start will cause an integer underflow.
464            // So instead, in that case we increment start rather than decrementing end.
465            if self.end.start_address().as_u64() != 0 {
466                self.end -= 1;
467            } else {
468                self.start += 1;
469            }
470            Some(frame)
471        } else {
472            None
473        }
474    }
475
476    fn nth_back(&mut self, n: usize) -> Option<Self::Item> {
477        if self.is_empty() {
478            return None;
479        }
480
481        // Convert to `u64`. If the value doesn't fit just use `u64::MAX`.
482        // `self.len()` is guaranteed to be smaller than the real value and
483        // `u64::MAX` anyway, so it doesn't make a difference.
484        let n = u64::try_from(n).unwrap_or(u64::MAX);
485
486        // Handling `n >= self.len()` is a bit more complicated because we
487        // can't just subtract `n` to `self.end` (it might overflow). Handle
488        // this by doing two steps, `self.len()-1` and `1`. This should return
489        // `None`.
490        if n >= self.len() {
491            self.nth_back(self.len() as usize - 1)?;
492            return self.next_back();
493        }
494
495        self.end -= n;
496        self.next_back()
497    }
498}
499
500impl<S: PageSize> fmt::Debug for PhysFrameRangeInclusive<S> {
501    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
502        f.debug_struct("PhysFrameRangeInclusive")
503            .field("start", &self.start)
504            .field("end", &self.end)
505            .finish()
506    }
507}
508
509#[cfg(kani)]
510impl<S: PageSize> kani::Arbitrary for PhysFrame<S> {
511    fn any() -> Self {
512        Self::containing_address(kani::any())
513    }
514}
515
516#[cfg(test)]
517mod tests {
518    use super::*;
519    #[test]
520    pub fn test_frame_range_len() {
521        let start_addr = PhysAddr::new(0xdead_beaf);
522        let start = PhysFrame::<Size4KiB>::containing_address(start_addr);
523        let end = start + 50;
524
525        let range = PhysFrameRange { start, end };
526        assert_eq!(range.len(), 50);
527
528        let range_inclusive = PhysFrameRangeInclusive { start, end };
529        assert_eq!(range_inclusive.len(), 51);
530    }
531}
532
533#[cfg(kani)]
534mod proofs {
535    use super::*;
536
537    #[kani::proof]
538    fn phys_frame_range_next() {
539        let start = kani::any::<PhysFrame>();
540        let end = kani::any::<PhysFrame>();
541        let mut range = PhysFrame::range(start, end);
542
543        // Test that calling `next` twice works.
544        let difference = end
545            .start_address()
546            .as_u64()
547            .checked_sub(start.start_address().as_u64());
548        let expected_result = difference.is_some_and(|d| d >= 0x1000).then(|| start);
549        assert_eq!(range.next(), expected_result);
550        let expected_result = difference.is_some_and(|d| d >= 0x2000).then(|| start + 1);
551        assert_eq!(range.next(), expected_result);
552    }
553
554    #[kani::proof]
555    fn phys_frame_range_inclusive_next() {
556        let start = kani::any::<PhysFrame>();
557        let end = kani::any::<PhysFrame>();
558        let mut range = PhysFrame::range_inclusive(start, end);
559
560        // Test that calling `next` twice works.
561        let difference = end
562            .start_address()
563            .as_u64()
564            .checked_sub(start.start_address().as_u64());
565        let expected_result = difference.is_some().then(|| start);
566        assert_eq!(range.next(), expected_result);
567        let expected_result = difference.is_some_and(|d| d >= 0x1000).then(|| start + 1);
568        assert_eq!(range.next(), expected_result);
569    }
570
571    #[kani::proof]
572    fn phys_frame_range_next_back() {
573        let start = kani::any::<PhysFrame>();
574        let end = kani::any::<PhysFrame>();
575        let mut range = PhysFrame::range(start, end);
576
577        // Test that calling `next_back` twice works.
578        let difference = end
579            .start_address()
580            .as_u64()
581            .checked_sub(start.start_address().as_u64());
582        let expected_result = difference.is_some_and(|d| d >= 0x1000).then(|| end - 1);
583        assert_eq!(range.next_back(), expected_result);
584        let expected_result = difference.is_some_and(|d| d >= 0x2000).then(|| end - 2);
585        assert_eq!(range.next_back(), expected_result);
586    }
587
588    #[kani::proof]
589    fn phys_frame_range_inclusive_next_back() {
590        let start = kani::any::<PhysFrame>();
591        let end = kani::any::<PhysFrame>();
592        let mut range = PhysFrame::range_inclusive(start, end);
593
594        // Test that calling `next_back` twice works.
595        let difference = end
596            .start_address()
597            .as_u64()
598            .checked_sub(start.start_address().as_u64());
599        let expected_result = difference.is_some().then(|| end);
600        assert_eq!(range.next_back(), expected_result);
601        let expected_result = difference.is_some_and(|d| d >= 0x1000).then(|| end - 1);
602        assert_eq!(range.next_back(), expected_result);
603    }
604
605    #[kani::proof]
606    #[kani::unwind(1)]
607    fn phys_frame_range_nth_0() {
608        let start = kani::any::<PhysFrame>();
609        let end = kani::any::<PhysFrame>();
610        let mut range = PhysFrame::range(start, end);
611        let mut range2 = PhysFrame::range(start, end);
612
613        // Test that nth(0) behaves like next().
614        assert_eq!(range.next(), range2.nth(0));
615        assert_eq!(range.next(), range2.nth(0));
616    }
617
618    #[kani::proof]
619    #[kani::unwind(1)]
620    fn phys_frame_range_nth() {
621        let start = kani::any::<PhysFrame>();
622        let end = kani::any::<PhysFrame>();
623        let m = kani::any::<usize>();
624        let n = kani::any::<usize>();
625        let sum = m.saturating_add(n).saturating_add(1);
626        let mut range = PhysFrame::range(start, end);
627        let mut range2 = PhysFrame::range(start, end);
628
629        // Test that doing steps of size m and n is equivalent to a single step
630        // of size m+n+1.
631        range.nth(m);
632        assert_eq!(range.nth(n), range2.nth(sum));
633    }
634
635    #[kani::proof]
636    #[kani::unwind(1)]
637    fn phys_frame_range_inclusive_nth_0() {
638        let start = kani::any::<PhysFrame>();
639        let end = kani::any::<PhysFrame>();
640        let mut range = PhysFrame::range_inclusive(start, end);
641        let mut range2 = PhysFrame::range_inclusive(start, end);
642
643        // Test that nth(0) behaves like next().
644        assert_eq!(range.next(), range2.nth(0));
645        assert_eq!(range.next(), range2.nth(0));
646    }
647
648    #[kani::proof]
649    #[kani::unwind(1)]
650    fn phys_frame_range_inclusive_nth() {
651        let start = kani::any::<PhysFrame>();
652        let end = kani::any::<PhysFrame>();
653        let m = kani::any::<usize>();
654        let n = kani::any::<usize>();
655        let sum = m.saturating_add(n).saturating_add(1);
656        let mut range = PhysFrame::range_inclusive(start, end);
657        let mut range2 = PhysFrame::range_inclusive(start, end);
658
659        // Test that doing steps of size m and n is equivalent to a single step
660        // of size m+n+1.
661        range.nth(m);
662        assert_eq!(range.nth(n), range2.nth(sum));
663    }
664
665    #[kani::proof]
666    #[kani::unwind(1)]
667    fn phys_frame_range_nth_back_0() {
668        let start = kani::any::<PhysFrame>();
669        let end = kani::any::<PhysFrame>();
670        let mut range = PhysFrame::range(start, end);
671        let mut range2 = PhysFrame::range(start, end);
672
673        // Test that nth_back(0) behaves like next_back().
674        assert_eq!(range.next_back(), range2.nth_back(0));
675        assert_eq!(range.next_back(), range2.nth_back(0));
676    }
677
678    #[kani::proof]
679    #[kani::unwind(1)]
680    fn phys_frame_range_nth_back() {
681        let start = kani::any::<PhysFrame>();
682        let end = kani::any::<PhysFrame>();
683        let m = kani::any::<usize>();
684        let n = kani::any::<usize>();
685        let sum = m.saturating_add(n).saturating_add(1);
686        let mut range = PhysFrame::range(start, end);
687        let mut range2 = PhysFrame::range(start, end);
688
689        // Test that doing steps of size m and n is equivalent to a single step
690        // of size m+n+1.
691        range.nth_back(m);
692        assert_eq!(range.nth_back(n), range2.nth_back(sum));
693    }
694
695    #[kani::proof]
696    #[kani::unwind(1)]
697    fn phys_frame_range_inclusive_nth_back_0() {
698        let start = kani::any::<PhysFrame>();
699        let end = kani::any::<PhysFrame>();
700        let mut range = PhysFrame::range_inclusive(start, end);
701        let mut range2 = PhysFrame::range_inclusive(start, end);
702
703        // Test that nth_back(0) behaves like next_back().
704        assert_eq!(range.next_back(), range2.nth_back(0));
705        assert_eq!(range.next_back(), range2.nth_back(0));
706    }
707
708    #[kani::proof]
709    #[kani::unwind(1)]
710    fn phys_frame_range_inclusive_nth_back() {
711        let start = kani::any::<PhysFrame>();
712        let end = kani::any::<PhysFrame>();
713        let m = kani::any::<usize>();
714        let n = kani::any::<usize>();
715        let sum = m.saturating_add(n).saturating_add(1);
716        let mut range = PhysFrame::range_inclusive(start, end);
717        let mut range2 = PhysFrame::range_inclusive(start, end);
718
719        // Test that doing steps of size m and n is equivalent to a single step
720        // of size m+n+1.
721        range.nth_back(m);
722        assert_eq!(range.nth_back(n), range2.nth_back(sum));
723    }
724}
x86_64/structures/paging/frame.rs

x86_64/structures/paging/
frame.rs
