WIP: kani proofs

Signed-off-by: Babis Chalios <[email protected]>

Author: bchalios

src/vmm/src/arch/aarch64/mod.rs

@@ -53,26 +53,15 @@ pub enum ConfigurationError {
 
 /// Returns a Vec of the valid memory addresses for aarch64.
 /// See [`layout`](layout) module for a drawing of the specific memory model for this platform.
-///
-/// The `offset` parameter specified the offset from [`layout::DRAM_MEM_START`].
-pub fn arch_memory_regions(offset: usize, size: usize) -> Vec<(GuestAddress, usize)> {
+pub fn arch_memory_regions(size: usize) -> Vec<(GuestAddress, usize)> {
     assert!(size > 0, "Attempt to allocate guest memory of length 0");
-    assert!(
-        offset.checked_add(size).is_some(),
-        "Attempt to allocate guest memory such that the address space would wrap around"
-    );
-    assert!(
-        offset < layout::DRAM_MEM_MAX_SIZE,
-        "offset outside allowed DRAM range"
-    );
 
-    let dram_size = min(size, layout::DRAM_MEM_MAX_SIZE - offset);
+    let dram_size = min(size, layout::DRAM_MEM_MAX_SIZE);
 
     if dram_size != size {
         logger::warn!(
-            "Requested offset/memory size {}/{} exceeds architectural maximum (1022GiB). Size has \
+            "Requested offset/memory size {} exceeds architectural maximum (1022GiB). Size has \
              been truncated to {}",
-            offset,
             size,
             dram_size
         );
@@ -81,7 +70,7 @@ pub fn arch_memory_regions(offset: usize, size: usize) -> Vec<(GuestAddress, usi
     let mut regions = vec![];
     if let Some((offset, remaining)) = arch_memory_regions_with_gap(
         &mut regions,
-        u64_to_usize(layout::DRAM_MEM_START) + offset,
+        u64_to_usize(layout::DRAM_MEM_START),
         dram_size,
         u64_to_usize(layout::MMIO64_MEM_START),
         u64_to_usize(layout::MMIO64_MEM_SIZE),
@@ -293,15 +282,15 @@ mod tests {
 
     #[test]
     fn test_regions_lt_1024gb() {
-        let regions = arch_memory_regions(0, 1usize << 29);
+        let regions = arch_memory_regions(1usize << 29);
         assert_eq!(1, regions.len());
         assert_eq!(GuestAddress(DRAM_MEM_START), regions[0].0);
         assert_eq!(1usize << 29, regions[0].1);
     }
 
     #[test]
     fn test_regions_gt_1024gb() {
-        let regions = arch_memory_regions(0, 1usize << 41);
+        let regions = arch_memory_regions(1usize << 41);
         assert_eq!(2, regions.len());
         assert_eq!(GuestAddress(DRAM_MEM_START), regions[0].0);
         assert_eq!(MMIO64_MEM_START - DRAM_MEM_START, regions[0].1 as u64);

src/vmm/src/arch/x86_64/layout.rs

@@ -9,6 +9,12 @@
 
 use crate::utils::mib_to_bytes;
 
+/// Maximum physical memory address space.
+///
+/// Typically, x86_64 architecture supports up to 48 bits of physical addresses.
+/// This space includes the MMIO addresses.
+pub const MAX_PHYSICAL_ADDRESS_SPACE: usize = 1usize << 48;
+
 /// Initial stack for the boot CPU.
 pub const BOOT_STACK_POINTER: u64 = 0x8ff0;
 

src/vmm/src/arch/x86_64/mod.rs

@@ -34,8 +34,8 @@ pub mod generated;
 use std::fs::File;
 
 use layout::{
-    CMDLINE_START, FIRST_ADDR_PAST_32BITS, FIRST_ADDR_PAST_64BITS_MMIO, MMIO32_MEM_SIZE,
-    MMIO32_MEM_START, MMIO64_MEM_SIZE, MMIO64_MEM_START,
+    CMDLINE_START, FIRST_ADDR_PAST_32BITS, FIRST_ADDR_PAST_64BITS_MMIO, MAX_PHYSICAL_ADDRESS_SPACE,
+    MMIO32_MEM_SIZE, MMIO32_MEM_START, MMIO64_MEM_SIZE, MMIO64_MEM_START,
 };
 use linux_loader::configurator::linux::LinuxBootConfigurator;
 use linux_loader::configurator::pvh::PvhBootConfigurator;
@@ -101,22 +101,25 @@ pub enum ConfigurationError {
 
 /// Returns a Vec of the valid memory addresses.
 /// These should be used to configure the GuestMemoryMmap structure for the platform.
-/// For x86_64 all addresses are valid from the start of the kernel except a
-/// carve out at the end of 32bit address space.
-pub fn arch_memory_regions(offset: usize, size: usize) -> Vec<(GuestAddress, usize)> {
+/// For x86_64 all addresses are valid from the start of the kernel except an 1GB
+/// carve out at the end of 32bit address space and a second 256GB one at the 256GB limit.
+pub fn arch_memory_regions(size: usize) -> Vec<(GuestAddress, usize)> {
     // If we get here with size == 0 something has seriously gone wrong. Firecracker should never
     // try to allocate guest memory of size 0
     assert!(size > 0, "Attempt to allocate guest memory of length 0");
+    // The resulting address space must fit in 48 bits.
     assert!(
-        offset.checked_add(size).is_some(),
-        "Attempt to allocate guest memory such that the address space would wrap around"
+        size <= MAX_PHYSICAL_ADDRESS_SPACE
+            - u64_to_usize(MMIO32_MEM_SIZE)
+            - u64_to_usize(MMIO64_MEM_SIZE),
+        "Memory size would result in an address space that exceeds 48 bits."
     );
 
     let mut regions = vec![];
 
     if let Some((start_past_32bit_gap, remaining_past_32bit_gap)) = arch_memory_regions_with_gap(
         &mut regions,
-        offset,
+        0,
         size,
         u64_to_usize(MMIO32_MEM_START),
         u64_to_usize(MMIO32_MEM_SIZE),
@@ -471,26 +474,33 @@ pub fn load_kernel(
 
 #[cfg(kani)]
 mod verification {
+
     use crate::arch::arch_memory_regions;
     use crate::arch::x86_64::layout::{
-        FIRST_ADDR_PAST_32BITS, FIRST_ADDR_PAST_64BITS_MMIO, MMIO32_MEM_START, MMIO64_MEM_START,
+        FIRST_ADDR_PAST_32BITS, FIRST_ADDR_PAST_64BITS_MMIO, MAX_PHYSICAL_ADDRESS_SPACE,
+        MMIO32_MEM_SIZE, MMIO32_MEM_START, MMIO64_MEM_SIZE, MMIO64_MEM_START,
     };
+    use crate::utils::usize_to_u64;
 
     #[kani::proof]
     #[kani::unwind(4)]
     fn verify_arch_memory_regions() {
-        let offset: u64 = kani::any::<u64>();
         let len: u64 = kani::any::<u64>();
 
         kani::assume(len > 0);
-        kani::assume(offset.checked_add(len).is_some());
+        kani::assume(
+            len <= usize_to_u64(MAX_PHYSICAL_ADDRESS_SPACE) - MMIO32_MEM_SIZE - MMIO64_MEM_SIZE,
+        );
 
-        let regions = arch_memory_regions(offset as usize, len as usize);
+        let regions = arch_memory_regions(len as usize);
 
         // There are two MMIO gaps, so we can get either 1, 2 or 3 regions
         assert!(regions.len() <= 3);
         assert!(regions.len() >= 1);
 
+        // The first address is always 0
+        assert_eq!(regions[0].0.0, 0);
+
         // The total length of all regions is what we requested
         assert_eq!(
             regions.iter().map(|&(_, len)| len).sum::<usize>(),
@@ -507,23 +517,15 @@ mod verification {
                         || start.0 + len as u64 <= MMIO64_MEM_START))
         );
 
-        // All regions start after our specified offset
-        assert!(regions.iter().all(|&(start, _)| start.0 >= offset as u64));
-
         // All regions have non-zero length
         assert!(regions.iter().all(|&(_, len)| len > 0));
 
         // If there's at least two regions, they perfectly snuggle up to one of the two MMIO gaps
         if regions.len() >= 2 {
             kani::cover!();
 
-            if offset < MMIO32_MEM_START {
-                assert_eq!(regions[0].0.0 + regions[0].1 as u64, MMIO32_MEM_START);
-                assert_eq!(regions[1].0.0, FIRST_ADDR_PAST_32BITS);
-            } else {
-                assert_eq!(regions[0].0.0 + regions[0].1 as u64, MMIO64_MEM_START);
-                assert_eq!(regions[1].0.0, FIRST_ADDR_PAST_64BITS_MMIO);
-            }
+            assert_eq!(regions[0].0.0 + regions[0].1 as u64, MMIO32_MEM_START);
+            assert_eq!(regions[1].0.0, FIRST_ADDR_PAST_32BITS);
         }
 
         // If there are three regions, the last two perfectly snuggle up to the 64bit
@@ -548,34 +550,21 @@ mod tests {
 
     #[test]
     fn regions_lt_4gb() {
-        let regions = arch_memory_regions(0, 1usize << 29);
+        let regions = arch_memory_regions(1usize << 29);
         assert_eq!(1, regions.len());
         assert_eq!(GuestAddress(0), regions[0].0);
         assert_eq!(1usize << 29, regions[0].1);
-
-        let regions = arch_memory_regions(1 << 28, 1 << 29);
-        assert_eq!(1, regions.len());
-        assert_eq!(regions[0], (GuestAddress(1 << 28), 1 << 29));
     }
 
     #[test]
     fn regions_gt_4gb() {
         const MEMORY_SIZE: usize = (1 << 32) + 0x8000;
 
-        let regions = arch_memory_regions(0, MEMORY_SIZE);
+        let regions = arch_memory_regions(MEMORY_SIZE);
         assert_eq!(2, regions.len());
         assert_eq!(GuestAddress(0), regions[0].0);
         assert_eq!(GuestAddress(1u64 << 32), regions[1].0);
 
-        let regions = arch_memory_regions(1 << 31, MEMORY_SIZE);
-        assert_eq!(2, regions.len());
-        assert_eq!(
-            regions[0],
-            (
-                GuestAddress(1 << 31),
-                u64_to_usize(MMIO32_MEM_START) - (1 << 31)
-            )
-        );
         assert_eq!(
             regions[1],
             (

src/vmm/src/resources.rs

@@ -474,7 +474,7 @@ impl VmResources {
         // a single way of backing guest memory for vhost-user and non-vhost-user cases,
         // that would not be worth the effort.
         let regions =
-            crate::arch::arch_memory_regions(0, mib_to_bytes(self.machine_config.mem_size_mib));
+            crate::arch::arch_memory_regions(mib_to_bytes(self.machine_config.mem_size_mib));
         if vhost_user_device_used {
             memory::memfd_backed(
                 regions.as_ref(),

src/vmm/src/test_utils/mod.rs

@@ -58,11 +58,11 @@ pub fn multi_region_mem_raw(regions: &[(GuestAddress, usize)]) -> Vec<GuestRegio
 /// Creates a [`GuestMemoryMmap`] of the given size with the contained regions laid out in
 /// accordance with the requirements of the architecture on which the tests are being run.
 pub fn arch_mem(mem_size_bytes: usize) -> GuestMemoryMmap {
-    multi_region_mem(&crate::arch::arch_memory_regions(0, mem_size_bytes))
+    multi_region_mem(&crate::arch::arch_memory_regions(mem_size_bytes))
 }
 
 pub fn arch_mem_raw(mem_size_bytes: usize) -> Vec<GuestRegionMmap> {
-    multi_region_mem_raw(&crate::arch::arch_memory_regions(0, mem_size_bytes))
+    multi_region_mem_raw(&crate::arch::arch_memory_regions(mem_size_bytes))
 }
 
 pub fn create_vmm(