Skip to content

kani: improve performance #4779

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Sep 3, 2024
Merged

kani: improve performance #4779

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5c75fee
kani: improve performance
roypat Sep 2, 2024
37ceaee
Merge branch 'main' into kani-perf
roypat Sep 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
116 changes: 61 additions & 55 deletions src/vmm/src/devices/virtio/iovec.rs
View file
Open in desktop
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)
);
}
}
}
Loading