Skip to content

Add a timeout option #3649

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Oct 29, 2024
Merged

Add a timeout option #3649

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
6003829
Add a timeout option
zhassan-aws Oct 25, 2024
9ca5f7c
clippy
zhassan-aws Oct 25, 2024
9381a60
Address PR comments
zhassan-aws Oct 25, 2024
220a52d
Merge branch 'main' into cbmc-timeout
zhassan-aws Oct 25, 2024
0502cc2
Make function async and call block_on
zhassan-aws Oct 26, 2024
c96ea92
Allow a unit suffix
zhassan-aws Oct 26, 2024
482ed11
Use strum::EnumString
zhassan-aws Oct 29, 2024
22be3f3
Merge branch 'main' into cbmc-timeout
zhassan-aws Oct 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
103 changes: 103 additions & 0 deletions Cargo.lock
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -807,6 +855,7 @@ dependencies = [
"strum_macros",
"tempfile",
"time",
"tokio",
"toml",
"tracing",
"tracing-subscriber",
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down
1 change: 1 addition & 0 deletions kani-driver/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 4 additions & 0 deletions kani-driver/src/args/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -281,6 +281,10 @@ pub struct VerificationArgs {
#[arg(long, hide = true)]
pub print_llbc: bool,

/// Timeout for CBMC command in seconds
#[arg(long)]
pub cbmc_timeout: Option<u32>,

/// Arguments to pass down to Cargo
#[command(flatten)]
pub cargo: CargoCommonArgs,
Expand Down
10 changes: 7 additions & 3 deletions kani-driver/src/assess/table_failure_reasons.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ use std::collections::HashSet;

use serde::{Deserialize, Serialize};

use crate::harness_runner::HarnessResult;
use crate::{call_cbmc::CbmcExitStatus, harness_runner::HarnessResult};

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

Expand Down Expand Up @@ -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 {
CbmcExitStatus::Timeout => String::from("CBMC timed out"),
CbmcExitStatus::OutOfMemory => String::from("CBMC ran out of memory"),
CbmcExitStatus::Other(exit_code) => format!("CBMC failed with status {exit_code}"),
}
} else {
let failures = r.result.failed_properties();
if failures.is_empty() {
Expand Down
Loading
Loading