bolero_kani/
lib.rs

1//! kani plugin for bolero
2//!
3//! This crate should not be used directly. Instead, use `bolero`.
4
5#[doc(hidden)]
6#[cfg(all(feature = "lib", kani))]
7pub mod lib {
8    #[allow(unused_imports)]
9    use super::*;
10
11    use bolero_engine::{
12        driver, input, kani::Driver as KaniDriver, Engine, ScopedEngine, TargetLocation, Test,
13    };
14
15    #[derive(Debug, Default)]
16    pub struct KaniEngine {}
17
18    impl KaniEngine {
19        pub fn new(_location: TargetLocation) -> Self {
20            Self::default()
21        }
22    }
23
24    impl<T: Test> Engine<T> for KaniEngine
25    where
26        T::Value: core::fmt::Debug,
27    {
28        type Output = ();
29
30        fn run(self, mut test: T, options: driver::Options) -> Self::Output {
31            let mut input = KaniInput { options };
32            match test.test(&mut input) {
33                Ok(was_valid) => {
34                    // show if the generator was satisfiable
35                    // TODO fail the harness if it's not: https://github.com/model-checking/kani/issues/2792
36                    #[cfg(kani)]
37                    kani::cover!(
38                        was_valid,
39                        "the generator should produce at least one valid value"
40                    );
41                    let _ = was_valid;
42                }
43                Err(_) => {
44                    panic!("test failed");
45                }
46            }
47        }
48    }
49
50    impl ScopedEngine for KaniEngine {
51        type Output = ();
52
53        fn run<F, R>(self, test: F, options: driver::Options) -> Self::Output
54        where
55            F: FnMut() -> R,
56            R: bolero_engine::IntoResult,
57        {
58            let driver = KaniDriver::new(&options);
59            let (_driver, result) = bolero_engine::any::run(driver, test);
60            match result {
61                Ok(was_valid) => {
62                    // show if the generator was satisfiable
63                    // TODO fail the harness if it's not: https://github.com/model-checking/kani/issues/2792
64                    #[cfg(kani)]
65                    kani::cover!(
66                        was_valid,
67                        "the generator should produce at least one valid value"
68                    );
69                    let _ = was_valid;
70                }
71                Err(_) => {
72                    panic!("test failed");
73                }
74            }
75        }
76    }
77
78    struct KaniInput {
79        options: driver::Options,
80    }
81
82    impl<Output> input::Input<Output> for KaniInput {
83        type Driver = KaniDriver;
84
85        fn with_slice<F: FnMut(&[u8]) -> Output>(&mut self, f: &mut F) -> Output {
86            // TODO make this configurable
87            const MAX_LEN: usize = 256;
88
89            let bytes = kani::any::<[u8; MAX_LEN]>();
90            let len = kani::any::<usize>();
91            let max_len = self.options.max_len_or_default().min(MAX_LEN);
92            kani::assume(len <= max_len);
93
94            f(&bytes[..len])
95        }
96
97        fn with_driver<F: FnMut(&mut Self::Driver) -> Output>(&mut self, f: &mut F) -> Output {
98            let mut driver = KaniDriver::new(&self.options);
99            f(&mut driver)
100        }
101    }
102}
103
104#[doc(hidden)]
105#[cfg(all(feature = "lib", kani))]
106pub use lib::*;
bolero_kani/lib.rs

bolero_kani/
lib.rs
