From 6003829f15f9fef1494489d2d6a2d6626040175a Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 25 Oct 2024 11:03:30 -0700 Subject: [PATCH 1/6] Add a timeout option --- Cargo.lock | 103 +++++++++++++++++ kani-driver/Cargo.toml | 1 + kani-driver/src/args/mod.rs | 4 + .../src/assess/table_failure_reasons.rs | 10 +- kani-driver/src/call_cbmc.rs | 108 +++++++++++++++--- kani-driver/src/cbmc_output_parser.rs | 51 +++++---- kani-driver/src/session.rs | 54 +++++++++ tests/.gitignore | 2 +- tests/ui/cbmc-timeout/no_timeout.expected | 1 + tests/ui/cbmc-timeout/no_timeout.rs | 14 +++ tests/ui/cbmc-timeout/timeout.expected | 4 + tests/ui/cbmc-timeout/timeout.rs | 16 +++ 12 files changed, 323 insertions(+), 45 deletions(-) create mode 100644 tests/ui/cbmc-timeout/no_timeout.expected create mode 100644 tests/ui/cbmc-timeout/no_timeout.rs create mode 100644 tests/ui/cbmc-timeout/timeout.expected create mode 100644 tests/ui/cbmc-timeout/timeout.rs diff --git a/Cargo.lock b/Cargo.lock index 6b59d0179bde..1399e798a266 100644 --- 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 index 67214738fa7c..d1460a9c943d 100644 --- 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 index b0811915aaf7..e81ab12d8f6e 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -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, + /// Arguments to pass down to Cargo #[command(flatten)] pub cargo: CargoCommonArgs, diff --git a/kani-driver/src/assess/table_failure_reasons.rs b/kani-driver/src/assess/table_failure_reasons.rs index 9836aaa871cd..9233451e9432 100644 --- 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::CbmcExitStatus, harness_runner::HarnessResult}; use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRow}; @@ -35,8 +35,12 @@ pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder format!("CBMC timed out"), + CbmcExitStatus::OutOfMemory => format!("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() { diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index e69985760460..5d04903bd9b5 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -13,7 +13,9 @@ use std::path::Path; use std::process::Command; use std::sync::OnceLock; use std::time::{Duration, Instant}; +use tokio::process::Command as TokioCommand; +use crate::args::common::Verbosity; use crate::args::{OutputFormat, VerificationArgs}; use crate::cbmc_output_parser::{ CheckStatus, Property, VerificationOutput, extract_results, process_cbmc_output, @@ -22,6 +24,7 @@ use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_ou use crate::coverage::cov_results::{CoverageCheck, CoverageResults}; use crate::coverage::cov_results::{CoverageRegion, CoverageTerm}; use crate::session::KaniSession; +use crate::util::render_command; /// We will use Cadical by default since it performed better than MiniSAT in our analysis. /// Note: Kissat was marginally better, but it is an external solver which could be more unstable. @@ -45,6 +48,15 @@ pub enum FailedProperties { Other, } +/// The possible CBMC exit statuses +#[derive(Clone, Copy, Debug)] +pub enum CbmcExitStatus { + Timeout, + OutOfMemory, + /// the integer is the process exit status + Other(i32), +} + /// Our (kani-driver) notions of CBMC results. #[derive(Debug)] pub struct VerificationResult { @@ -56,7 +68,7 @@ pub struct VerificationResult { /// Note: CBMC process exit status is only potentially useful if `status` is `Failure`. /// Kani will see CBMC report "failure" that's actually success (interpreting "failed" /// checks like coverage as expected and desirable.) - pub results: Result, i32>, + pub results: Result, CbmcExitStatus>, /// The runtime duration of this CBMC invocation. pub runtime: Duration, /// Whether concrete playback generated a test @@ -71,13 +83,11 @@ impl KaniSession { let args: Vec = self.cbmc_flags(file, harness)?; // TODO get cbmc path from self - let mut cmd = Command::new("cbmc"); + let mut cmd = TokioCommand::new("cbmc"); cmd.args(args); - let start_time = Instant::now(); - let verification_results = if self.args.output_format == crate::args::OutputFormat::Old { - if self.run_terminal(cmd).is_err() { + if self.run_terminal_timeout(cmd).is_err() { VerificationResult::mock_failure() } else { VerificationResult::mock_success() @@ -87,18 +97,66 @@ impl KaniSession { // Done here because `--visualize` uses the XML format instead. cmd.arg("--json-ui"); - // Spawn the CBMC process and process its output below - let cbmc_process = - self.run_piped(cmd).map_err(|_| anyhow::Error::msg("Failed to run cbmc"))?; - let output = process_cbmc_output(cbmc_process, |i| { + self.runtime.block_on(self.run_cbmc_piped(cmd, harness))? + }; + + Ok(verification_results) + } + + async fn run_cbmc_piped( + &self, + mut cmd: TokioCommand, + harness: &HarnessMetadata, + ) -> Result { + if self.args.common_args.verbose() { + println!("[Kani] Running: `{}`", render_command(cmd.as_std()).to_string_lossy()); + } + // Spawn the CBMC process and process its output below + let cbmc_process = cmd + .stdout(std::process::Stdio::piped()) + .spawn() + .map_err(|_| anyhow::Error::msg("Failed to run cbmc"))?; + + let start_time = Instant::now(); + + let res = if let Some(timeout) = self.args.cbmc_timeout { + tokio::time::timeout( + std::time::Duration::from_secs(timeout.into()), + process_cbmc_output(cbmc_process, |i| { + kani_cbmc_output_filter( + i, + self.args.extra_pointer_checks, + self.args.common_args.quiet, + &self.args.output_format, + ) + }), + ) + .await + } else { + Ok(process_cbmc_output(cbmc_process, |i| { kani_cbmc_output_filter( i, self.args.extra_pointer_checks, self.args.common_args.quiet, &self.args.output_format, ) - })?; + }) + .await) + }; + let verification_results = if res.is_err() { + // An error occurs if the timeout was reached + VerificationResult { + status: VerificationStatus::Failure, + failed_properties: FailedProperties::None, + results: Err(CbmcExitStatus::Timeout), + runtime: start_time.elapsed(), + generated_concrete_test: false, + coverage_results: None, + } + } else { + // The timeout wasn't reached + let output = res.unwrap()?; VerificationResult::from(output, harness.attributes.should_panic, start_time) }; @@ -293,10 +351,15 @@ impl VerificationResult { } } else { // We never got results from CBMC - something went wrong (e.g. crash) so it's failure + let exit_status = if output.process_status == 137 { + CbmcExitStatus::OutOfMemory + } else { + CbmcExitStatus::Other(output.process_status) + }; VerificationResult { status: VerificationStatus::Failure, failed_properties: FailedProperties::Other, - results: Err(output.process_status), + results: Err(exit_status), runtime, generated_concrete_test: false, coverage_results: None, @@ -322,7 +385,7 @@ impl VerificationResult { // on failure, exit codes in theory might be used, // but `mock_failure` should never be used in a context where they will, // so again use something weird: - results: Err(42), + results: Err(CbmcExitStatus::Other(42)), runtime: Duration::from_secs(0), generated_concrete_test: false, coverage_results: None, @@ -353,15 +416,24 @@ impl VerificationResult { } Err(exit_status) => { let verification_result = console::style("FAILED").red(); - let explanation = if *exit_status == 137 { - "CBMC appears to have run out of memory. You may want to rerun your proof in \ + let (header, explanation) = match exit_status { + CbmcExitStatus::OutOfMemory => ( + String::from("CBMC failed"), + "CBMC appears to have run out of memory. You may want to rerun your proof in \ an environment with additional memory or use stubbing to reduce the size of the \ - code the verifier reasons about.\n" - } else { - "" + code the verifier reasons about.\n", + ), + CbmcExitStatus::Timeout => ( + String::from("CBMC failed"), + "CBMC timed out. You may want to rerun your proof with a larger timeout \ + or use stubbing to reduce the size of the code the verifier reasons about.\n", + ), + CbmcExitStatus::Other(exit_status) => { + (format!("CBMC failed with status {exit_status}"), "") + } }; format!( - "\nCBMC failed with status {exit_status}\n\ + "\n{header}\n\ VERIFICATION:- {verification_result}\n\ {explanation}", ) diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index 58a93df3a2f6..d2ae389c0063 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -30,10 +30,10 @@ use rustc_demangle::demangle; use serde::{Deserialize, Deserializer, Serialize}; use std::env; -use std::io::{BufRead, BufReader}; use std::os::unix::process::ExitStatusExt; use std::path::PathBuf; -use std::process::{Child, ChildStdout}; +use tokio::io::{AsyncBufReadExt, BufReader}; +use tokio::process::{Child, ChildStdout}; const RESULT_ITEM_PREFIX: &str = " {\n \"result\":"; @@ -360,9 +360,8 @@ enum Action { ProcessItem, } -/// A parser for CBMC output, whose state is determined by: -/// 1. The input accumulator, required to process items on the fly. -/// 2. The buffer, which is accessed to retrieve more lines. +/// A parser for CBMC output, whose state is determined by +/// the input accumulator, required to process items on the fly. /// /// CBMC's JSON output is defined as a JSON array which contains: /// 1. One program at the beginning (i.e., a message with CBMC's version). @@ -377,14 +376,13 @@ enum Action { /// There is a feature request for serde_json which would obsolete this if /// it ever lands: /// (Would provide a streaming iterator over a json array.) -struct Parser<'a, 'b> { +struct Parser { pub input_so_far: String, - pub buffer: &'a mut BufReader<&'b mut ChildStdout>, } -impl<'a, 'b> Parser<'a, 'b> { - fn new(buffer: &'a mut BufReader<&'b mut ChildStdout>) -> Self { - Parser { input_so_far: String::new(), buffer } +impl Parser { + fn new() -> Self { + Parser { input_so_far: String::new() } } /// Triggers an action based on the input: @@ -479,16 +477,16 @@ impl<'a, 'b> Parser<'a, 'b> { } None } -} -/// The iterator implementation for `Parser` reads the buffer line by line, -/// and determines if it must return an item based on processing each line. -impl Iterator for Parser<'_, '_> { - type Item = ParserItem; - fn next(&mut self) -> Option { + /// Read the process output and return when an item is found in the output + /// or the EOF is reached + async fn read_output<'a, 'b>( + &mut self, + buffer: &'a mut BufReader<&'b mut ChildStdout>, + ) -> Option { loop { let mut input = String::new(); - match self.buffer.read_line(&mut input) { + match buffer.read_line(&mut input).await { Ok(len) => { if len == 0 { return None; @@ -522,17 +520,24 @@ pub struct VerificationOutput { /// then formatted (according to the output format) and print. /// /// The cbmc process status is returned, along with the (post-filter) items. -pub fn process_cbmc_output( +pub async fn process_cbmc_output( mut process: Child, - eager_filter: impl FnMut(ParserItem) -> Option, + mut eager_filter: impl FnMut(ParserItem) -> Option, ) -> Result { let stdout = process.stdout.as_mut().unwrap(); let mut stdout_reader = BufReader::new(stdout); - let parser = Parser::new(&mut stdout_reader); - // This should run until stdout is closed (which should mean the process exited) - let processed_items: Vec<_> = parser.filter_map(eager_filter).collect(); + let mut parser = Parser::new(); + // This should run until stdout is closed (which should mean the process + // exited) or the specified timeout is reached + let mut processed_items = Vec::new(); + while let Some(item) = parser.read_output(&mut stdout_reader).await { + if let Some(item) = eager_filter(item) { + processed_items.push(item); + } + } + // This will get us the process's exit code - let status = process.wait()?; + let status = process.wait().await?; let process_status = match (status.code(), status.signal()) { // normal unix exit codes (cbmc uses currently 0-10) diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 5ab5a635d91f..a9d39c63f510 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -12,6 +12,7 @@ use std::process::{Child, Command, ExitStatus, Stdio}; use std::sync::Mutex; use std::time::Instant; use strum_macros::Display; +use tokio::process::Command as TokioCommand; use tracing::level_filters::LevelFilter; use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt}; @@ -38,6 +39,9 @@ pub struct KaniSession { /// The temporary files we littered that need to be cleaned up at the end of execution pub temporaries: Mutex>, + + /// The tokio runtime + pub runtime: tokio::runtime::Runtime, } /// Represents where we detected Kani, with helper methods for using that information to find critical paths @@ -61,6 +65,7 @@ impl KaniSession { kani_compiler: install.kani_compiler()?, kani_lib_c: install.kani_lib_c()?, temporaries: Mutex::new(vec![]), + runtime: tokio::runtime::Builder::new_current_thread().enable_all().build().unwrap(), }) } @@ -113,6 +118,12 @@ impl KaniSession { run_terminal(&self.args.common_args, cmd) } + /// Call [run_terminal_timeout] with the verbosity configured by the user. + /// The `bool` value indicates whether the command timed out + pub fn run_terminal_timeout(&self, cmd: TokioCommand) -> Result { + run_terminal_timeout(&self.args.common_args, cmd, &self.runtime, self.args.cbmc_timeout) + } + /// Call [run_suppress] with the verbosity configured by the user. pub fn run_suppress(&self, cmd: Command) -> Result<()> { run_suppress(&self.args.common_args, cmd) @@ -174,6 +185,49 @@ pub fn run_terminal(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()> Ok(()) } +/// The `bool` value indicates whether the command timed out +fn run_terminal_timeout( + verbosity: &impl Verbosity, + mut cmd: TokioCommand, + runtime: &tokio::runtime::Runtime, + timeout: Option, +) -> Result { + if verbosity.quiet() { + cmd.stdout(std::process::Stdio::null()); + cmd.stderr(std::process::Stdio::null()); + } + if verbosity.verbose() { + println!("[Kani] Running: `{}`", render_command(&cmd.as_std()).to_string_lossy()); + } + let program = cmd.as_std().get_program().to_string_lossy().to_string(); + let result = with_timer( + verbosity, + || { + runtime.block_on(async { + if let Some(timeout) = timeout { + tokio::time::timeout( + std::time::Duration::from_secs(timeout as u64), + cmd.status(), + ) + .await + } else { + Ok(cmd.status().await) + } + }) + }, + &program, + ); + // outer result indicates whether the command timed out + if result.is_err() { + return Ok(true); + } + let result = result.unwrap().context(format!("Failed to invoke {program}"))?; + if !result.success() { + bail!("{} exited with status {}", cmd.as_std().get_program().to_string_lossy(), result); + } + Ok(false) +} + /// Run a job, but only output (unless --quiet) if it fails, and fail if there's a problem. pub fn run_suppress(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()> { if verbosity.is_set() { diff --git a/tests/.gitignore b/tests/.gitignore index 7f948a83337c..814a069a9424 100644 --- a/tests/.gitignore +++ b/tests/.gitignore @@ -6,7 +6,7 @@ target/ # Binary artifacts *.goto -*out +*.out smoke check_tests function diff --git a/tests/ui/cbmc-timeout/no_timeout.expected b/tests/ui/cbmc-timeout/no_timeout.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/ui/cbmc-timeout/no_timeout.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/ui/cbmc-timeout/no_timeout.rs b/tests/ui/cbmc-timeout/no_timeout.rs new file mode 100644 index 000000000000..71e152aed763 --- /dev/null +++ b/tests/ui/cbmc-timeout/no_timeout.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --cbmc-timeout 10 +// +// Check the behavior of Kani when given a timeout via `--cbmc-timeout`, but +// CBMC completes before the timeout + +#[kani::proof] +fn check_cbmc_no_timeout() { + let x: u8 = kani::any(); + let y: u8 = kani::any(); + kani::assume(y == 0); + assert_eq!(x + y, x); +} diff --git a/tests/ui/cbmc-timeout/timeout.expected b/tests/ui/cbmc-timeout/timeout.expected new file mode 100644 index 000000000000..76102989b631 --- /dev/null +++ b/tests/ui/cbmc-timeout/timeout.expected @@ -0,0 +1,4 @@ +VERIFICATION:- FAILED +CBMC timed out. You may want to rerun your proof with a larger timeout or use stubbing to reduce the size of the code the verifier reasons about. + +Verification failed for - check_cbmc_timeout diff --git a/tests/ui/cbmc-timeout/timeout.rs b/tests/ui/cbmc-timeout/timeout.rs new file mode 100644 index 000000000000..975009be1ac1 --- /dev/null +++ b/tests/ui/cbmc-timeout/timeout.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --cbmc-timeout 5 +// +// Check that Kani respects the specified `--cbmc-timeout` option + +#[kani::proof] +fn check_cbmc_timeout() { + // construct a problem that requires a long time to solve + let (a1, b1, c1): (u64, u64, u64) = kani::any(); + let (a2, b2, c2): (u64, u64, u64) = kani::any(); + let p1 = a1.saturating_mul(b1).saturating_mul(c1); + let p2 = a2.saturating_mul(b2).saturating_mul(c2); + // (a1 == a2 && b1 == b2 && c1 == c2) implies p1 == p2 + assert!(a1 != a2 || b1 != b2 || c1 != c2 || p1 == p2) +} From 9ca5f7c4ed5e95e94cb4d920da32677b3fc561c1 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 25 Oct 2024 11:16:34 -0700 Subject: [PATCH 2/6] clippy --- kani-driver/src/assess/table_failure_reasons.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-driver/src/assess/table_failure_reasons.rs b/kani-driver/src/assess/table_failure_reasons.rs index 9233451e9432..975e38919e64 100644 --- a/kani-driver/src/assess/table_failure_reasons.rs +++ b/kani-driver/src/assess/table_failure_reasons.rs @@ -37,8 +37,8 @@ pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder format!("CBMC timed out"), - CbmcExitStatus::OutOfMemory => format!("CBMC ran out of memory"), + 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 { From 9381a60994eac2976b2628fc82bea53f645e64e4 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 25 Oct 2024 15:29:55 -0700 Subject: [PATCH 3/6] Address PR comments --- kani-driver/src/args/mod.rs | 16 +++++++++++++-- .../src/assess/table_failure_reasons.rs | 8 ++++---- kani-driver/src/call_cbmc.rs | 20 +++++++++---------- kani-driver/src/session.rs | 2 +- .../no_timeout.expected | 0 .../no_timeout.rs | 6 +++--- .../timeout.expected | 0 .../timeout.rs | 4 ++-- 8 files changed, 34 insertions(+), 22 deletions(-) rename tests/ui/{cbmc-timeout => harness-timeout}/no_timeout.expected (100%) rename tests/ui/{cbmc-timeout => harness-timeout}/no_timeout.rs (58%) rename tests/ui/{cbmc-timeout => harness-timeout}/timeout.expected (100%) rename tests/ui/{cbmc-timeout => harness-timeout}/timeout.rs (83%) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index e81ab12d8f6e..a2c230870aae 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -281,9 +281,9 @@ pub struct VerificationArgs { #[arg(long, hide = true)] pub print_llbc: bool, - /// Timeout for CBMC command in seconds + /// Timeout for each harness in seconds. This option is experimental and requires `-Z unstable-options` to be used. #[arg(long)] - pub cbmc_timeout: Option, + pub harness_timeout: Option, /// Arguments to pass down to Cargo #[command(flatten)] @@ -641,6 +641,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 index 975e38919e64..0566532dd9df 100644 --- 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::{call_cbmc::CbmcExitStatus, harness_runner::HarnessResult}; +use crate::{call_cbmc::ExitStatus, harness_runner::HarnessResult}; use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRow}; @@ -37,9 +37,9 @@ pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder 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}"), + 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(); diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 5d04903bd9b5..06e82103330f 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -50,7 +50,7 @@ pub enum FailedProperties { /// The possible CBMC exit statuses #[derive(Clone, Copy, Debug)] -pub enum CbmcExitStatus { +pub enum ExitStatus { Timeout, OutOfMemory, /// the integer is the process exit status @@ -68,7 +68,7 @@ pub struct VerificationResult { /// Note: CBMC process exit status is only potentially useful if `status` is `Failure`. /// Kani will see CBMC report "failure" that's actually success (interpreting "failed" /// checks like coverage as expected and desirable.) - pub results: Result, CbmcExitStatus>, + pub results: Result, ExitStatus>, /// The runtime duration of this CBMC invocation. pub runtime: Duration, /// Whether concrete playback generated a test @@ -119,7 +119,7 @@ impl KaniSession { let start_time = Instant::now(); - let res = if let Some(timeout) = self.args.cbmc_timeout { + let res = if let Some(timeout) = self.args.harness_timeout { tokio::time::timeout( std::time::Duration::from_secs(timeout.into()), process_cbmc_output(cbmc_process, |i| { @@ -149,7 +149,7 @@ impl KaniSession { VerificationResult { status: VerificationStatus::Failure, failed_properties: FailedProperties::None, - results: Err(CbmcExitStatus::Timeout), + results: Err(ExitStatus::Timeout), runtime: start_time.elapsed(), generated_concrete_test: false, coverage_results: None, @@ -352,9 +352,9 @@ impl VerificationResult { } else { // We never got results from CBMC - something went wrong (e.g. crash) so it's failure let exit_status = if output.process_status == 137 { - CbmcExitStatus::OutOfMemory + ExitStatus::OutOfMemory } else { - CbmcExitStatus::Other(output.process_status) + ExitStatus::Other(output.process_status) }; VerificationResult { status: VerificationStatus::Failure, @@ -385,7 +385,7 @@ impl VerificationResult { // on failure, exit codes in theory might be used, // but `mock_failure` should never be used in a context where they will, // so again use something weird: - results: Err(CbmcExitStatus::Other(42)), + results: Err(ExitStatus::Other(42)), runtime: Duration::from_secs(0), generated_concrete_test: false, coverage_results: None, @@ -417,18 +417,18 @@ impl VerificationResult { Err(exit_status) => { let verification_result = console::style("FAILED").red(); let (header, explanation) = match exit_status { - CbmcExitStatus::OutOfMemory => ( + ExitStatus::OutOfMemory => ( String::from("CBMC failed"), "CBMC appears to have run out of memory. You may want to rerun your proof in \ an environment with additional memory or use stubbing to reduce the size of the \ code the verifier reasons about.\n", ), - CbmcExitStatus::Timeout => ( + ExitStatus::Timeout => ( String::from("CBMC failed"), "CBMC timed out. You may want to rerun your proof with a larger timeout \ or use stubbing to reduce the size of the code the verifier reasons about.\n", ), - CbmcExitStatus::Other(exit_status) => { + ExitStatus::Other(exit_status) => { (format!("CBMC failed with status {exit_status}"), "") } }; diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index a9d39c63f510..140a20f506a6 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -121,7 +121,7 @@ impl KaniSession { /// Call [run_terminal_timeout] with the verbosity configured by the user. /// The `bool` value indicates whether the command timed out pub fn run_terminal_timeout(&self, cmd: TokioCommand) -> Result { - run_terminal_timeout(&self.args.common_args, cmd, &self.runtime, self.args.cbmc_timeout) + run_terminal_timeout(&self.args.common_args, cmd, &self.runtime, self.args.harness_timeout) } /// Call [run_suppress] with the verbosity configured by the user. diff --git a/tests/ui/cbmc-timeout/no_timeout.expected b/tests/ui/harness-timeout/no_timeout.expected similarity index 100% rename from tests/ui/cbmc-timeout/no_timeout.expected rename to tests/ui/harness-timeout/no_timeout.expected diff --git a/tests/ui/cbmc-timeout/no_timeout.rs b/tests/ui/harness-timeout/no_timeout.rs similarity index 58% rename from tests/ui/cbmc-timeout/no_timeout.rs rename to tests/ui/harness-timeout/no_timeout.rs index 71e152aed763..dea2b70d4718 100644 --- a/tests/ui/cbmc-timeout/no_timeout.rs +++ b/tests/ui/harness-timeout/no_timeout.rs @@ -1,9 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --cbmc-timeout 10 +// kani-flags: --harness-timeout 10 // -// Check the behavior of Kani when given a timeout via `--cbmc-timeout`, but -// CBMC completes before the timeout +// This test covers the case where a timeout is specified via `--harness-timeout`, but +// CBMC completes before the timeout is reached #[kani::proof] fn check_cbmc_no_timeout() { diff --git a/tests/ui/cbmc-timeout/timeout.expected b/tests/ui/harness-timeout/timeout.expected similarity index 100% rename from tests/ui/cbmc-timeout/timeout.expected rename to tests/ui/harness-timeout/timeout.expected diff --git a/tests/ui/cbmc-timeout/timeout.rs b/tests/ui/harness-timeout/timeout.rs similarity index 83% rename from tests/ui/cbmc-timeout/timeout.rs rename to tests/ui/harness-timeout/timeout.rs index 975009be1ac1..bb8588e60e58 100644 --- a/tests/ui/cbmc-timeout/timeout.rs +++ b/tests/ui/harness-timeout/timeout.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --cbmc-timeout 5 +// kani-flags: --harness-timeout 5 // -// Check that Kani respects the specified `--cbmc-timeout` option +// Check that Kani respects the specified `--harness-timeout` option #[kani::proof] fn check_cbmc_timeout() { From 0502cc20ac1296e10f0e7d4ad0a13c527f22f3a6 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 25 Oct 2024 17:12:02 -0700 Subject: [PATCH 4/6] Make function async and call block_on --- kani-driver/src/call_cbmc.rs | 10 +++++-- kani-driver/src/cbmc_output_parser.rs | 2 +- kani-driver/src/session.rs | 38 ++++++++++++++++---------- tests/ui/harness-timeout/no_timeout.rs | 2 +- tests/ui/harness-timeout/timeout.rs | 2 +- 5 files changed, 33 insertions(+), 21 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 06e82103330f..58ba10b7363e 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -112,7 +112,7 @@ impl KaniSession { println!("[Kani] Running: `{}`", render_command(cmd.as_std()).to_string_lossy()); } // Spawn the CBMC process and process its output below - let cbmc_process = cmd + let mut cbmc_process = cmd .stdout(std::process::Stdio::piped()) .spawn() .map_err(|_| anyhow::Error::msg("Failed to run cbmc"))?; @@ -122,7 +122,7 @@ impl KaniSession { let res = if let Some(timeout) = self.args.harness_timeout { tokio::time::timeout( std::time::Duration::from_secs(timeout.into()), - process_cbmc_output(cbmc_process, |i| { + process_cbmc_output(&mut cbmc_process, |i| { kani_cbmc_output_filter( i, self.args.extra_pointer_checks, @@ -133,7 +133,7 @@ impl KaniSession { ) .await } else { - Ok(process_cbmc_output(cbmc_process, |i| { + Ok(process_cbmc_output(&mut cbmc_process, |i| { kani_cbmc_output_filter( i, self.args.extra_pointer_checks, @@ -146,6 +146,10 @@ impl KaniSession { let verification_results = if res.is_err() { // An error occurs if the timeout was reached + + // Kill the process + cbmc_process.kill().await?; + VerificationResult { status: VerificationStatus::Failure, failed_properties: FailedProperties::None, diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index d2ae389c0063..a34f6815e3dd 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -521,7 +521,7 @@ pub struct VerificationOutput { /// /// The cbmc process status is returned, along with the (post-filter) items. pub async fn process_cbmc_output( - mut process: Child, + process: &mut Child, mut eager_filter: impl FnMut(ParserItem) -> Option, ) -> Result { let stdout = process.stdout.as_mut().unwrap(); diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 140a20f506a6..6e5bc505b614 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -121,7 +121,11 @@ impl KaniSession { /// Call [run_terminal_timeout] with the verbosity configured by the user. /// The `bool` value indicates whether the command timed out pub fn run_terminal_timeout(&self, cmd: TokioCommand) -> Result { - run_terminal_timeout(&self.args.common_args, cmd, &self.runtime, self.args.harness_timeout) + self.runtime.block_on(run_terminal_timeout( + &self.args.common_args, + cmd, + self.args.harness_timeout, + )) } /// Call [run_suppress] with the verbosity configured by the user. @@ -186,10 +190,9 @@ pub fn run_terminal(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()> } /// The `bool` value indicates whether the command timed out -fn run_terminal_timeout( +async fn run_terminal_timeout( verbosity: &impl Verbosity, mut cmd: TokioCommand, - runtime: &tokio::runtime::Runtime, timeout: Option, ) -> Result { if verbosity.quiet() { @@ -202,21 +205,26 @@ fn run_terminal_timeout( let program = cmd.as_std().get_program().to_string_lossy().to_string(); let result = with_timer( verbosity, - || { - runtime.block_on(async { - if let Some(timeout) = timeout { - tokio::time::timeout( - std::time::Duration::from_secs(timeout as u64), - cmd.status(), - ) - .await - } else { - Ok(cmd.status().await) + || async { + if let Some(timeout) = timeout { + let mut child = cmd.spawn().unwrap(); + let res = tokio::time::timeout( + std::time::Duration::from_secs(timeout as u64), + child.wait(), + ) + .await; + if res.is_err() { + // Kill the process + child.kill().await.unwrap(); } - }) + res + } else { + Ok(cmd.status().await) + } }, &program, - ); + ) + .await; // outer result indicates whether the command timed out if result.is_err() { return Ok(true); diff --git a/tests/ui/harness-timeout/no_timeout.rs b/tests/ui/harness-timeout/no_timeout.rs index dea2b70d4718..8d27fdf15fd9 100644 --- a/tests/ui/harness-timeout/no_timeout.rs +++ b/tests/ui/harness-timeout/no_timeout.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --harness-timeout 10 +// kani-flags: --harness-timeout 10 -Zunstable-options // // This test covers the case where a timeout is specified via `--harness-timeout`, but // CBMC completes before the timeout is reached diff --git a/tests/ui/harness-timeout/timeout.rs b/tests/ui/harness-timeout/timeout.rs index bb8588e60e58..a65fb8a9de94 100644 --- a/tests/ui/harness-timeout/timeout.rs +++ b/tests/ui/harness-timeout/timeout.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --harness-timeout 5 +// kani-flags: --harness-timeout 5 -Zunstable-options // // Check that Kani respects the specified `--harness-timeout` option From c96ea92a87dec18a485be6ba36dfd6b3bf6ca804 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 25 Oct 2024 23:17:44 -0700 Subject: [PATCH 5/6] Allow a unit suffix --- kani-driver/src/args/mod.rs | 57 ++++++++++++++++++++++- kani-driver/src/call_cbmc.rs | 2 +- kani-driver/src/session.rs | 9 ++-- tests/ui/harness-timeout/hours.expected | 1 + tests/ui/harness-timeout/hours.rs | 10 ++++ tests/ui/harness-timeout/invalid.expected | 1 + tests/ui/harness-timeout/invalid.rs | 10 ++++ tests/ui/harness-timeout/minutes.expected | 1 + tests/ui/harness-timeout/minutes.rs | 11 +++++ tests/ui/harness-timeout/no_timeout.rs | 2 +- tests/ui/harness-timeout/timeout.expected | 2 +- tests/ui/harness-timeout/timeout.rs | 2 +- 12 files changed, 96 insertions(+), 12 deletions(-) create mode 100644 tests/ui/harness-timeout/hours.expected create mode 100644 tests/ui/harness-timeout/hours.rs create mode 100644 tests/ui/harness-timeout/invalid.expected create mode 100644 tests/ui/harness-timeout/invalid.rs create mode 100644 tests/ui/harness-timeout/minutes.expected create mode 100644 tests/ui/harness-timeout/minutes.rs diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index a2c230870aae..e806ca858b5d 100644 --- 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,58 @@ 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)] +enum TimeUnit { + Seconds, + Minutes, + 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 { + 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::().map_err(|_| "Invalid timeout value")?; + + let unit = match unit_str.to_lowercase().as_str() { + "s" => TimeUnit::Seconds, + "m" => TimeUnit::Minutes, + "h" => TimeUnit::Hours, + _ => { + return Err( + "Invalid time unit. Use 's' for seconds, 'm' for minutes, or 'h' for hours" + .to_string(), + ); + } + }; + + Ok(Timeout { value, unit }) + } +} + +impl From 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,9 +334,9 @@ pub struct VerificationArgs { #[arg(long, hide = true)] pub print_llbc: bool, - /// Timeout for each harness in seconds. This option is experimental and requires `-Z unstable-options` to be used. + /// 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, + pub harness_timeout: Option, /// Arguments to pass down to Cargo #[command(flatten)] diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 58ba10b7363e..670a81f9d665 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -121,7 +121,7 @@ impl KaniSession { let res = if let Some(timeout) = self.args.harness_timeout { tokio::time::timeout( - std::time::Duration::from_secs(timeout.into()), + timeout.into(), process_cbmc_output(&mut cbmc_process, |i| { kani_cbmc_output_filter( i, diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 6e5bc505b614..2cf394184b4d 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -1,6 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use crate::args::Timeout; use crate::args::VerificationArgs; use crate::args::common::Verbosity; use crate::util::render_command; @@ -193,7 +194,7 @@ pub fn run_terminal(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()> async fn run_terminal_timeout( verbosity: &impl Verbosity, mut cmd: TokioCommand, - timeout: Option, + timeout: Option, ) -> Result { if verbosity.quiet() { cmd.stdout(std::process::Stdio::null()); @@ -208,11 +209,7 @@ async fn run_terminal_timeout( || async { if let Some(timeout) = timeout { let mut child = cmd.spawn().unwrap(); - let res = tokio::time::timeout( - std::time::Duration::from_secs(timeout as u64), - child.wait(), - ) - .await; + let res = tokio::time::timeout(timeout.into(), child.wait()).await; if res.is_err() { // Kill the process child.kill().await.unwrap(); diff --git a/tests/ui/harness-timeout/hours.expected b/tests/ui/harness-timeout/hours.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/ui/harness-timeout/hours.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/ui/harness-timeout/hours.rs b/tests/ui/harness-timeout/hours.rs new file mode 100644 index 000000000000..d003679daae4 --- /dev/null +++ b/tests/ui/harness-timeout/hours.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness-timeout 24h -Zunstable-options +// +// This test checks that Kani accepts a `--harness-timeout` specified in hours + +#[kani::proof] +fn check_harness_timeout_hours() { + assert_ne!(42, 17); +} diff --git a/tests/ui/harness-timeout/invalid.expected b/tests/ui/harness-timeout/invalid.expected new file mode 100644 index 000000000000..aa44e32a052d --- /dev/null +++ b/tests/ui/harness-timeout/invalid.expected @@ -0,0 +1 @@ +error: invalid value '5k' for '--harness-timeout ': Invalid time unit. Use 's' for seconds, 'm' for minutes, or 'h' for hours diff --git a/tests/ui/harness-timeout/invalid.rs b/tests/ui/harness-timeout/invalid.rs new file mode 100644 index 000000000000..4859ff4bc262 --- /dev/null +++ b/tests/ui/harness-timeout/invalid.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness-timeout 5k -Zunstable-options +// +// This test checks the error message when the argument to the `--harness-timeout` option is invalid + +#[kani::proof] +fn check_invalid_harness_timeout() { + assert!(true); +} diff --git a/tests/ui/harness-timeout/minutes.expected b/tests/ui/harness-timeout/minutes.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/ui/harness-timeout/minutes.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/ui/harness-timeout/minutes.rs b/tests/ui/harness-timeout/minutes.rs new file mode 100644 index 000000000000..4737a1f98a49 --- /dev/null +++ b/tests/ui/harness-timeout/minutes.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness-timeout 1m -Zunstable-options +// +// This test checks that Kani accepts a `--harness-timeout` specified in minutes + +#[kani::proof] +fn check_harness_timeout_minutes() { + let s = String::from("Hello, world!"); + assert_eq!(s.len(), 13); +} diff --git a/tests/ui/harness-timeout/no_timeout.rs b/tests/ui/harness-timeout/no_timeout.rs index 8d27fdf15fd9..493030fe378c 100644 --- a/tests/ui/harness-timeout/no_timeout.rs +++ b/tests/ui/harness-timeout/no_timeout.rs @@ -6,7 +6,7 @@ // CBMC completes before the timeout is reached #[kani::proof] -fn check_cbmc_no_timeout() { +fn check_harness_no_timeout() { let x: u8 = kani::any(); let y: u8 = kani::any(); kani::assume(y == 0); diff --git a/tests/ui/harness-timeout/timeout.expected b/tests/ui/harness-timeout/timeout.expected index 76102989b631..aefd7a340753 100644 --- a/tests/ui/harness-timeout/timeout.expected +++ b/tests/ui/harness-timeout/timeout.expected @@ -1,4 +1,4 @@ VERIFICATION:- FAILED CBMC timed out. You may want to rerun your proof with a larger timeout or use stubbing to reduce the size of the code the verifier reasons about. -Verification failed for - check_cbmc_timeout +Verification failed for - check_harness_timeout diff --git a/tests/ui/harness-timeout/timeout.rs b/tests/ui/harness-timeout/timeout.rs index a65fb8a9de94..4b63551a79ac 100644 --- a/tests/ui/harness-timeout/timeout.rs +++ b/tests/ui/harness-timeout/timeout.rs @@ -5,7 +5,7 @@ // Check that Kani respects the specified `--harness-timeout` option #[kani::proof] -fn check_cbmc_timeout() { +fn check_harness_timeout() { // construct a problem that requires a long time to solve let (a1, b1, c1): (u64, u64, u64) = kani::any(); let (a2, b2, c2): (u64, u64, u64) = kani::any(); From 482ed1130f4f75c1aa90896092758c2db0250301 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 29 Oct 2024 14:30:18 -0700 Subject: [PATCH 6/6] Use strum::EnumString --- kani-driver/src/args/mod.rs | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index e806ca858b5d..6901828b4dd7 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -63,10 +63,13 @@ 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)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, strum_macros::EnumString)] enum TimeUnit { + #[strum(serialize = "s")] Seconds, + #[strum(serialize = "m")] Minutes, + #[strum(serialize = "h")] Hours, } @@ -89,17 +92,9 @@ impl FromStr for Timeout { }; let value = value_str.parse::().map_err(|_| "Invalid timeout value")?; - let unit = match unit_str.to_lowercase().as_str() { - "s" => TimeUnit::Seconds, - "m" => TimeUnit::Minutes, - "h" => TimeUnit::Hours, - _ => { - return Err( - "Invalid time unit. Use 's' for seconds, 'm' for minutes, or 'h' for hours" - .to_string(), - ); - } - }; + 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 }) }