Skip to content

Commit 323fc27

Browse files
zhassan-awszhassan-aws
authored
Add a timeout option (#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.
1 parent 87cd331 commit 323fc27

18 files changed

+427
-46
lines changed

‎Cargo.lock

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,21 @@
22
# It is not intended for manual editing.
33
version = 4
44

5+
[[package]]
6+
name = "addr2line"
7+
version = "0.24.2"
8+
source = "registry+https://github.com/rust-lang/crates.io-index"
9+
checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1"
10+
dependencies = [
11+
"gimli",
12+
]
13+
14+
[[package]]
15+
name = "adler2"
16+
version = "2.0.0"
17+
source = "registry+https://github.com/rust-lang/crates.io-index"
18+
checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627"
19+
520
[[package]]
621
name = "ahash"
722
version = "0.8.11"
@@ -113,6 +128,21 @@ version = "1.4.0"
113128
source = "registry+https://github.com/rust-lang/crates.io-index"
114129
checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26"
115130

131+
[[package]]
132+
name = "backtrace"
133+
version = "0.3.74"
134+
source = "registry+https://github.com/rust-lang/crates.io-index"
135+
checksum = "8d82cb332cdfaed17ae235a638438ac4d4839913cc2af585c3c6746e8f8bee1a"
136+
dependencies = [
137+
"addr2line",
138+
"cfg-if",
139+
"libc",
140+
"miniz_oxide",
141+
"object",
142+
"rustc-demangle",
143+
"windows-targets 0.52.6",
144+
]
145+
116146
[[package]]
117147
name = "bitflags"
118148
version = "2.6.0"
@@ -164,6 +194,12 @@ version = "1.5.0"
164194
source = "registry+https://github.com/rust-lang/crates.io-index"
165195
checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b"
166196

197+
[[package]]
198+
name = "bytes"
199+
version = "1.7.2"
200+
source = "registry+https://github.com/rust-lang/crates.io-index"
201+
checksum = "428d9aa8fbc0670b7b8d6030a7fadd0f86151cae55e4dbbece15f3780a3dfaf3"
202+
167203
[[package]]
168204
name = "camino"
169205
version = "1.1.9"
@@ -592,6 +628,12 @@ dependencies = [
592628
"wasi",
593629
]
594630

631+
[[package]]
632+
name = "gimli"
633+
version = "0.31.1"
634+
source = "registry+https://github.com/rust-lang/crates.io-index"
635+
checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f"
636+
595637
[[package]]
596638
name = "glob"
597639
version = "0.3.1"
@@ -640,6 +682,12 @@ version = "0.5.0"
640682
source = "registry+https://github.com/rust-lang/crates.io-index"
641683
checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
642684

685+
[[package]]
686+
name = "hermit-abi"
687+
version = "0.3.9"
688+
source = "registry+https://github.com/rust-lang/crates.io-index"
689+
checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024"
690+
643691
[[package]]
644692
name = "home"
645693
version = "0.5.9"
@@ -807,6 +855,7 @@ dependencies = [
807855
"strum_macros",
808856
"tempfile",
809857
"time",
858+
"tokio",
810859
"toml",
811860
"tracing",
812861
"tracing-subscriber",
@@ -930,6 +979,27 @@ version = "0.2.1"
930979
source = "registry+https://github.com/rust-lang/crates.io-index"
931980
checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
932981

982+
[[package]]
983+
name = "miniz_oxide"
984+
version = "0.8.0"
985+
source = "registry+https://github.com/rust-lang/crates.io-index"
986+
checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1"
987+
dependencies = [
988+
"adler2",
989+
]
990+
991+
[[package]]
992+
name = "mio"
993+
version = "1.0.2"
994+
source = "registry+https://github.com/rust-lang/crates.io-index"
995+
checksum = "80e04d1dcff3aae0704555fe5fee3bcfaf3d1fdf8a7e521d5b9d2b42acb52cec"
996+
dependencies = [
997+
"hermit-abi",
998+
"libc",
999+
"wasi",
1000+
"windows-sys 0.52.0",
1001+
]
1002+
9331003
[[package]]
9341004
name = "nom"
9351005
version = "7.1.3"
@@ -1051,6 +1121,15 @@ dependencies = [
10511121
"autocfg",
10521122
]
10531123

1124+
[[package]]
1125+
name = "object"
1126+
version = "0.36.5"
1127+
source = "registry+https://github.com/rust-lang/crates.io-index"
1128+
checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e"
1129+
dependencies = [
1130+
"memchr",
1131+
]
1132+
10541133
[[package]]
10551134
name = "once_cell"
10561135
version = "1.20.2"
@@ -1512,6 +1591,15 @@ version = "1.3.0"
15121591
source = "registry+https://github.com/rust-lang/crates.io-index"
15131592
checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
15141593

1594+
[[package]]
1595+
name = "signal-hook-registry"
1596+
version = "1.4.2"
1597+
source = "registry+https://github.com/rust-lang/crates.io-index"
1598+
checksum = "a9e9e0b4211b72e7b8b6e85c807d36c212bdb33ea8587f7569562a84df5465b1"
1599+
dependencies = [
1600+
"libc",
1601+
]
1602+
15151603
[[package]]
15161604
name = "sized-chunks"
15171605
version = "0.6.5"
@@ -1692,6 +1780,21 @@ dependencies = [
16921780
"time-core",
16931781
]
16941782

1783+
[[package]]
1784+
name = "tokio"
1785+
version = "1.40.0"
1786+
source = "registry+https://github.com/rust-lang/crates.io-index"
1787+
checksum = "e2b070231665d27ad9ec9b8df639893f46727666c6767db40317fbe920a5d998"
1788+
dependencies = [
1789+
"backtrace",
1790+
"bytes",
1791+
"libc",
1792+
"mio",
1793+
"pin-project-lite",
1794+
"signal-hook-registry",
1795+
"windows-sys 0.52.0",
1796+
]
1797+
16951798
[[package]]
16961799
name = "toml"
16971800
version = "0.8.19"

‎kani-driver/Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"
3636
rand = "0.8"
3737
which = "6"
3838
time = {version = "0.3.36", features = ["formatting"]}
39+
tokio = { version = "1.40.0", features = ["io-util", "process", "rt", "time"] }
3940

4041
# A good set of suggested dependencies can be found in rustup:
4142
# https://github.com/rust-lang/rustup/blob/master/Cargo.toml

‎kani-driver/src/args/mod.rs

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ use kani_metadata::CbmcSolver;
2121
use std::ffi::OsString;
2222
use std::path::PathBuf;
2323
use std::str::FromStr;
24+
use std::time::Duration;
2425
use strum::VariantNames;
2526

2627
/// Trait used to perform extra validation after parsing.
@@ -62,6 +63,53 @@ pub fn print_deprecated(verbosity: &CommonArgs, option: &str, alternative: &str)
6263
// By default we configure CBMC to use 16 bits to represent the object bits in pointers.
6364
const DEFAULT_OBJECT_BITS: u32 = 16;
6465

66+
#[derive(Clone, Copy, Debug, PartialEq, Eq, strum_macros::EnumString)]
67+
enum TimeUnit {
68+
#[strum(serialize = "s")]
69+
Seconds,
70+
#[strum(serialize = "m")]
71+
Minutes,
72+
#[strum(serialize = "h")]
73+
Hours,
74+
}
75+
76+
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
77+
pub struct Timeout {
78+
value: u32,
79+
unit: TimeUnit,
80+
}
81+
82+
impl FromStr for Timeout {
83+
type Err = String;
84+
85+
fn from_str(s: &str) -> Result<Self, Self::Err> {
86+
let last_char = s.chars().last().unwrap();
87+
let (value_str, unit_str) = if last_char.is_ascii_digit() {
88+
// no suffix
89+
(s, "s")
90+
} else {
91+
s.split_at(s.len() - 1)
92+
};
93+
let value = value_str.parse::<u32>().map_err(|_| "Invalid timeout value")?;
94+
95+
let unit = TimeUnit::from_str(unit_str).map_err(
96+
|_| "Invalid time unit. Use 's' for seconds, 'm' for minutes, or 'h' for hours",
97+
)?;
98+
99+
Ok(Timeout { value, unit })
100+
}
101+
}
102+
103+
impl From<Timeout> for Duration {
104+
fn from(timeout: Timeout) -> Self {
105+
match timeout.unit {
106+
TimeUnit::Seconds => Duration::from_secs(timeout.value as u64),
107+
TimeUnit::Minutes => Duration::from_secs(timeout.value as u64 * 60),
108+
TimeUnit::Hours => Duration::from_secs(timeout.value as u64 * 3600),
109+
}
110+
}
111+
}
112+
65113
#[derive(Debug, clap::Parser)]
66114
#[command(
67115
version,
@@ -281,6 +329,10 @@ pub struct VerificationArgs {
281329
#[arg(long, hide = true)]
282330
pub print_llbc: bool,
283331

332+
/// 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.
333+
#[arg(long)]
334+
pub harness_timeout: Option<Timeout>,
335+
284336
/// Arguments to pass down to Cargo
285337
#[command(flatten)]
286338
pub cargo: CargoCommonArgs,
@@ -637,6 +689,18 @@ impl ValidateArgs for VerificationArgs {
637689
"The `--cbmc-args` argument cannot be used with -Z lean.",
638690
));
639691
}
692+
693+
if self.harness_timeout.is_some()
694+
&& !self.common_args.unstable_features.contains(UnstableFeature::UnstableOptions)
695+
{
696+
return Err(Error::raw(
697+
ErrorKind::MissingRequiredArgument,
698+
format!(
699+
"The `--harness-timeout` argument is unstable and requires `-Z {}` to be used.",
700+
UnstableFeature::UnstableOptions
701+
),
702+
));
703+
}
640704
Ok(())
641705
}
642706
}

‎kani-driver/src/assess/table_failure_reasons.rs

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use std::collections::HashSet;
66

77
use serde::{Deserialize, Serialize};
88

9-
use crate::harness_runner::HarnessResult;
9+
use crate::{call_cbmc::ExitStatus, harness_runner::HarnessResult};
1010

1111
use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRow};
1212

@@ -35,8 +35,12 @@ pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder<FailureReasonsTab
3535
let mut builder = TableBuilder::new();
3636

3737
for r in results {
38-
let classification = if let Err(exit_code) = r.result.results {
39-
format!("CBMC failed with status {exit_code}")
38+
let classification = if let Err(exit_status) = r.result.results {
39+
match exit_status {
40+
ExitStatus::Timeout => String::from("CBMC timed out"),
41+
ExitStatus::OutOfMemory => String::from("CBMC ran out of memory"),
42+
ExitStatus::Other(exit_code) => format!("CBMC failed with status {exit_code}"),
43+
}
4044
} else {
4145
let failures = r.result.failed_properties();
4246
if failures.is_empty() {

0 commit comments

Comments
 (0)