WIP: kani proofs

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

Author: bchalios

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

@@ -81,7 +81,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,
-        usize::try_from(layout::DRAM_MEM_START).unwrap() + offset,
+        u64_to_usize(layout::DRAM_MEM_START) + offset,
         dram_size,
         u64_to_usize(layout::MMIO64_MEM_START),
         u64_to_usize(layout::MMIO64_MEM_SIZE),
@@ -222,14 +222,14 @@ mod verification {
     #[kani::proof]
     #[kani::unwind(3)]
     fn verify_arch_memory_regions() {
-        let offset: u64 = kani::any::<u64>();
-        let len: u64 = kani::any::<u64>();
+        let offset: u64 = kani::any::<usize>();
+        let len: u64 = kani::any::<usize>();
 
         kani::assume(len > 0);
         kani::assume(offset.checked_add(len).is_some());
-        kani::assume(offset < DRAM_MEM_MAX_SIZE as u64);
+        kani::assume(offset < DRAM_MEM_MAX_SIZE);
 
-        let regions = arch_memory_regions(offset as usize, len as usize);
+        let regions = arch_memory_regions(offset, len);
 
         for region in &regions {
             println!(
@@ -248,10 +248,10 @@ mod verification {
         let actual_len = regions.iter().map(|&(_, len)| len).sum::<usize>();
         assert!(actual_len <= DRAM_MEM_MAX_SIZE);
         // The total length is smaller or equal to the length we asked
-        assert!((actual_len as u64) <= len);
+        assert!(actual_len <= len);
         // If it's smaller, it's because we asked more than the the maximum possible.
-        if (actual_len as u64) < len {
-            assert!(offset + len >= DRAM_MEM_MAX_SIZE as u64);
+        if (actual_len) < len {
+            assert!(offset + len >= DRAM_MEM_MAX_SIZE);
         }
 
         // No region overlaps the 64-bit MMIO gap

src/vmm/src/arch/mod.rs

@@ -144,10 +144,7 @@ fn arch_memory_regions_with_gap(
         }
         // case1: region starts before the gap and goes past it
         Some(remaining) if offset < gap_start => {
-            regions.push((
-                GuestAddress(offset as u64),
-                u64_to_usize(gap_start as u64) - offset,
-            ));
+            regions.push((GuestAddress(offset as u64), gap_start - offset));
             Some((first_addr_past_gap, remaining))
         }
         // case2: region starts past the gap