From 081321ae1f166d45b03db77146d0f7b1a8c24a8f Mon Sep 17 00:00:00 2001 From: Patrick Roy Date: Mon, 20 Jan 2025 06:44:57 +0000 Subject: [PATCH] fix: clarify comments in kani module QUEUE_END is the address of the first byte past the end of our queue indeed, but the queue doesnt start at 0 (it starts at QUEUE_BASE_ADDRESS, which is 512), and thus GUEST_MEMORY_SIZE was 512 byte too large, because it assumed QUEUE_END was also the size of the queue. Closes #4997 Reported-by: Matias Ezequiel Vara Larsen Signed-off-by: Patrick Roy --- src/vmm/src/devices/virtio/queue.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/vmm/src/devices/virtio/queue.rs b/src/vmm/src/devices/virtio/queue.rs index 7f595d7d9f7..d84c4988d62 100644 --- a/src/vmm/src/devices/virtio/queue.rs +++ b/src/vmm/src/devices/virtio/queue.rs @@ -803,10 +803,11 @@ mod verification { const GUEST_MEMORY_BASE: u64 = 512; // We size our guest memory to fit a properly aligned queue, plus some wiggles bytes - // to make sure we not only test queues where all segments are consecutively aligned. + // to make sure we not only test queues where all segments are consecutively aligned (at least + // for those proofs that use a completely arbitrary queue structure). // We need to give at least 16 bytes of buffer space for the descriptor table to be // able to change its address, as it is 16-byte aligned. - const GUEST_MEMORY_SIZE: usize = QUEUE_END as usize + 30; + const GUEST_MEMORY_SIZE: usize = (QUEUE_END - QUEUE_BASE_ADDRESS) as usize + 30; fn guest_memory(memory: *mut u8) -> ProofGuestMemory { // Ideally, we'd want to do @@ -876,8 +877,7 @@ mod verification { const USED_RING_BASE_ADDRESS: u64 = AVAIL_RING_BASE_ADDRESS + 6 + 2 * FIRECRACKER_MAX_QUEUE_SIZE as u64 + 2; - /// The address of the first byte after the queue. Since our queue starts at guest physical - /// address 0, this is also the size of the memory area occupied by the queue. + /// The address of the first byte after the queue (which starts at QUEUE_BASE_ADDRESS). /// Note that the used ring structure has size 6 + 8 * FIRECRACKER_MAX_QUEUE_SIZE const QUEUE_END: u64 = USED_RING_BASE_ADDRESS + 6 + 8 * FIRECRACKER_MAX_QUEUE_SIZE as u64;