Fix kani modules

Addressing comments in PR. Mainly kani module fixes.

Signed-off-by: brandonpike <bpike@amazon.com>

src/vmm/src/devices/virtio/iovec.rs

@@ -613,7 +613,6 @@ mod verification {
 
     use libc::{c_void, iovec};
     use vm_memory::bitmap::BitmapSlice;
-    use vm_memory::volatile_memory::Error;
     use vm_memory::VolatileSlice;
 
     use super::{IoVecBuffer, IoVecBufferMut, IoVecVec};
@@ -628,10 +627,10 @@ mod verification {
     // >= 1.
     const MAX_DESC_LENGTH: usize = 4;
 
-    fn create_iovecs(mem: *mut u8, size: usize) -> (IoVecVec, usize) {
+    fn create_iovecs(mem: *mut u8, size: usize) -> (IoVecVec, u32) {
         let nr_descs: usize = kani::any_where(|&n| n <= MAX_DESC_LENGTH);
         let mut vecs: Vec<iovec> = Vec::with_capacity(nr_descs);
-        let mut len = 0usize;
+        let mut len = 0u32;
         for _ in 0..nr_descs {
             // The `IoVecBuffer(Mut)` constructors ensure that the memory region described by every
             // `Descriptor` in the chain is a valid, i.e. it is memory with then guest's memory
@@ -643,7 +642,7 @@ mod verification {
             let iov_base = unsafe { mem.offset(addr.try_into().unwrap()) } as *mut c_void;
 
             vecs.push(iovec { iov_base, iov_len });
-            len += iov_len;
+            len += u32::try_from(iov_len).unwrap();
         }
 
         (vecs, len)
@@ -718,7 +717,7 @@ mod verification {
         let iov: IoVecBuffer = kani::any();
 
         let mut buf = vec![0; GUEST_MEMORY_SIZE];
-        let offset: usize = kani::any();
+        let offset: u32 = kani::any();
 
         // We can't really check the contents that the operation here writes into `buf`, because
         // our `IoVecBuffer` being completely arbitrary can contain overlapping memory regions, so
@@ -730,9 +729,13 @@ mod verification {
         // Furthermore, we know our Read-/WriteVolatile implementation above is infallible, so
         // provided that the logic inside read_volatile_at is correct, we should always get Ok(...)
         assert_eq!(
-            iov.read_volatile_at(&mut KaniBuffer(&mut buf), offset, GUEST_MEMORY_SIZE)
-                .unwrap(),
-            buf.len().min(iov.len().saturating_sub(offset))
+            iov.read_volatile_at(
+                &mut KaniBuffer(&mut buf),
+                offset as usize,
+                GUEST_MEMORY_SIZE
+            )
+            .unwrap(),
+            buf.len().min(iov.len().saturating_sub(offset) as usize)
         );
     }
 
@@ -743,7 +746,7 @@ mod verification {
         let mut iov_mut: IoVecBufferMut = kani::any();
 
         let mut buf = kani::vec::any_vec::<u8, GUEST_MEMORY_SIZE>();
-        let offset: usize = kani::any();
+        let offset: u32 = kani::any();
 
         // We can't really check the contents that the operation here writes into `IoVecBufferMut`,
         // because our `IoVecBufferMut` being completely arbitrary can contain overlapping memory
@@ -756,9 +759,13 @@ mod verification {
         // provided that the logic inside write_volatile_at is correct, we should always get Ok(...)
         assert_eq!(
             iov_mut
-                .write_volatile_at(&mut KaniBuffer(&mut buf), offset, GUEST_MEMORY_SIZE)
+                .write_volatile_at(
+                    &mut KaniBuffer(&mut buf),
+                    offset as usize,
+                    GUEST_MEMORY_SIZE
+                )
                 .unwrap(),
-            buf.len().min(iov_mut.len().saturating_sub(offset))
+            buf.len().min(iov_mut.len().saturating_sub(offset) as usize)
         );
     }
 }

src/vmm/src/devices/virtio/net/tap.rs

@@ -363,7 +363,7 @@ pub mod tests {
 
         tap.write_iovec(&scattered).unwrap();
 
-        let mut read_buf = vec![0u8; scattered.len().try_into().unwrap()];
+        let mut read_buf = vec![0u8; scattered.len() as usize];
         assert!(tap_traffic_simulator.pop_rx_packet(&mut read_buf));
         assert_eq!(
             &read_buf[..PAYLOAD_SIZE - VNET_HDR_SIZE],

src/vmm/src/devices/virtio/vsock/packet.rs

@@ -139,7 +139,7 @@ impl VsockPacket {
             return Err(VsockError::InvalidPktLen(hdr.len));
         }
 
-        if (hdr.len) > buffer.len() - VSOCK_PKT_HDR_SIZE {
+        if hdr.len > buffer.len() - VSOCK_PKT_HDR_SIZE {
             return Err(VsockError::DescChainTooShortForPacket(
                 buffer.len(),
                 hdr.len,