use core::convert::TryFrom;
use core::fmt;
#[cfg(feature = "step_trait")]
use core::iter::Step;
use core::ops::{Add, AddAssign, Sub, SubAssign};
#[cfg(feature = "memory_encryption")]
use core::sync::atomic::Ordering as MemOrdering;
use core::sync::atomic::{AtomicBool, Ordering};
#[cfg(feature = "memory_encryption")]
use crate::structures::mem_encrypt::ENC_BIT_MASK;
use crate::structures::paging::page_table::PageTableLevel;
use crate::structures::paging::{PageOffset, PageTableIndex};
use bit_field::BitField;
use dep_const_fn::const_fn;
pub static LA57_ENABLED: AtomicBool = AtomicBool::new(false);
#[inline]
pub fn enable_la57_mode() {
LA57_ENABLED.store(true, Ordering::SeqCst);
}
#[inline]
pub fn disable_la57_mode() {
LA57_ENABLED.store(false, Ordering::SeqCst);
}
#[inline]
pub fn is_la57_mode() -> bool {
LA57_ENABLED.load(Ordering::SeqCst)
}
#[inline]
fn canonicalize(addr: u64) -> u64 {
if is_la57_mode() {
((addr << 7) as i64 >> 7) as u64
} else {
((addr << 16) as i64 >> 16) as u64
}
}
#[inline]
const fn canonicalize_48bit(addr: u64) -> u64 {
((addr << 16) as i64 >> 16) as u64
}
const ADDRESS_SPACE_SIZE: u64 = 0x1_0000_0000_0000;
#[allow(dead_code)]
const ADDRESS_SPACE_SIZE_LA57: u64 = 0x100_0000_0000_0000;
#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
#[repr(transparent)]
pub struct VirtAddr(u64);
#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
#[repr(transparent)]
pub struct PhysAddr(u64);
pub struct VirtAddrNotValid(pub u64);
impl core::fmt::Debug for VirtAddrNotValid {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
f.debug_tuple("VirtAddrNotValid")
.field(&format_args!("{:#x}", self.0))
.finish()
}
}
impl VirtAddr {
#[inline]
pub fn new(addr: u64) -> VirtAddr {
match Self::try_new(addr) {
Ok(v) => v,
Err(_) => {
if is_la57_mode() {
panic!("virtual address must be sign extended in bits 57 to 64 (LA57 mode)")
} else {
panic!("virtual address must be sign extended in bits 48 to 64")
}
}
}
}
#[inline]
pub const fn new_const(addr: u64) -> VirtAddr {
match Self::try_new_const(addr) {
Ok(v) => v,
Err(_) => panic!("virtual address must be sign extended in bits 48 to 64"),
}
}
#[inline]
pub fn try_new(addr: u64) -> Result<VirtAddr, VirtAddrNotValid> {
let canonical = canonicalize(addr);
if canonical == addr {
Ok(VirtAddr(addr))
} else {
Err(VirtAddrNotValid(addr))
}
}
#[inline]
pub const fn try_new_const(addr: u64) -> Result<VirtAddr, VirtAddrNotValid> {
let v = Self::new_truncate_const(addr);
if v.0 == addr {
Ok(v)
} else {
Err(VirtAddrNotValid(addr))
}
}
#[inline]
pub fn new_truncate(addr: u64) -> VirtAddr {
VirtAddr(canonicalize(addr))
}
#[inline]
pub const fn new_truncate_const(addr: u64) -> VirtAddr {
VirtAddr(canonicalize_48bit(addr))
}
#[inline]
pub const unsafe fn new_unsafe(addr: u64) -> VirtAddr {
VirtAddr(addr)
}
#[inline]
pub const fn zero() -> VirtAddr {
VirtAddr(0)
}
#[inline]
pub const fn as_u64(self) -> u64 {
self.0
}
#[cfg(target_pointer_width = "64")]
#[inline]
pub fn from_ptr<T: ?Sized>(ptr: *const T) -> Self {
Self::new(ptr as *const () as u64)
}
#[cfg(target_pointer_width = "64")]
#[inline]
pub const fn as_ptr<T>(self) -> *const T {
self.as_u64() as *const T
}
#[cfg(target_pointer_width = "64")]
#[inline]
pub const fn as_mut_ptr<T>(self) -> *mut T {
self.as_ptr::<T>() as *mut T
}
#[inline]
pub const fn is_null(self) -> bool {
self.0 == 0
}
#[inline]
pub fn align_up<U>(self, align: U) -> Self
where
U: Into<u64>,
{
VirtAddr::new_truncate(align_up(self.0, align.into()))
}
#[inline]
pub fn align_down<U>(self, align: U) -> Self
where
U: Into<u64>,
{
self.align_down_u64(align.into())
}
#[inline]
pub(crate) const fn align_down_u64(self, align: u64) -> Self {
VirtAddr::new_truncate_const(align_down(self.0, align))
}
#[inline]
pub fn is_aligned<U>(self, align: U) -> bool
where
U: Into<u64>,
{
self.is_aligned_u64(align.into())
}
#[inline]
pub(crate) const fn is_aligned_u64(self, align: u64) -> bool {
self.align_down_u64(align).as_u64() == self.as_u64()
}
#[inline]
pub const fn page_offset(self) -> PageOffset {
PageOffset::new_truncate(self.0 as u16)
}
#[inline]
pub const fn p1_index(self) -> PageTableIndex {
PageTableIndex::new_truncate((self.0 >> 12) as u16)
}
#[inline]
pub const fn p2_index(self) -> PageTableIndex {
PageTableIndex::new_truncate((self.0 >> 12 >> 9) as u16)
}
#[inline]
pub const fn p3_index(self) -> PageTableIndex {
PageTableIndex::new_truncate((self.0 >> 12 >> 9 >> 9) as u16)
}
#[inline]
pub const fn p4_index(self) -> PageTableIndex {
PageTableIndex::new_truncate((self.0 >> 12 >> 9 >> 9 >> 9) as u16)
}
#[inline]
pub const fn p5_index(self) -> PageTableIndex {
PageTableIndex::new_truncate((self.0 >> 12 >> 9 >> 9 >> 9 >> 9) as u16)
}
#[inline]
pub const fn page_table_index(self, level: PageTableLevel) -> PageTableIndex {
PageTableIndex::new_truncate((self.0 >> 12 >> ((level as u8 - 1) * 9)) as u16)
}
#[cfg(feature = "step_trait")]
pub(crate) fn steps_between_impl(start: &Self, end: &Self) -> (usize, Option<usize>) {
if let Some(steps) = Self::steps_between_u64(start, end) {
let steps = usize::try_from(steps).ok();
(steps.unwrap_or(usize::MAX), steps)
} else {
(0, None)
}
}
#[cfg(any(feature = "instructions", feature = "step_trait"))]
pub(crate) fn steps_between_u64(start: &Self, end: &Self) -> Option<u64> {
let mut steps = end.0.checked_sub(start.0)?;
steps &= 0xffff_ffff_ffff;
Some(steps)
}
#[inline]
pub(crate) fn forward_checked_impl(start: Self, count: usize) -> Option<Self> {
Self::forward_checked_u64(start, u64::try_from(count).ok()?)
}
#[inline]
pub(crate) fn forward_checked_u64(start: Self, count: u64) -> Option<Self> {
if count > ADDRESS_SPACE_SIZE {
return None;
}
let mut addr = start.0.checked_add(count)?;
match addr.get_bits(47..) {
0x1 => {
addr.set_bits(47.., 0x1ffff);
}
0x2 => {
return None;
}
_ => {}
}
Some(unsafe { Self::new_unsafe(addr) })
}
#[cfg(feature = "step_trait")]
#[inline]
pub(crate) fn backward_checked_u64(start: Self, count: u64) -> Option<Self> {
if count > ADDRESS_SPACE_SIZE {
return None;
}
let mut addr = start.0.checked_sub(count)?;
match addr.get_bits(47..) {
0x1fffe => {
addr.set_bits(47.., 0);
}
0x1fffd => {
return None;
}
_ => {}
}
Some(unsafe { Self::new_unsafe(addr) })
}
}
impl fmt::Debug for VirtAddr {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
f.debug_tuple("VirtAddr")
.field(&format_args!("{:#x}", self.0))
.finish()
}
}
impl fmt::Binary for VirtAddr {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
fmt::Binary::fmt(&self.0, f)
}
}
impl fmt::LowerHex for VirtAddr {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
fmt::LowerHex::fmt(&self.0, f)
}
}
impl fmt::Octal for VirtAddr {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
fmt::Octal::fmt(&self.0, f)
}
}
impl fmt::UpperHex for VirtAddr {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
fmt::UpperHex::fmt(&self.0, f)
}
}
impl fmt::Pointer for VirtAddr {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
fmt::Pointer::fmt(&(self.0 as *const ()), f)
}
}
impl Add<u64> for VirtAddr {
type Output = Self;
#[cfg_attr(not(feature = "step_trait"), allow(rustdoc::broken_intra_doc_links))]
#[inline]
fn add(self, rhs: u64) -> Self::Output {
VirtAddr::try_new(
self.0
.checked_add(rhs)
.expect("attempt to add with overflow"),
)
.expect("attempt to add resulted in non-canonical virtual address")
}
}
impl AddAssign<u64> for VirtAddr {
#[cfg_attr(not(feature = "step_trait"), allow(rustdoc::broken_intra_doc_links))]
#[inline]
fn add_assign(&mut self, rhs: u64) {
*self = *self + rhs;
}
}
impl Sub<u64> for VirtAddr {
type Output = Self;
#[cfg_attr(not(feature = "step_trait"), allow(rustdoc::broken_intra_doc_links))]
#[inline]
fn sub(self, rhs: u64) -> Self::Output {
VirtAddr::try_new(
self.0
.checked_sub(rhs)
.expect("attempt to subtract with overflow"),
)
.expect("attempt to subtract resulted in non-canonical virtual address")
}
}
impl SubAssign<u64> for VirtAddr {
#[cfg_attr(not(feature = "step_trait"), allow(rustdoc::broken_intra_doc_links))]
#[inline]
fn sub_assign(&mut self, rhs: u64) {
*self = *self - rhs;
}
}
impl Sub<VirtAddr> for VirtAddr {
type Output = u64;
#[inline]
fn sub(self, rhs: VirtAddr) -> Self::Output {
self.as_u64()
.checked_sub(rhs.as_u64())
.expect("attempt to subtract with overflow")
}
}
#[cfg(feature = "step_trait")]
impl Step for VirtAddr {
#[inline]
fn steps_between(start: &Self, end: &Self) -> (usize, Option<usize>) {
Self::steps_between_impl(start, end)
}
#[inline]
fn forward_checked(start: Self, count: usize) -> Option<Self> {
Self::forward_checked_impl(start, count)
}
#[inline]
fn backward_checked(start: Self, count: usize) -> Option<Self> {
Self::backward_checked_u64(start, u64::try_from(count).ok()?)
}
}
pub struct PhysAddrNotValid(pub u64);
impl core::fmt::Debug for PhysAddrNotValid {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
f.debug_tuple("PhysAddrNotValid")
.field(&format_args!("{:#x}", self.0))
.finish()
}
}
impl PhysAddr {
#[inline]
#[const_fn(cfg(not(feature = "memory_encryption")))]
pub const fn new(addr: u64) -> Self {
match Self::try_new(addr) {
Ok(p) => p,
Err(_) => panic!("physical addresses must not have any bits in the range 52 to 64 set"),
}
}
#[cfg(not(feature = "memory_encryption"))]
#[inline]
pub const fn new_truncate(addr: u64) -> PhysAddr {
PhysAddr(addr % (1 << 52))
}
#[cfg(feature = "memory_encryption")]
#[inline]
pub fn new_truncate(addr: u64) -> PhysAddr {
PhysAddr((addr % (1 << 52)) & !ENC_BIT_MASK.load(Ordering::Relaxed))
}
#[inline]
pub const unsafe fn new_unsafe(addr: u64) -> PhysAddr {
PhysAddr(addr)
}
#[inline]
#[const_fn(cfg(not(feature = "memory_encryption")))]
pub const fn try_new(addr: u64) -> Result<Self, PhysAddrNotValid> {
let p = Self::new_truncate(addr);
if p.0 == addr {
Ok(p)
} else {
Err(PhysAddrNotValid(addr))
}
}
#[inline]
pub const fn zero() -> PhysAddr {
PhysAddr(0)
}
#[inline]
pub const fn as_u64(self) -> u64 {
self.0
}
#[inline]
pub const fn is_null(self) -> bool {
self.0 == 0
}
#[inline]
pub fn align_up<U>(self, align: U) -> Self
where
U: Into<u64>,
{
PhysAddr::new(align_up(self.0, align.into()))
}
#[inline]
pub fn align_down<U>(self, align: U) -> Self
where
U: Into<u64>,
{
self.align_down_u64(align.into())
}
#[inline]
pub(crate) const fn align_down_u64(self, align: u64) -> Self {
PhysAddr(align_down(self.0, align))
}
#[inline]
pub fn is_aligned<U>(self, align: U) -> bool
where
U: Into<u64>,
{
self.is_aligned_u64(align.into())
}
#[inline]
pub(crate) const fn is_aligned_u64(self, align: u64) -> bool {
self.align_down_u64(align).as_u64() == self.as_u64()
}
}
impl fmt::Debug for PhysAddr {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
f.debug_tuple("PhysAddr")
.field(&format_args!("{:#x}", self.0))
.finish()
}
}
impl fmt::Binary for PhysAddr {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
fmt::Binary::fmt(&self.0, f)
}
}
impl fmt::LowerHex for PhysAddr {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
fmt::LowerHex::fmt(&self.0, f)
}
}
impl fmt::Octal for PhysAddr {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
fmt::Octal::fmt(&self.0, f)
}
}
impl fmt::UpperHex for PhysAddr {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
fmt::UpperHex::fmt(&self.0, f)
}
}
impl fmt::Pointer for PhysAddr {
#[inline]
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
fmt::Pointer::fmt(&(self.0 as *const ()), f)
}
}
impl Add<u64> for PhysAddr {
type Output = Self;
#[inline]
fn add(self, rhs: u64) -> Self::Output {
PhysAddr::new(self.0.checked_add(rhs).unwrap())
}
}
impl AddAssign<u64> for PhysAddr {
#[inline]
fn add_assign(&mut self, rhs: u64) {
*self = *self + rhs;
}
}
impl Sub<u64> for PhysAddr {
type Output = Self;
#[inline]
fn sub(self, rhs: u64) -> Self::Output {
PhysAddr::new(self.0.checked_sub(rhs).unwrap())
}
}
impl SubAssign<u64> for PhysAddr {
#[inline]
fn sub_assign(&mut self, rhs: u64) {
*self = *self - rhs;
}
}
impl Sub<PhysAddr> for PhysAddr {
type Output = u64;
#[inline]
fn sub(self, rhs: PhysAddr) -> Self::Output {
self.as_u64().checked_sub(rhs.as_u64()).unwrap()
}
}
#[inline]
pub const fn align_down(addr: u64, align: u64) -> u64 {
assert!(align.is_power_of_two(), "`align` must be a power of two");
addr & !(align - 1)
}
#[inline]
pub const fn align_up(addr: u64, align: u64) -> u64 {
assert!(align.is_power_of_two(), "`align` must be a power of two");
let align_mask = align - 1;
if addr & align_mask == 0 {
addr } else {
if let Some(aligned) = (addr | align_mask).checked_add(1) {
aligned
} else {
panic!("attempt to add with overflow")
}
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
#[should_panic]
pub fn add_overflow_virtaddr() {
let _ = VirtAddr::new(0xffff_ffff_ffff_ffff) + 1;
}
#[test]
#[should_panic]
pub fn add_overflow_physaddr() {
let _ = PhysAddr::new(0x000f_ffff_ffff_ffff) + 0xffff_0000_0000_0000;
}
#[test]
#[should_panic]
pub fn sub_underflow_virtaddr() {
let _ = VirtAddr::new(0) - 1;
}
#[test]
#[should_panic]
pub fn sub_overflow_physaddr() {
let _ = PhysAddr::new(0) - 1;
}
#[test]
pub fn virtaddr_new_truncate() {
assert_eq!(VirtAddr::new_truncate(0), VirtAddr(0));
assert_eq!(VirtAddr::new_truncate(1 << 47), VirtAddr(0xfffff << 47));
assert_eq!(VirtAddr::new_truncate(123), VirtAddr(123));
assert_eq!(VirtAddr::new_truncate(123 << 47), VirtAddr(0xfffff << 47));
}
#[test]
#[cfg(feature = "step_trait")]
fn virtaddr_step_forward() {
assert_eq!(Step::forward(VirtAddr(0), 0), VirtAddr(0));
assert_eq!(Step::forward(VirtAddr(0), 1), VirtAddr(1));
assert_eq!(
Step::forward(VirtAddr(0x7fff_ffff_ffff), 1),
VirtAddr(0xffff_8000_0000_0000)
);
assert_eq!(
Step::forward(VirtAddr(0xffff_8000_0000_0000), 1),
VirtAddr(0xffff_8000_0000_0001)
);
assert_eq!(
Step::forward_checked(VirtAddr(0xffff_ffff_ffff_ffff), 1),
None
);
#[cfg(target_pointer_width = "64")]
assert_eq!(
Step::forward(VirtAddr(0x7fff_ffff_ffff), 0x1234_5678_9abd),
VirtAddr(0xffff_9234_5678_9abc)
);
#[cfg(target_pointer_width = "64")]
assert_eq!(
Step::forward(VirtAddr(0x7fff_ffff_ffff), 0x8000_0000_0000),
VirtAddr(0xffff_ffff_ffff_ffff)
);
#[cfg(target_pointer_width = "64")]
assert_eq!(
Step::forward(VirtAddr(0x7fff_ffff_ff00), 0x8000_0000_00ff),
VirtAddr(0xffff_ffff_ffff_ffff)
);
#[cfg(target_pointer_width = "64")]
assert_eq!(
Step::forward_checked(VirtAddr(0x7fff_ffff_ff00), 0x8000_0000_0100),
None
);
#[cfg(target_pointer_width = "64")]
assert_eq!(
Step::forward_checked(VirtAddr(0x7fff_ffff_ffff), 0x8000_0000_0001),
None
);
}
#[test]
#[cfg(feature = "step_trait")]
fn virtaddr_step_backward() {
assert_eq!(Step::backward(VirtAddr(0), 0), VirtAddr(0));
assert_eq!(Step::backward_checked(VirtAddr(0), 1), None);
assert_eq!(Step::backward(VirtAddr(1), 1), VirtAddr(0));
assert_eq!(
Step::backward(VirtAddr(0xffff_8000_0000_0000), 1),
VirtAddr(0x7fff_ffff_ffff)
);
assert_eq!(
Step::backward(VirtAddr(0xffff_8000_0000_0001), 1),
VirtAddr(0xffff_8000_0000_0000)
);
#[cfg(target_pointer_width = "64")]
assert_eq!(
Step::backward(VirtAddr(0xffff_9234_5678_9abc), 0x1234_5678_9abd),
VirtAddr(0x7fff_ffff_ffff)
);
#[cfg(target_pointer_width = "64")]
assert_eq!(
Step::backward(VirtAddr(0xffff_8000_0000_0000), 0x8000_0000_0000),
VirtAddr(0)
);
#[cfg(target_pointer_width = "64")]
assert_eq!(
Step::backward(VirtAddr(0xffff_8000_0000_0000), 0x7fff_ffff_ff01),
VirtAddr(0xff)
);
#[cfg(target_pointer_width = "64")]
assert_eq!(
Step::backward_checked(VirtAddr(0xffff_8000_0000_0000), 0x8000_0000_0001),
None
);
}
#[test]
#[cfg(feature = "step_trait")]
fn virtaddr_steps_between() {
assert_eq!(
Step::steps_between(&VirtAddr(0), &VirtAddr(0)),
(0, Some(0))
);
assert_eq!(
Step::steps_between(&VirtAddr(0), &VirtAddr(1)),
(1, Some(1))
);
assert_eq!(Step::steps_between(&VirtAddr(1), &VirtAddr(0)), (0, None));
assert_eq!(
Step::steps_between(
&VirtAddr(0x7fff_ffff_ffff),
&VirtAddr(0xffff_8000_0000_0000)
),
(1, Some(1))
);
assert_eq!(
Step::steps_between(
&VirtAddr(0xffff_8000_0000_0000),
&VirtAddr(0x7fff_ffff_ffff)
),
(0, None)
);
assert_eq!(
Step::steps_between(
&VirtAddr(0xffff_8000_0000_0000),
&VirtAddr(0xffff_8000_0000_0000)
),
(0, Some(0))
);
assert_eq!(
Step::steps_between(
&VirtAddr(0xffff_8000_0000_0000),
&VirtAddr(0xffff_8000_0000_0001)
),
(1, Some(1))
);
assert_eq!(
Step::steps_between(
&VirtAddr(0xffff_8000_0000_0001),
&VirtAddr(0xffff_8000_0000_0000)
),
(0, None)
);
#[cfg(target_pointer_width = "64")]
assert_eq!(
Step::steps_between(&VirtAddr(0), &VirtAddr(0x1_0000_0000)),
(0x1_0000_0000, Some(0x1_0000_0000))
);
#[cfg(not(target_pointer_width = "64"))]
assert_eq!(
Step::steps_between(&VirtAddr(0), &VirtAddr(0x1_0000_0000)),
(usize::MAX, None)
);
}
#[test]
pub fn test_align_up() {
assert_eq!(align_up(0, 1), 0);
assert_eq!(align_up(1234, 1), 1234);
assert_eq!(align_up(0xffff_ffff_ffff_ffff, 1), 0xffff_ffff_ffff_ffff);
assert_eq!(align_up(0, 2), 0);
assert_eq!(align_up(1233, 2), 1234);
assert_eq!(align_up(0xffff_ffff_ffff_fffe, 2), 0xffff_ffff_ffff_fffe);
assert_eq!(align_up(0, 128), 0);
assert_eq!(align_up(0, 1), 0);
assert_eq!(align_up(0, 2), 0);
assert_eq!(align_up(0, 0x8000_0000_0000_0000), 0);
}
#[test]
fn test_virt_addr_align_up() {
assert_eq!(
VirtAddr::new(0x7fff_ffff_ffff).align_up(2u64),
VirtAddr::new(0xffff_8000_0000_0000)
);
}
#[test]
fn test_virt_addr_align_down() {
assert_eq!(
VirtAddr::new(0xffff_8000_0000_0000).align_down(1u64 << 48),
VirtAddr::new(0)
);
}
#[test]
#[should_panic]
fn test_virt_addr_align_up_overflow() {
VirtAddr::new(0xffff_ffff_ffff_ffff).align_up(2u64);
}
#[test]
#[should_panic]
fn test_phys_addr_align_up_overflow() {
PhysAddr::new(0x000f_ffff_ffff_ffff).align_up(2u64);
}
#[test]
#[cfg(target_pointer_width = "64")]
fn test_from_ptr_array() {
let slice = &[1, 2, 3, 4, 5];
assert_eq!(
VirtAddr::from_ptr(slice.as_slice()),
VirtAddr::from_ptr(&slice[0])
);
}
}
#[cfg(kani)]
mod proofs {
use super::*;
#[kani::proof]
fn forward_base_case() {
let start_raw: u64 = kani::any();
let Ok(start) = VirtAddr::try_new(start_raw) else {
return;
};
let same = Step::forward(start, 0);
assert!(start == same);
let expected = match start_raw {
0x0000_0000_0000_0000..=0x0000_7fff_ffff_fffe => Some(start_raw + 1),
0x0000_7fff_ffff_ffff => Some(0xffff_8000_0000_0000),
0x0000_8000_0000_0000..=0xffff_7fff_ffff_ffff => unreachable!(),
0xffff_8000_0000_0000..=0xffff_ffff_ffff_fffe => Some(start_raw + 1),
0xffff_ffff_ffff_ffff => None,
};
if let Some(expected) = expected {
assert!(VirtAddr::try_new(expected).is_ok());
}
let next = Step::forward_checked(start, 1);
assert!(next.map(VirtAddr::as_u64) == expected);
}
#[kani::proof]
fn forward_induction_step() {
let start_raw: u64 = kani::any();
let Ok(start) = VirtAddr::try_new(start_raw) else {
return;
};
let count1: usize = kani::any();
let count2: usize = kani::any();
let Some(next1) = Step::forward_checked(start, count1) else {
return;
};
let Some(next2) = Step::forward_checked(next1, count2) else {
return;
};
let count_both = count1 + count2;
let next_both = Step::forward(start, count_both);
assert!(next2 == next_both);
}
#[kani::proof]
fn forward_implies_backward() {
let start_raw: u64 = kani::any();
let Ok(start) = VirtAddr::try_new(start_raw) else {
return;
};
let count: usize = kani::any();
let Some(end) = Step::forward_checked(start, count) else {
return;
};
let start2 = Step::backward(end, count);
assert!(start == start2);
}
#[kani::proof]
fn backward_implies_forward() {
let end_raw: u64 = kani::any();
let Ok(end) = VirtAddr::try_new(end_raw) else {
return;
};
let count: usize = kani::any();
let Some(start) = Step::backward_checked(end, count) else {
return;
};
let end2 = Step::forward(start, count);
assert!(end == end2);
}
#[kani::proof]
fn forward_implies_steps_between() {
let start: u64 = kani::any();
let Ok(start) = VirtAddr::try_new(start) else {
return;
};
let count: usize = kani::any();
let Some(end) = Step::forward_checked(start, count) else {
return;
};
assert!(Step::steps_between(&start, &end) == (count, Some(count)));
}
#[kani::proof]
fn steps_between_implies_forward() {
let start: u64 = kani::any();
let Ok(start) = VirtAddr::try_new(start) else {
return;
};
let end: u64 = kani::any();
let Ok(end) = VirtAddr::try_new(end) else {
return;
};
let Some(count) = Step::steps_between(&start, &end).1 else {
return;
};
assert!(Step::forward(start, count) == end);
}
}