Skip to content
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.

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

Add kani harness and auto-generated bolero harnesses #227

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
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
8 changes: 8 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ rustdoc-args = ["--cfg", "docsrs"]
with-serde = ["serde", "serde_derive"]

[dependencies]
arbitrary_shim = { version = "0.1.0", path = "../KaniAutoGenRegression/src/plugin/arbitrary_shim" }
libc = "0.2.39"
serde = { version = "1.0.27", optional = true }
serde_derive = { version = "1.0.27", optional = true }
Expand All @@ -27,3 +28,10 @@ bitflags = "1.0"
[dev-dependencies]
serde_json = "1.0.9"
bincode = "1.3.3"
bolero = "0.11.1"

[profile.fuzz]
inherits="dev"
opt-level=3
incremental=false
codegen-units=1
35 changes: 35 additions & 0 deletions src/errno.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ use std::result;
/// The error number is an integer number set by system calls and some libc
/// functions in case of error.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
#[cfg_attr(test, derive(bolero::TypeGenerator))]
pub struct Error(i32);

/// A specialized [Result](https://doc.rust-lang.org/std/result/enum.Result.html) type
Expand Down Expand Up @@ -195,3 +196,37 @@ mod tests {
);
}
}
/// The following harnesses were automatically generated by an
/// experimental tool developed by the Kani team.
#[cfg(test)]
mod bolero_harnesses {
use super::*;


#[test]
#[cfg_attr(kani, kani::proof)]
fn bolero_test_8_new() {
bolero::check!()
.with_type()
.cloned()
.for_each(|errno: i32| Some(Error::new(errno)));
}

#[test]
#[cfg_attr(kani, kani::proof)]
fn bolero_test_9_last() {
bolero::check!()
.with_type()
.cloned()
.for_each(|()| Some(Error::last()));
}

#[test]
#[cfg_attr(kani, kani::proof)]
fn bolero_test_10_errno() {
bolero::check!()
.with_type()
.cloned()
.for_each(|callee: Error| Some(callee.errno().clone()));
}
}
105 changes: 105 additions & 0 deletions src/fam.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ use std::mem::{self, size_of};

/// Errors associated with the [`FamStructWrapper`](struct.FamStructWrapper.html) struct.
#[derive(Clone, Debug, PartialEq, Eq)]
#[cfg_attr(test, derive(bolero::TypeGenerator))]
pub enum Error {
/// The max size has been exceeded
SizeLimitExceeded,
Expand Down Expand Up @@ -1140,3 +1141,107 @@ mod tests {
);
}
}

#[cfg(kani)]
mod kani_harnesses {

use super::*;

#[repr(C)]
#[derive(Default, Debug, PartialEq, Eq)]
pub struct __IncompleteArrayField<T>(::std::marker::PhantomData<T>, [T; 0]);
impl<T> __IncompleteArrayField<T> {
#[inline]
pub fn new() -> Self {
__IncompleteArrayField(::std::marker::PhantomData, [])
}
#[inline]
pub unsafe fn as_ptr(&self) -> *const T {
self as *const __IncompleteArrayField<T> as *const T
}
#[inline]
pub unsafe fn as_mut_ptr(&mut self) -> *mut T {
self as *mut __IncompleteArrayField<T> as *mut T
}
#[inline]
pub unsafe fn as_slice(&self, len: usize) -> &[T] {
::std::slice::from_raw_parts(self.as_ptr(), len)
}
#[inline]
pub unsafe fn as_mut_slice(&mut self, len: usize) -> &mut [T] {
::std::slice::from_raw_parts_mut(self.as_mut_ptr(), len)
}
}

#[repr(C)]
#[derive(Default, PartialEq)]
struct MockFamStructU8 {
pub len: u32,
pub padding: u32,
pub entries: __IncompleteArrayField<u8>,
}
generate_fam_struct_impl!(MockFamStructU8, u8, entries, u32, len, 100);
type MockFamStructWrapperU8 = FamStructWrapper<MockFamStructU8>;

#[kani::proof]
#[kani::unwind(20)]
fn prove_as_mut_fam_struct() {
type U8Wrapper = FamStructWrapper<MockFamStructU8>;

let len: usize = kani::any();

let mut adapter = U8Wrapper::new(len).unwrap();

unsafe {
adapter.as_mut_fam_struct();
}
}

#[kani::proof]
#[kani::unwind(20)]
fn prove_into_raw() {
type U8Wrapper = FamStructWrapper<MockFamStructU8>;

let len: usize = kani::any();

let mut adapter = U8Wrapper::new(len).unwrap();

adapter.into_raw();
}

#[kani::proof]
#[kani::unwind(20)]
fn prove_as_fam_struct_ptr() {
type U8Wrapper = FamStructWrapper<MockFamStructU8>;

let len: usize = kani::any();

let mut adapter = U8Wrapper::new(len).unwrap();

adapter.as_fam_struct_ptr();
}

#[kani::proof]
#[kani::unwind(20)]
fn prove_len() {
type U8Wrapper = FamStructWrapper<MockFamStructU8>;

let len: usize = kani::any();

let mut adapter = U8Wrapper::new(len).unwrap();

adapter.len();
}

#[kani::proof]
#[kani::unwind(20)]
fn prove_capacity() {
type U8Wrapper = FamStructWrapper<MockFamStructU8>;

let len: usize = kani::any();

let mut adapter = U8Wrapper::new(len).unwrap();

adapter.capacity();
}
}
41 changes: 41 additions & 0 deletions src/rand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -177,3 +177,44 @@ mod tests {
}
}
}
/// The following harnesses were automatically generated by an
/// experimental tool developed by the Kani team.
#[cfg(test)]
mod bolero_harnesses {
use super::*;
#[test]
#[cfg_attr(kani, kani::proof)]
fn bolero_test_3_timestamp_cycles() {
bolero::check!()
.with_type()
.cloned()
.for_each(|()| Some(timestamp_cycles()));
}

#[test]
#[cfg_attr(kani, kani::proof)]
fn bolero_test_4_xor_pseudo_rng_u32() {
bolero::check!()
.with_type()
.cloned()
.for_each(|()| Some(xor_pseudo_rng_u32()));
}

#[test]
#[cfg_attr(kani, kani::proof)]
fn bolero_test_5_rand_alphanumerics() {
bolero::check!()
.with_type()
.cloned()
.for_each(|len: usize| Some(rand_alphanumerics(len)));
}

#[test]
#[cfg_attr(kani, kani::proof)]
fn bolero_test_6_rand_bytes() {
bolero::check!()
.with_type()
.cloned()
.for_each(|len: usize| Some(rand_bytes(len)));
}
}
1 change: 1 addition & 0 deletions src/syscall.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ use std::os::raw::c_int;

/// Wrapper to interpret syscall exit codes and provide a rustacean `io::Result`.
#[derive(Debug)]
#[cfg_attr(test, derive(Clone, bolero::TypeGenerator))]
pub struct SyscallReturnCode<T: From<i8> + Eq = c_int>(pub T);

impl<T: From<i8> + Eq> SyscallReturnCode<T> {
Expand Down