Skip to content

Commit

Permalink
kani: improve performance
Browse files Browse the repository at this point in the history
The `verify_read_from_iovec` and especially `verify_write_from_iovec`
harnesses started taking upwards of 30 minutes for verification.
Optimize them down to take less than 1 minute without losing generality.

Achieve this by applying something akin to loop-unrolling: Instead of
having a `let nr_desc: usize = kani::any_where(...)` that limits
`nr_desc` to be at most a fixed constant, use a for loop to explicitly
list all possibilities up to said constant.

Signed-off-by: Patrick Roy <roypat@amazon.co.uk>
  • Loading branch information
roypat committed Sep 3, 2024
1 parent eb4540c commit 2521805
Showing 1 changed file with 61 additions and 55 deletions.
116 changes: 61 additions & 55 deletions src/vmm/src/devices/virtio/iovec.rs
Original file line number Diff line number Diff line change
Expand Up @@ -690,8 +690,7 @@ mod verification {
// >= 1.
const MAX_DESC_LENGTH: usize = 4;

fn create_iovecs(mem: *mut u8, size: usize) -> (IoVecVec, u32) {
let nr_descs: usize = kani::any_where(|&n| n <= MAX_DESC_LENGTH);
fn create_iovecs(mem: *mut u8, size: usize, nr_descs: usize) -> (IoVecVec, u32) {
let mut vecs: Vec<iovec> = Vec::with_capacity(nr_descs);
let mut len = 0u32;
for _ in 0..nr_descs {
Expand All @@ -711,18 +710,18 @@ mod verification {
(vecs, len)
}

impl kani::Arbitrary for IoVecBuffer {
fn any() -> Self {
impl IoVecBuffer {
fn any_of_length(nr_descs: usize) -> Self {
// We only read from `IoVecBuffer`, so create here a guest memory object, with arbitrary
// contents and size up to GUEST_MEMORY_SIZE.
let mut mem = ManuallyDrop::new(kani::vec::exact_vec::<u8, GUEST_MEMORY_SIZE>());
let (vecs, len) = create_iovecs(mem.as_mut_ptr(), mem.len());
let (vecs, len) = create_iovecs(mem.as_mut_ptr(), mem.len(), nr_descs);
Self { vecs, len }
}
}

impl kani::Arbitrary for IoVecBufferMut {
fn any() -> Self {
impl IoVecBufferMut {
fn any_of_length(nr_descs: usize) -> Self {
// We only write into `IoVecBufferMut` objects, so we can simply create a guest memory
// object initialized to zeroes, trying to be nice to Kani.
let mem = unsafe {
Expand All @@ -732,7 +731,7 @@ mod verification {
))
};

let (vecs, len) = create_iovecs(mem, GUEST_MEMORY_SIZE);
let (vecs, len) = create_iovecs(mem, GUEST_MEMORY_SIZE, nr_descs);
Self { vecs, len }
}
}
Expand Down Expand Up @@ -777,58 +776,65 @@ mod verification {
#[kani::unwind(5)]
#[kani::solver(cadical)]
fn verify_read_from_iovec() {
let iov: IoVecBuffer = kani::any();

let mut buf = vec![0; GUEST_MEMORY_SIZE];
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
// checking the data copied is not exactly trivial.
//
// What we can verify is the bytes that we read out from guest memory:
// - `buf.len()`, if `offset + buf.len() < iov.len()`;
// - `iov.len() - offset`, otherwise.
// 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 as usize,
GUEST_MEMORY_SIZE
)
.unwrap(),
buf.len().min(iov.len().saturating_sub(offset) as usize)
);
for nr_descs in 0..MAX_DESC_LENGTH {
let iov = IoVecBuffer::any_of_length(nr_descs);

let mut buf = vec![0; GUEST_MEMORY_SIZE];
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 checking the data copied is not exactly trivial.
//
// What we can verify is the bytes that we read out from guest memory:
// - `buf.len()`, if `offset + buf.len() < iov.len()`;
// - `iov.len() - offset`, otherwise.
// 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 as usize,
GUEST_MEMORY_SIZE
)
.unwrap(),
buf.len().min(iov.len().saturating_sub(offset) as usize)
);
}
}

#[kani::proof]
#[kani::unwind(5)]
#[kani::solver(cadical)]
fn verify_write_to_iovec() {
let mut iov_mut: IoVecBufferMut = kani::any();

let mut buf = kani::vec::any_vec::<u8, GUEST_MEMORY_SIZE>();
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
// regions, so checking the data copied is not exactly trivial.
//
// What we can verify is the bytes that we write into guest memory:
// - `buf.len()`, if `offset + buf.len() < iov.len()`;
// - `iov.len() - offset`, otherwise.
// Furthermore, we know our Read-/WriteVolatile implementation above is infallible, so
// 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 as usize,
GUEST_MEMORY_SIZE
)
.unwrap(),
buf.len().min(iov_mut.len().saturating_sub(offset) as usize)
);
for nr_descs in 0..MAX_DESC_LENGTH {
let mut iov_mut = IoVecBufferMut::any_of_length(nr_descs);

let mut buf = kani::vec::any_vec::<u8, GUEST_MEMORY_SIZE>();
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 regions, so checking the data copied is
// not exactly trivial.
//
// What we can verify is the bytes that we write into guest memory:
// - `buf.len()`, if `offset + buf.len() < iov.len()`;
// - `iov.len() - offset`, otherwise.
// Furthermore, we know our Read-/WriteVolatile implementation above is infallible, so
// 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 as usize,
GUEST_MEMORY_SIZE
)
.unwrap(),
buf.len().min(iov_mut.len().saturating_sub(offset) as usize)
);
}
}
}

0 comments on commit 2521805

Please sign in to comment.