WIP: kani proofs

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

Author: bchalios

src/vmm/src/arch/mod.rs

@@ -132,6 +132,9 @@ fn arch_memory_regions_with_gap(
     gap_start: usize,
     gap_size: usize,
 ) -> Option<(usize, usize)> {
+    // 0-sized gaps don't really make sense. We should never receive such a gap.
+    assert!(gap_size > 0);
+
     let first_addr_past_gap = gap_start + gap_size;
     match (size + offset).checked_sub(gap_start) {
         // case0: region fits all before gap

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

@@ -477,7 +477,7 @@ mod verification {
     };
 
     #[kani::proof]
-    #[kani::unwind(3)]
+    #[kani::unwind(4)]
     fn verify_arch_memory_regions() {
         let offset: u64 = kani::any::<u64>();
         let len: u64 = kani::any::<u64>();
@@ -486,6 +486,13 @@ 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);