From 754dc57ef0edf24e91cc275731ac889fcef089cf Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 31 Jul 2024 09:56:00 +0000 Subject: [PATCH] Reduce CBMC verbosity to CBMC's default CBMC v6 included changes to hide timing information and loop unwinding status output at the default verbosity. To not impact Kani users, #2995 included changes to make Kani run CBMC with `--verbosity 9`. This change now makes Kani run CBMC with just the default verbosity, hiding timing information and loop unwinding status by default. If users still wish to see this information, they can invoke Kani with `--cbmc args --verbosity 9`. --- kani-driver/src/call_cbmc.rs | 5 ----- scripts/kani-perf.sh | 3 ++- tests/cargo-kani/simple-kissat/Cargo.toml | 2 +- tests/ui/solver-attribute/cadical/test.rs | 1 + tests/ui/solver-option/bin/test.rs | 2 +- tests/ui/solver-option/cadical/test.rs | 2 +- tests/ui/solver-option/kissat/test.rs | 2 +- tests/ui/solver-option/minisat/test.rs | 2 +- tools/benchcomp/test/test_regression.py | 6 ++++-- 9 files changed, 12 insertions(+), 13 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 387a9723fcdb..a0be50ab0428 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -153,11 +153,6 @@ impl KaniSession { args.push(file.to_owned().into_os_string()); - // Make CBMC verbose by default to tell users about unwinding progress. This should be - // reviewed as CBMC's verbosity defaults evolve. - args.push("--verbosity".into()); - args.push("9".into()); - Ok(args) } diff --git a/scripts/kani-perf.sh b/scripts/kani-perf.sh index a7e2710773aa..170ef7682e3b 100755 --- a/scripts/kani-perf.sh +++ b/scripts/kani-perf.sh @@ -27,7 +27,8 @@ done suite="perf" mode="cargo-kani-test" echo "Check compiletest suite=$suite mode=$mode" -cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast +cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast \ + --kani-flag="--enable-unstable" --kani-flag="--cbmc-args" --kani-flag="--verbosity" --kani-flag="9" exit_code=$? echo "Cleaning up..." diff --git a/tests/cargo-kani/simple-kissat/Cargo.toml b/tests/cargo-kani/simple-kissat/Cargo.toml index 3bde94c619fb..260c3f62313c 100644 --- a/tests/cargo-kani/simple-kissat/Cargo.toml +++ b/tests/cargo-kani/simple-kissat/Cargo.toml @@ -12,4 +12,4 @@ description = "Tests that Kani can be invoked with Kissat" [kani.flags] enable-unstable = true -cbmc-args = ["--external-sat-solver", "kissat" ] +cbmc-args = ["--external-sat-solver", "kissat", "--verbosity", "9" ] diff --git a/tests/ui/solver-attribute/cadical/test.rs b/tests/ui/solver-attribute/cadical/test.rs index d8e897f923fb..2c4feaa4c356 100644 --- a/tests/ui/solver-attribute/cadical/test.rs +++ b/tests/ui/solver-attribute/cadical/test.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --enable-unstable --cbmc-args --verbosity 9 //! Checks that `cadical` is a valid argument to `kani::solver` diff --git a/tests/ui/solver-option/bin/test.rs b/tests/ui/solver-option/bin/test.rs index 3529deb0eea9..c79618ecd028 100644 --- a/tests/ui/solver-option/bin/test.rs +++ b/tests/ui/solver-option/bin/test.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --solver bin=kissat +// kani-flags: --solver bin=kissat --enable-unstable --cbmc-args --verbosity 9 //! Checks that `--solver` accepts `bin=` diff --git a/tests/ui/solver-option/cadical/test.rs b/tests/ui/solver-option/cadical/test.rs index a7b6e1304bf3..8742c1e2df87 100644 --- a/tests/ui/solver-option/cadical/test.rs +++ b/tests/ui/solver-option/cadical/test.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --solver cadical +// kani-flags: --solver cadical --enable-unstable --cbmc-args --verbosity 9 //! Checks that the `cadical` is supported as an argument to `--solver` diff --git a/tests/ui/solver-option/kissat/test.rs b/tests/ui/solver-option/kissat/test.rs index 0b1403132ae3..4d876cdb952f 100644 --- a/tests/ui/solver-option/kissat/test.rs +++ b/tests/ui/solver-option/kissat/test.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --solver kissat +// kani-flags: --solver kissat --enable-unstable --cbmc-args --verbosity 9 //! Checks that the solver option overrides the solver attribute diff --git a/tests/ui/solver-option/minisat/test.rs b/tests/ui/solver-option/minisat/test.rs index b92a4cd1b6c6..44778fd4f704 100644 --- a/tests/ui/solver-option/minisat/test.rs +++ b/tests/ui/solver-option/minisat/test.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --solver minisat +// kani-flags: --solver minisat --enable-unstable --cbmc-args --verbosity 9 //! Checks that `--solver minisat` is accepted diff --git a/tools/benchcomp/test/test_regression.py b/tools/benchcomp/test/test_regression.py index ccf2259f7f0b..124e16b2ceb7 100644 --- a/tools/benchcomp/test/test_regression.py +++ b/tools/benchcomp/test/test_regression.py @@ -56,7 +56,8 @@ def test_kani_perf_fail(self): cmd = ( "rm -rf build target &&" "mkdir -p build/tests/perf/Unwind-Attribute/expected &&" - "kani tests/kani/Unwind-Attribute/fixme_lib.rs > " + "kani tests/kani/Unwind-Attribute/fixme_lib.rs " + "--enable-unstable --cbmc-args --verbosity 9 > " "build/tests/perf/Unwind-Attribute/expected/expected.out" ) self._run_kani_perf_test(cmd, False) @@ -65,7 +66,8 @@ def test_kani_perf_success(self): cmd = ( "rm -rf build target &&" "mkdir -p build/tests/perf/Arbitrary/expected &&" - "kani tests/kani/Arbitrary/arbitrary_impls.rs > " + "kani tests/kani/Arbitrary/arbitrary_impls.rs " + "--enable-unstable --cbmc-args --verbosity 9 > " "build/tests/perf/Arbitrary/expected/expected.out" ) self._run_kani_perf_test(cmd, True)