Repository: firecracker-microvm/firecracker
File: src/vmm/src/devices/virtio/queue.rs (Rust)

Code before:
    fn verify_is_empty() {
        let ProofContext(queue, _) = kani::any();

        assert_eq!(queue.len() == 0, queue.is_empty());
    }

    #[kani::proof]
    #[kani::unwind(0)]
    #[kani::solver(cadical)]
    fn verify_is_valid() {
        let ProofContext(queue, mem) = kani::any();

        if queue.is_valid(&mem) {
            // Section 2.6: Alignment of descriptor table, available ring and used ring; size of
            // queue
            fn alignment_of(val: u64) -> u64 {
                if val == 0 { u64::MAX } else { val & (!val + 1) }
            }

            assert!(alignment_of(queue.desc_table_address.0) >= 16);
            assert!(alignment_of(queue.avail_ring_address.0) >= 2);
            assert!(alignment_of(queue.used_ring_address.0) >= 4);

            // length of queue must be power-of-two, and at most 2^15
            assert_eq!(queue.size.count_ones(), 1);
            assert!(queue.size <= 1u16 << 15);
        }
    }

    #[kani::proof]
    #[kani::unwind(0)]
    fn verify_actual_size() {
        let ProofContext(queue, _) = kani::any();

        assert!(queue.actual_size() <= queue.get_max_size());
        assert!(queue.actual_size() <= queue.size);
    }

    #[kani::proof]
    #[kani::unwind(0)]
    fn verify_avail_ring_idx_get() {
        let ProofContext(queue, _) = kani::any();
        _ = queue.avail_ring_idx_get();
    }

    #[kani::proof]
    #[kani::unwind(0)]
    fn verify_avail_ring_ring_get() {
        let ProofContext(queue, _) = kani::any();
        let x: usize = kani::any_where(|x| *x < usize::from(queue.size));
        unsafe { _ = queue.avail_ring_ring_get(x) };

Review comment (suggestion):
the second assertion is very useless now, but actually the entire harness can be deleted, as it just tests the mock now. But I'll handle this in a follow up, no need to fix here

Code after:

        if queue.is_valid(&mem) {
            // Section 2.6: Alignment of descriptor table, available ring and used ring; size of
            // queue
            fn alignment_of(val: u64) -> u64 {
                if val == 0 { u64::MAX } else { val & (!val + 1) }
            }

            assert!(alignment_of(queue.desc_table_address.0) >= 16);
            assert!(alignment_of(queue.avail_ring_address.0) >= 2);
            assert!(alignment_of(queue.used_ring_address.0) >= 4);

            // length of queue must be power-of-two, and at most 2^15
            assert_eq!(queue.size.count_ones(), 1);
            assert!(queue.size <= 1u16 << 15);
        }
    }

    #[kani::proof]
    #[kani::unwind(0)]
    fn verify_size() {
        let ProofContext(queue, _) = kani::any();

        assert!(queue.size <= queue.max_size);
        assert!(queue.size <= queue.size);
    }

    #[kani::proof]
    #[kani::unwind(0)]
    fn verify_avail_ring_idx_get() {
        let ProofContext(queue, _) = kani::any();
        _ = queue.avail_ring_idx_get();
    }

    #[kani::proof]
    #[kani::unwind(0)]
    fn verify_avail_ring_ring_get() {
        let ProofContext(queue, _) = kani::any();
        let x: usize = kani::any_where(|x| *x < usize::from(queue.size));
        unsafe { _ = queue.avail_ring_ring_get(x) };
    }

    #[kani::proof]
    #[kani::unwind(0)]
    fn verify_avail_ring_used_event_get() {
        let ProofContext(queue, _) = kani::any();
        _ = queue.avail_ring_used_event_get();
    }

    #[kani::proof]
    #[kani::unwind(0)]