bolero-kani 0.13.0

kani plugin for bolero
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106

//! kani plugin for bolero
//!
//! This crate should not be used directly. Instead, use `bolero`.

#[doc(hidden)]
#[cfg(all(feature = "lib", kani))]
pub mod lib {
    #[allow(unused_imports)]
    use super::*;

    use bolero_engine::{
        driver, input, kani::Driver as KaniDriver, Engine, ScopedEngine, TargetLocation, Test,
    };

    #[derive(Debug, Default)]
    pub struct KaniEngine {}

    impl KaniEngine {
        pub fn new(_location: TargetLocation) -> Self {
            Self::default()
        }
    }

    impl<T: Test> Engine<T> for KaniEngine
    where
        T::Value: core::fmt::Debug,
    {
        type Output = ();

        fn run(self, mut test: T, options: driver::Options) -> Self::Output {
            let mut input = KaniInput { options };
            match test.test(&mut input) {
                Ok(was_valid) => {
                    // show if the generator was satisfiable
                    // TODO fail the harness if it's not: https://github.com/model-checking/kani/issues/2792
                    #[cfg(kani)]
                    kani::cover!(
                        was_valid,
                        "the generator should produce at least one valid value"
                    );
                    let _ = was_valid;
                }
                Err(_) => {
                    panic!("test failed");
                }
            }
        }
    }

    impl ScopedEngine for KaniEngine {
        type Output = ();

        fn run<F, R>(self, test: F, options: driver::Options) -> Self::Output
        where
            F: FnMut() -> R,
            R: bolero_engine::IntoResult,
        {
            let driver = KaniDriver::new(&options);
            let (_driver, result) = bolero_engine::any::run(driver, test);
            match result {
                Ok(was_valid) => {
                    // show if the generator was satisfiable
                    // TODO fail the harness if it's not: https://github.com/model-checking/kani/issues/2792
                    #[cfg(kani)]
                    kani::cover!(
                        was_valid,
                        "the generator should produce at least one valid value"
                    );
                    let _ = was_valid;
                }
                Err(_) => {
                    panic!("test failed");
                }
            }
        }
    }

    struct KaniInput {
        options: driver::Options,
    }

    impl<Output> input::Input<Output> for KaniInput {
        type Driver = KaniDriver;

        fn with_slice<F: FnMut(&[u8]) -> Output>(&mut self, f: &mut F) -> Output {
            // TODO make this configurable
            const MAX_LEN: usize = 256;

            let bytes = kani::any::<[u8; MAX_LEN]>();
            let len = kani::any::<usize>();
            let max_len = self.options.max_len_or_default().min(MAX_LEN);
            kani::assume(len <= max_len);

            f(&bytes[..len])
        }

        fn with_driver<F: FnMut(&mut Self::Driver) -> Output>(&mut self, f: &mut F) -> Output {
            let mut driver = KaniDriver::new(&self.options);
            f(&mut driver)
        }
    }
}

#[doc(hidden)]
#[cfg(all(feature = "lib", kani))]
pub use lib::*;