From 058ee88c1f7d0ba2bdbadd1c469585cda339bf7b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 26 Apr 2022 12:10:33 -0700 Subject: [PATCH] Audit command line arguments (#1106) * Remove unused --allow-cbmc-verification-failure flag * Cleaning up the kani arguments. - Removed --auto-unwind which as broken. - Fixed punctuation to be consistent. - Hide unstable / developer features from short help. * Fix --unwind conflict check We were not covering any other form of unwind. Note that this will also conflict with --unwinding-assertions which I think is probably fine since we have that option in Kani. --- kani-driver/src/args.rs | 64 ++++++++----------- kani-driver/src/call_cbmc.rs | 7 +- .../expected | 1 - .../dry-run-flag-unwind-conflict/expected | 1 + .../main.rs | 2 +- tests/expected/dry-run/main.rs | 2 +- tests/ui/code-location/main.rs | 2 +- tests/ui/code-location/module/mod.rs | 2 +- tests/ui/missing-function/extern_c.rs | 2 +- tools/bookrunner/src/util.rs | 4 +- 10 files changed, 36 insertions(+), 51 deletions(-) delete mode 100644 tests/expected/dry-run-flag-conflict-auto-unwind/expected create mode 100644 tests/expected/dry-run-flag-unwind-conflict/expected rename tests/expected/{dry-run-flag-conflict-auto-unwind => dry-run-flag-unwind-conflict}/main.rs (76%) diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs index 681ba6e3ef95b..babf6f265fb46 100644 --- a/kani-driver/src/args.rs +++ b/kani-driver/src/args.rs @@ -41,7 +41,7 @@ pub struct KaniArgs { #[structopt(long)] pub visualize: bool, /// Keep temporary files generated throughout Kani process - #[structopt(long)] + #[structopt(long, hidden_short_help(true))] pub keep_temps: bool, /// Produce full debug information @@ -53,20 +53,21 @@ pub struct KaniArgs { /// Output processing stages and commands, along with minor debug information #[structopt(long, short)] pub verbose: bool, - /// Enable usage of unstable options. + /// Enable usage of unstable options #[structopt(long, hidden_short_help(true))] pub enable_unstable: bool, + // Hide this since it depends on function that is a hidden option. /// Print commands instead of running them - #[structopt(long, requires("function"))] + #[structopt(long, requires("function"), hidden(true))] pub dry_run: bool, /// Generate C file equivalent to inputted program. - /// This feature is unstable and it requires `--enable-unstable` to be used. + /// This feature is unstable and it requires `--enable-unstable` to be used #[structopt(long, hidden_short_help(true), requires("enable-unstable"))] pub gen_c: bool, // TODO: currently only cargo-kani pays attention to this. - /// Directory for all generated artifacts + /// Directory for all generated artifacts. Only effective when running Kani with cargo #[structopt(long, parse(from_os_str))] pub target_dir: Option, @@ -77,8 +78,9 @@ pub struct KaniArgs { #[structopt(flatten)] pub checks: CheckArgs, - /// Entry point for verification (symbol name) - #[structopt(long, hidden = true)] + /// Entry point for verification (symbol name). + /// This is an unstable feature. Consider using --harness instead + #[structopt(long, hidden = true, requires("enable-unstable"))] pub function: Option, /// Entry point for verification (proof harness) // In a dry-run, we don't have kani-metadata.json to read, so we can't use this flag @@ -86,17 +88,14 @@ pub struct KaniArgs { pub harness: Option, /// Link external C files referenced by Rust code. - /// This is an experimental feature and requires `--enable-unstable` to be used. + /// This is an experimental feature and requires `--enable-unstable` to be used #[structopt(long, parse(from_os_str), hidden = true, requires("enable-unstable"))] pub c_lib: Vec, - /// Enable test function verification. Only use this option when the entry point is a test function. + /// Enable test function verification. Only use this option when the entry point is a test function #[structopt(long)] pub tests: bool, - /// Do not produce error return code on CBMC verification failure + /// Kani will only compile the crate. No verification will be performed #[structopt(long, hidden_short_help(true))] - pub allow_cbmc_verification_failure: bool, - /// Kani will only compile the crate - #[structopt(long)] pub only_codegen: bool, /// Specify the number of bits used for representing object IDs in CBMC @@ -108,23 +107,20 @@ pub struct KaniArgs { /// Specify the value used for loop unwinding for the specified harness in CBMC #[structopt(long, requires("harness"))] pub unwind: Option, - /// Turn on automatic loop unwinding - #[structopt(long)] - pub auto_unwind: bool, - /// Pass through directly to CBMC; must be the last flag - /// This feature is unstable and it requires `--enable-unstable` to be used. + /// Pass through directly to CBMC; must be the last flag. + /// This feature is unstable and it requires `--enable-unstable` to be used #[structopt(long, allow_hyphen_values = true, min_values(0), requires("enable-unstable"))] // consumes everything pub cbmc_args: Vec, // Hide option till https://github.com/model-checking/kani/issues/697 is - // fixed - /// Use abstractions for the standard library - /// This is an experimental feature and requires `--enable-unstable` to be used. + // fixed. + /// Use abstractions for the standard library. + /// This is an experimental feature and requires `--enable-unstable` to be used #[structopt(long, hidden = true, requires("enable-unstable"))] pub use_abs: bool, // Hide option till https://github.com/model-checking/kani/issues/697 is - // fixed + // fixed. /// Choose abstraction for modules of standard library if available #[structopt(long, default_value = "std", possible_values = &AbstractionType::variants(), case_insensitive = true, hidden = true)] @@ -133,12 +129,12 @@ pub struct KaniArgs { /// Enable extra pointer checks such as invalid pointers in relation operations and pointer /// arithmetic overflow. /// This feature is unstable and it may yield false counter examples. It requires - /// `--enable-unstable` to be used. + /// `--enable-unstable` to be used #[structopt(long, hidden_short_help(true), requires("enable-unstable"))] pub extra_pointer_checks: bool, - /// Restrict the targets of virtual table function pointer calls - /// This feature is unstable and it requires `--enable-unstable` to be used. + /// Restrict the targets of virtual table function pointer calls. + /// This feature is unstable and it requires `--enable-unstable` to be used #[structopt(long, hidden_short_help(true), requires("enable-unstable"))] pub restrict_vtable: bool, /// Disable restricting the targets of virtual table function pointer calls @@ -283,23 +279,13 @@ impl CargoKaniArgs { } impl KaniArgs { pub fn validate(&self) { - let extra_unwind = self.cbmc_args.contains(&OsString::from("--unwind")); - let extra_auto_unwind = self.cbmc_args.contains(&OsString::from("--auto-unwind")); - let extras = extra_auto_unwind || extra_unwind; - let natives = self.auto_unwind || self.default_unwind.is_some(); - let any_auto_unwind = extra_auto_unwind || self.auto_unwind; - let any_unwind = self.default_unwind.is_some() || extra_unwind; + let extra_unwind = + self.cbmc_args.iter().any(|s| s.to_str().unwrap().starts_with("--unwind")); + let natives_unwind = self.default_unwind.is_some() || self.unwind.is_some(); // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified. // We should consider improving the error messages slightly in a later pull request. - if any_auto_unwind && any_unwind { - Error::with_description( - "Conflicting flags: `--auto-unwind` is not compatible with other `--default-unwind` flags.", - ErrorKind::ArgumentConflict, - ) - .exit(); - } - if natives && extras { + if natives_unwind && extra_unwind { Error::with_description( "Conflicting flags: unwind flags provided to kani and in --cbmc-args.", ErrorKind::ArgumentConflict, diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index f54776975cadb..6025dbc96c45f 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -33,8 +33,7 @@ impl KaniSession { cmd.args(args); if self.args.output_format == crate::args::OutputFormat::Old { - let result = self.run_terminal(cmd); - if !self.args.allow_cbmc_verification_failure && result.is_err() { + if self.run_terminal(cmd).is_err() { return Ok(VerificationStatus::Failure); } } else { @@ -44,7 +43,7 @@ impl KaniSession { let _cbmc_result = self.run_redirect(cmd, &output_filename)?; let format_result = self.format_cbmc_output(&output_filename); - if !self.args.allow_cbmc_verification_failure && format_result.is_err() { + if format_result.is_err() { // Because of things like --assertion-reach-checks and other future features, // we now decide if we fail or not based solely on the output of the formatter. return Ok(VerificationStatus::Failure); @@ -88,8 +87,6 @@ impl KaniSession { if let Some(unwind_value) = resolve_unwind_value(&self.args, harness_metadata) { args.push("--unwind".into()); args.push(unwind_value.to_string().into()); - } else if self.args.auto_unwind { - args.push("--auto-unwind".into()); } args.extend(self.args.cbmc_args.iter().cloned()); diff --git a/tests/expected/dry-run-flag-conflict-auto-unwind/expected b/tests/expected/dry-run-flag-conflict-auto-unwind/expected deleted file mode 100644 index ff9e37aacd50b..0000000000000 --- a/tests/expected/dry-run-flag-conflict-auto-unwind/expected +++ /dev/null @@ -1 +0,0 @@ -Conflicting flags: `--auto-unwind` is not compatible with other `--default-unwind` flags. \ No newline at end of file diff --git a/tests/expected/dry-run-flag-unwind-conflict/expected b/tests/expected/dry-run-flag-unwind-conflict/expected new file mode 100644 index 0000000000000..7ff5525dd449b --- /dev/null +++ b/tests/expected/dry-run-flag-unwind-conflict/expected @@ -0,0 +1 @@ +error: Conflicting flags: unwind flags provided to kani and in --cbmc-args. diff --git a/tests/expected/dry-run-flag-conflict-auto-unwind/main.rs b/tests/expected/dry-run-flag-unwind-conflict/main.rs similarity index 76% rename from tests/expected/dry-run-flag-conflict-auto-unwind/main.rs rename to tests/expected/dry-run-flag-unwind-conflict/main.rs index fbc132f886cb8..28106d16667e8 100644 --- a/tests/expected/dry-run-flag-conflict-auto-unwind/main.rs +++ b/tests/expected/dry-run-flag-unwind-conflict/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --dry-run --auto-unwind --default-unwind 2 --enable-unstable --function main +// kani-flags: --dry-run --default-unwind 2 --enable-unstable --function main --cbmc-args --unwindset 2 // `--dry-run` causes Kani to print out commands instead of running them // In `expected` you will find substrings of these commands because the diff --git a/tests/expected/dry-run/main.rs b/tests/expected/dry-run/main.rs index 4d10b02857cd1..bda6e55383709 100644 --- a/tests/expected/dry-run/main.rs +++ b/tests/expected/dry-run/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --dry-run --function main +// kani-flags: --dry-run --function main --enable-unstable // `--dry-run` causes Kani to print out commands instead of running them // In `expected` you will find substrings of these commands because the diff --git a/tests/ui/code-location/main.rs b/tests/ui/code-location/main.rs index 3b5bef4dfe11d..e4d88bd69a85f 100644 --- a/tests/ui/code-location/main.rs +++ b/tests/ui/code-location/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --function harness +// kani-flags: --harness harness // //! This test is to check how file names are displayed in the Kani output. diff --git a/tests/ui/code-location/module/mod.rs b/tests/ui/code-location/module/mod.rs index 8bc84e5653154..884ef8e1bdffa 100644 --- a/tests/ui/code-location/module/mod.rs +++ b/tests/ui/code-location/module/mod.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --function empty_harness +// kani-flags: --harness empty_harness // This file is to be used as a module on a different test, but the compiletest will still run // kani on this file. Use an empty harness instead. diff --git a/tests/ui/missing-function/extern_c.rs b/tests/ui/missing-function/extern_c.rs index b1d95f523f5b6..2c2add19da3ce 100644 --- a/tests/ui/missing-function/extern_c.rs +++ b/tests/ui/missing-function/extern_c.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --function harness +// kani-flags: --harness harness // This test is to check Kani's error handling for missing functions. // TODO: Verify that this prints a compiler warning: diff --git a/tools/bookrunner/src/util.rs b/tools/bookrunner/src/util.rs index dde493d7ec417..c58041b2fd27e 100644 --- a/tools/bookrunner/src/util.rs +++ b/tools/bookrunner/src/util.rs @@ -205,7 +205,9 @@ pub fn add_verification_job(litani: &mut Litani, test_props: &TestProps) { let mut kani = Command::new("kani"); // Add `--function main` so we can run these without having to amend them to add `#[kani::proof]`. // Some of test_props.kani_args will contains `--cbmc-args` so we should always put that last. - kani.arg(&test_props.path).args(&["--function", "main"]).args(&test_props.kani_args); + kani.arg(&test_props.path) + .args(&["--enable-unstable", "--function", "main"]) + .args(&test_props.kani_args); if !test_props.rustc_args.is_empty() { kani.env("RUSTFLAGS", test_props.rustc_args.join(" ")); }