implement kani integration (#73)

Author: camshaft

.github/workflows/main.yml

@@ -42,8 +42,9 @@ jobs:
   test:
     runs-on: ${{ matrix.os }}
     strategy:
+      fail-fast: false
       matrix:
-        rust: [1.52.0, stable, beta, nightly]
+        rust: [1.56.1, stable, beta, nightly]
         os: [ubuntu-latest, macOS-latest]
         # TODO add honggfuzz back
         test: [unit-tests, libfuzzer, afl, examples-tests]
@@ -115,3 +116,26 @@ jobs:
         AFL_I_DONT_CARE_ABOUT_MISSING_CRASHES: 1
         AFL_SKIP_CPUFREQ: 1
         SANITIZER: ${{ matrix.sanitizer }}
+
+  kani:
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/[email protected]
+
+    - uses: actions-rs/[email protected]
+      id: toolchain
+      with:
+        toolchain: stable
+        profile: minimal
+        override: true
+
+    - name: Setup
+      run: |
+        cargo install kani-verifier
+        cargo-kani setup
+
+    - name: Test
+      working-directory: examples/basic
+      run: |
+        cargo kani

.rustfmt.toml

@@ -1,5 +1,4 @@
 edition = "2018"
 format_macro_matchers = true
-merge_imports = true
-reorder_impl_items = true
+imports_granularity = "Crate"
 use_field_init_shorthand = true

bolero-engine/Cargo.toml

@@ -10,17 +10,17 @@ license = "MIT"
 edition = "2018"
 readme = "../README.md"
 
-[features]
-default = ["rng"]
-rng = ["rand"]
-
 [dependencies]
-anyhow = "1.0"
-backtrace = "0.3"
+anyhow = "1"
 bolero-generator = { version = "0.6", path = "../bolero-generator", default-features = false }
 lazy_static = "1"
 pretty-hex = "0.2.1"
-rand = { version = "^0.8", optional = true }
+
+[target.'cfg(not(kani))'.dependencies]
+backtrace = { version = "0.3" }
+
+[target.'cfg(not(any(fuzzing, kani)))'.dependencies]
+rand = { version = "^0.8" }
 
 [dev-dependencies]
 bolero-generator = { version = "0.6", path = "../bolero-generator", features = ["std"] }

bolero-engine/src/lib.rs

@@ -5,8 +5,13 @@ pub use bolero_generator::{
 };
 use core::time::Duration;
 
+#[cfg(not(kani))]
 pub mod panic;
-#[cfg(feature = "rng")]
+#[cfg(kani)]
+#[path = "./noop/panic.rs"]
+pub mod panic;
+
+#[cfg(not(any(fuzzing, kani)))]
 pub mod rng;
 pub mod shrink;
 mod test;

bolero-engine/src/noop/panic.rs

@@ -0,0 +1,72 @@
+use core::fmt::{self, Debug, Display};
+use std::panic::RefUnwindSafe;
+
+#[derive(Debug)]
+#[allow(dead_code)]
+pub struct PanicError {
+    pub(crate) message: String,
+    pub(crate) location: Option<String>,
+    pub(crate) backtrace: Option<Backtrace>,
+    pub(crate) thread_name: String,
+}
+
+impl Display for PanicError {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        writeln!(f, "PANIC")?;
+        Ok(())
+    }
+}
+
+impl std::error::Error for PanicError {}
+
+impl PanicError {
+    pub(crate) fn new(message: String) -> Self {
+        Self {
+            message,
+            location: None,
+            backtrace: None,
+            thread_name: thread_name(),
+        }
+    }
+}
+
+pub fn catch<F: RefUnwindSafe + FnOnce() -> Output, Output>(fun: F) -> Result<Output, PanicError> {
+    Ok(fun())
+}
+
+pub fn take_panic() -> Option<PanicError> {
+    None
+}
+
+pub fn capture_backtrace(_value: bool) -> bool {
+    false
+}
+
+pub fn forward_panic(_value: bool) -> bool {
+    false
+}
+
+pub fn set_hook() {
+    // no-op
+}
+
+pub fn rust_backtrace() -> bool {
+    false
+}
+
+pub fn thread_name() -> String {
+    String::from("main")
+}
+
+#[derive(Debug)]
+pub struct Backtrace(());
+
+impl Display for Backtrace {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        writeln!(f, "backtrace")?;
+        Ok(())
+    }
+}
+
+#[derive(Debug)]
+pub struct BacktraceFrame(());

bolero-engine/src/target_location.rs

@@ -28,6 +28,10 @@ pub struct TargetLocation {
 
 impl TargetLocation {
     pub fn should_run(&self) -> bool {
+        if cfg!(kani) {
+            return true;
+        }
+
         // cargo-bolero needs to resolve information about the target
         if let Ok(mode) = ::std::env::var("CARGO_BOLERO_SELECT") {
             match mode.as_str() {
@@ -61,6 +65,10 @@ impl TargetLocation {
     }
 
     pub fn abs_path(&self) -> Option<PathBuf> {
+        if cfg!(kani) {
+            return None;
+        }
+
         let file = Path::new(self.file);
 
         #[cfg(not(miri))] // miri does not currently support this call
@@ -83,6 +91,10 @@ impl TargetLocation {
     }
 
     pub fn work_dir(&self) -> Option<PathBuf> {
+        if cfg!(kani) {
+            return None;
+        }
+
         let mut work_dir = self.abs_path()?;
         work_dir.pop();
 
@@ -101,6 +113,10 @@ impl TargetLocation {
     }
 
     pub fn is_harnessed(&self) -> bool {
+        if cfg!(kani) {
+            return false;
+        }
+
         is_harnessed(self.item_path)
     }
 

bolero-engine/src/test.rs

@@ -133,6 +133,7 @@ where
 }
 
 /// Lazily generates a new value for the given driver
+#[cfg(not(kani))]
 macro_rules! generate_value {
     ($self:ident, $driver:ident) => {{
         let forward_panic = crate::panic::forward_panic(true);
@@ -154,6 +155,14 @@ macro_rules! generate_value {
         value
     }};
 }
+#[cfg(kani)]
+macro_rules! generate_value {
+    ($self:ident, $driver:ident) => {{
+        $self.value = $self.gen.generate($driver);
+        kani::assume($self.value.is_some());
+        $self.value.as_ref().unwrap()
+    }};
+}
 
 pub struct BorrowedGeneratorTest<F, G, V> {
     fun: F,

bolero-generator/Cargo.toml

@@ -17,7 +17,6 @@ alloc = ["rand_core/alloc"]
 
 [dependencies]
 bolero-generator-derive = { version = "0.6.0", path = "../bolero-generator-derive" }
-byteorder = { version = "1.3", default-features = false }
 either = { version = "1.5", default-features = false, optional = true }
 rand_core = { version = "^0.6", default-features = false }
 

bolero-kani/Cargo.toml

@@ -0,0 +1,19 @@
+[package]
+name = "bolero-kani"
+version = "0.6.0"
+authors = ["Cameron Bytheway <[email protected]>"]
+description = "kani plugin for bolero"
+homepage = "https://github.com/camshaft/bolero"
+repository = "https://github.com/camshaft/bolero"
+keywords = ["testing", "model", "proof"]
+license = "MIT"
+edition = "2018"
+readme = "../README.md"
+
+[features]
+default = ["lib"]
+bin = []
+lib = ["bolero-engine"]
+
+[dependencies]
+bolero-engine = { version = "0.6", path = "../bolero-engine", optional = true }