WIP: kani proofs

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

Author: bchalios

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

@@ -486,13 +486,6 @@ mod verification {
         kani::assume(offset.checked_add(len).is_some());
 
         let regions = arch_memory_regions(offset as usize, len as usize);
-        for region in &regions {
-            println!(
-                "region: [{:x},{:x})",
-                region.0.0,
-                region.0.0 + region.1 as u64
-            );
-        }
 
         // There are two MMIO gaps, so we can get either 1, 2 or 3 regions
         assert!(regions.len() <= 3);
@@ -520,12 +513,16 @@ mod verification {
         // 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 the 32bit MMIO gap
+        // If there's at least two regions, they perfectly snuggle up to one of the two MMIO gaps
         if regions.len() >= 2 {
             kani::cover!();
 
-            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 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);
+            }
         }
 
         // If there are three regions, the last two perfectly snuggle up to the 64bit