Add a timeout option (model-checking#3649)

This PR adds a new option, `--cbmc-timeout` which can be used for setting a timeout for the CBMC run. The timeout applies on a per-harness basis in the Kani run. The implementation uses [tokio ](https://tokio.rs/) to perform non-blocking reads from the CBMC process's `stdout` so that the timeout can be checked asynchronously. **Call-outs:** There are other names I considered for the option: - `--harness-timeout`: This makes it clearer that the timeout applies to each individual harness (and not to the overall Kani run). It doesn't indicate that the timeout only applies to the CBMC portion of the flow though. - `--engine-timeout`: This makes it a bit more general across multiple engine/backends. The notion of an engine is not really part of the Kani jargon currently though, so might not be clear to users. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
carolynzech · Oct 29, 2024 · 323fc27 · 323fc27
1 parent 87cd331
commit 323fc27
Show file tree

Hide file tree

Showing 18 changed files with 427 additions and 46 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -2,6 +2,21 @@
 # It is not intended for manual editing.
 version = 4
 
+[[package]]
+name = "addr2line"
+version = "0.24.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1"
+dependencies = [
+ "gimli",
+]
+
+[[package]]
+name = "adler2"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627"
+
 [[package]]
 name = "ahash"
 version = "0.8.11"
@@ -113,6 +128,21 @@ version = "1.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26"
 
+[[package]]
+name = "backtrace"
+version = "0.3.74"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8d82cb332cdfaed17ae235a638438ac4d4839913cc2af585c3c6746e8f8bee1a"
+dependencies = [
+ "addr2line",
+ "cfg-if",
+ "libc",
+ "miniz_oxide",
+ "object",
+ "rustc-demangle",
+ "windows-targets 0.52.6",
+]
+
 [[package]]
 name = "bitflags"
 version = "2.6.0"
@@ -164,6 +194,12 @@ version = "1.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b"
 
+[[package]]
+name = "bytes"
+version = "1.7.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "428d9aa8fbc0670b7b8d6030a7fadd0f86151cae55e4dbbece15f3780a3dfaf3"
+
 [[package]]
 name = "camino"
 version = "1.1.9"
@@ -592,6 +628,12 @@ dependencies = [
  "wasi",
 ]
 
+[[package]]
+name = "gimli"
+version = "0.31.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f"
+
 [[package]]
 name = "glob"
 version = "0.3.1"
@@ -640,6 +682,12 @@ version = "0.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
 
+[[package]]
+name = "hermit-abi"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024"
+
 [[package]]
 name = "home"
 version = "0.5.9"
@@ -807,6 +855,7 @@ dependencies = [
  "strum_macros",
  "tempfile",
  "time",
+ "tokio",
  "toml",
  "tracing",
  "tracing-subscriber",
@@ -930,6 +979,27 @@ version = "0.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
 
+[[package]]
+name = "miniz_oxide"
+version = "0.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1"
+dependencies = [
+ "adler2",
+]
+
+[[package]]
+name = "mio"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "80e04d1dcff3aae0704555fe5fee3bcfaf3d1fdf8a7e521d5b9d2b42acb52cec"
+dependencies = [
+ "hermit-abi",
+ "libc",
+ "wasi",
+ "windows-sys 0.52.0",
+]
+
 [[package]]
 name = "nom"
 version = "7.1.3"
@@ -1051,6 +1121,15 @@ dependencies = [
  "autocfg",
 ]
 
+[[package]]
+name = "object"
+version = "0.36.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e"
+dependencies = [
+ "memchr",
+]
+
 [[package]]
 name = "once_cell"
 version = "1.20.2"
@@ -1512,6 +1591,15 @@ version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
 
+[[package]]
+name = "signal-hook-registry"
+version = "1.4.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a9e9e0b4211b72e7b8b6e85c807d36c212bdb33ea8587f7569562a84df5465b1"
+dependencies = [
+ "libc",
+]
+
 [[package]]
 name = "sized-chunks"
 version = "0.6.5"
@@ -1692,6 +1780,21 @@ dependencies = [
  "time-core",
 ]
 
+[[package]]
+name = "tokio"
+version = "1.40.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e2b070231665d27ad9ec9b8df639893f46727666c6767db40317fbe920a5d998"
+dependencies = [
+ "backtrace",
+ "bytes",
+ "libc",
+ "mio",
+ "pin-project-lite",
+ "signal-hook-registry",
+ "windows-sys 0.52.0",
+]
+
 [[package]]
 name = "toml"
 version = "0.8.19"

diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
@@ -36,6 +36,7 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"
 rand = "0.8"
 which = "6"
 time = {version = "0.3.36", features = ["formatting"]}
+tokio = { version = "1.40.0", features = ["io-util", "process", "rt", "time"] }
 
 # A good set of suggested dependencies can be found in rustup:
 # https://github.com/rust-lang/rustup/blob/master/Cargo.toml

diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
@@ -21,6 +21,7 @@ use kani_metadata::CbmcSolver;
 use std::ffi::OsString;
 use std::path::PathBuf;
 use std::str::FromStr;
+use std::time::Duration;
 use strum::VariantNames;
 
 /// Trait used to perform extra validation after parsing.
@@ -62,6 +63,53 @@ pub fn print_deprecated(verbosity: &CommonArgs, option: &str, alternative: &str)
 // By default we configure CBMC to use 16 bits to represent the object bits in pointers.
 const DEFAULT_OBJECT_BITS: u32 = 16;
 
+#[derive(Clone, Copy, Debug, PartialEq, Eq, strum_macros::EnumString)]
+enum TimeUnit {
+    #[strum(serialize = "s")]
+    Seconds,
+    #[strum(serialize = "m")]
+    Minutes,
+    #[strum(serialize = "h")]
+    Hours,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct Timeout {
+    value: u32,
+    unit: TimeUnit,
+}
+
+impl FromStr for Timeout {
+    type Err = String;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        let last_char = s.chars().last().unwrap();
+        let (value_str, unit_str) = if last_char.is_ascii_digit() {
+            // no suffix
+            (s, "s")
+        } else {
+            s.split_at(s.len() - 1)
+        };
+        let value = value_str.parse::<u32>().map_err(|_| "Invalid timeout value")?;
+
+        let unit = TimeUnit::from_str(unit_str).map_err(
+            |_| "Invalid time unit. Use 's' for seconds, 'm' for minutes, or 'h' for hours",
+        )?;
+
+        Ok(Timeout { value, unit })
+    }
+}
+
+impl From<Timeout> for Duration {
+    fn from(timeout: Timeout) -> Self {
+        match timeout.unit {
+            TimeUnit::Seconds => Duration::from_secs(timeout.value as u64),
+            TimeUnit::Minutes => Duration::from_secs(timeout.value as u64 * 60),
+            TimeUnit::Hours => Duration::from_secs(timeout.value as u64 * 3600),
+        }
+    }
+}
+
 #[derive(Debug, clap::Parser)]
 #[command(
     version,
@@ -281,6 +329,10 @@ pub struct VerificationArgs {
     #[arg(long, hide = true)]
     pub print_llbc: bool,
 
+    /// Timeout for each harness with optional suffix ('s': seconds, 'm': minutes, 'h': hours). Default is seconds. This option is experimental and requires `-Z unstable-options` to be used.
+    #[arg(long)]
+    pub harness_timeout: Option<Timeout>,
+
     /// Arguments to pass down to Cargo
     #[command(flatten)]
     pub cargo: CargoCommonArgs,
@@ -637,6 +689,18 @@ impl ValidateArgs for VerificationArgs {
                 "The `--cbmc-args` argument cannot be used with -Z lean.",
             ));
         }
+
+        if self.harness_timeout.is_some()
+            && !self.common_args.unstable_features.contains(UnstableFeature::UnstableOptions)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                format!(
+                    "The `--harness-timeout` argument is unstable and requires `-Z {}` to be used.",
+                    UnstableFeature::UnstableOptions
+                ),
+            ));
+        }
         Ok(())
     }
 }

diff --git a/kani-driver/src/assess/table_failure_reasons.rs b/kani-driver/src/assess/table_failure_reasons.rs
@@ -6,7 +6,7 @@ use std::collections::HashSet;
 
 use serde::{Deserialize, Serialize};
 
-use crate::harness_runner::HarnessResult;
+use crate::{call_cbmc::ExitStatus, harness_runner::HarnessResult};
 
 use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRow};
 
@@ -35,8 +35,12 @@ pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder<FailureReasonsTab
     let mut builder = TableBuilder::new();
 
     for r in results {
-        let classification = if let Err(exit_code) = r.result.results {
-            format!("CBMC failed with status {exit_code}")
+        let classification = if let Err(exit_status) = r.result.results {
+            match exit_status {
+                ExitStatus::Timeout => String::from("CBMC timed out"),
+                ExitStatus::OutOfMemory => String::from("CBMC ran out of memory"),
+                ExitStatus::Other(exit_code) => format!("CBMC failed with status {exit_code}"),
+            }
         } else {
             let failures = r.result.failed_properties();
             if failures.is_empty() {