From baf677743676b64f106ba5273447dec9b353efd9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 31 Jul 2026 18:43:58 +0000 Subject: [PATCH 1/2] Autoharness: verify harnesses in parallel by default Autoharness typically generates hundreds of harnesses, for which the sequential default of the shared harness runner is a poor fit: in a top-100 crates.io evaluation, 12 crates hit a 30-minute wall-clock cap. Kani already supports parallel harness verification behind --jobs (which requires --output-format=terse); with -j 16, num-traits went from timing out at 1800s to completing all 1,983 generated harnesses in 330s. Default autoharness to --jobs (thread-pool default) with terse output when the user passes neither option. Explicit choices are always preserved: --output-format=regular restores sequential verification with detailed output, and the parse-time validation that --jobs requires terse output is unaffected. Plain 'kani'/'cargo kani' verification is unchanged. To distinguish an explicit --output-format=regular from the clap default, the output_format argument becomes Option with an accessor defaulting to Regular. Existing autoharness tests assert on ordered per-harness output, so they pin --output-format=regular (also covering the opt-out); a new test pins the parallel default via order-independent assertions. Co-authored-by: Kiro --- .../src/reference/experimental/autoharness.md | 8 ++++ kani-driver/src/args/mod.rs | 37 ++++++++++++++----- kani-driver/src/autoharness/mod.rs | 1 + kani-driver/src/call_cbmc.rs | 6 +-- kani-driver/src/harness_runner.rs | 4 +- .../autoharness-refs_immutable/run.sh | 2 +- .../autoharness-refs_mutable/run.sh | 2 +- .../cargo_autoharness_contracts/contracts.sh | 2 +- .../dependencies.sh | 2 +- .../cargo_autoharness_exclude/exclude.sh | 2 +- .../cargo_autoharness_filter/filter.sh | 2 +- .../harnesses_fail.sh | 2 +- .../cargo_autoharness_include/include.sh | 2 +- .../cargo_autoharness_parallel/Cargo.toml | 6 +++ .../cargo_autoharness_parallel/config.yml | 4 ++ .../parallel.expected | 6 +++ .../cargo_autoharness_parallel/parallel.sh | 18 +++++++++ .../cargo_autoharness_parallel/src/lib.rs | 20 ++++++++++ .../termination_timeout.sh | 2 +- .../termination_unwind.sh | 2 +- .../type-invariant.sh | 2 +- 21 files changed, 107 insertions(+), 25 deletions(-) create mode 100644 tests/script-based-pre/cargo_autoharness_parallel/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoharness_parallel/config.yml create mode 100644 tests/script-based-pre/cargo_autoharness_parallel/parallel.expected create mode 100755 tests/script-based-pre/cargo_autoharness_parallel/parallel.sh create mode 100644 tests/script-based-pre/cargo_autoharness_parallel/src/lib.rs diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index efba41a3ee1e..6f0666c569f3 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -79,6 +79,14 @@ Autoharness also accepts a `--list` argument, which runs the [list subcommand](. For a full list of options, run `kani autoharness --help`. +### Parallel verification + +Since autoharness typically generates many harnesses, it verifies them in parallel by default, +using the `--jobs` option with the thread pool's default number of threads and +`--output-format=terse`. Pass `-j ` to control the number of threads, or +`--output-format=regular` to verify harnesses sequentially with Kani's default, more detailed +output. + ## Example Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again: ```rust diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index e7636d1a45ae..14c6e173d0c3 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -338,9 +338,11 @@ pub struct VerificationArgs { #[arg(long, hide_short_help = true)] pub only_codegen: bool, - /// Toggle between different styles of output - #[arg(long, default_value = "regular", ignore_case = true, value_enum)] - pub output_format: OutputFormat, + /// Toggle between different styles of output. Defaults to "regular", except for + /// `autoharness`, which defaults to "terse" (to support parallel harness verification, + /// c.f. `--jobs`) unless this option is passed explicitly. + #[arg(long, ignore_case = true, value_enum)] + pub output_format: Option, /// Write verification results into per-harness files, rather than to stdout #[arg(long, hide_short_help = true)] @@ -499,6 +501,23 @@ impl VerificationArgs { } } + /// The output format, defaulting to `regular` when the user did not specify one. + pub fn output_format(&self) -> OutputFormat { + self.output_format.unwrap_or(OutputFormat::Regular) + } + + /// Default to parallel harness verification with terse output for `autoharness`, which + /// typically generates hundreds of harnesses; sequential verification is a poor fit. + /// Explicit user choices are always preserved, and the parse-time validation that + /// `--jobs` requires `--output-format=terse` is unaffected (these defaults are applied + /// after it, and only when neither option was passed). + pub fn apply_autoharness_parallel_defaults(&mut self) { + if self.jobs.is_none() && self.output_format.is_none() { + self.jobs = Some(None); // `-j`: the thread pool's default thread count + self.output_format = Some(OutputFormat::Terse); + } + } + /// Computes how many threads should be used to verify harnesses. pub fn jobs(&self) -> NumThreads { match self.jobs { @@ -528,7 +547,7 @@ pub enum ConcretePlaybackMode { InPlace, } -#[derive(Clone, Debug, PartialEq, Eq, ValueEnum)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, ValueEnum)] pub enum OutputFormat { Regular, Terse, @@ -796,14 +815,14 @@ impl ValidateArgs for VerificationArgs { "Conflicting options: --concrete-playback=print and --quiet.", )); } - if self.concrete_playback.is_some() && self.output_format == OutputFormat::Old { + if self.concrete_playback.is_some() && self.output_format() == OutputFormat::Old { return Err(Error::raw( ErrorKind::ArgumentConflict, "Conflicting options: --concrete-playback isn't compatible with \ --output-format=old.", )); } - if self.sarif.is_some() && self.output_format == OutputFormat::Old { + if self.sarif.is_some() && self.output_format() == OutputFormat::Old { return Err(Error::raw( ErrorKind::ArgumentConflict, "Conflicting options: --sarif isn't compatible with --output-format=old.", @@ -812,7 +831,7 @@ impl ValidateArgs for VerificationArgs { // `--output-format=old` bypasses CBMC's structured output entirely: `run_cbmc` mocks a // result with no properties, and treats a timeout as success. An export produced from // that would be indistinguishable from a real clean run. - if self.export_json.is_some() && self.output_format == OutputFormat::Old { + if self.export_json.is_some() && self.output_format() == OutputFormat::Old { return Err(Error::raw( ErrorKind::ArgumentConflict, "Conflicting options: --export-json isn't compatible with --output-format=old.", @@ -844,7 +863,7 @@ impl ValidateArgs for VerificationArgs { ), )); } - if self.jobs().will_multithread() && self.output_format != OutputFormat::Terse { + if self.jobs().will_multithread() && self.output_format() != OutputFormat::Terse { // More verbose output formats make it hard to interpret output right now when run in parallel. // This can be removed when we change up how results are printed. return Err(Error::raw( @@ -852,7 +871,7 @@ impl ValidateArgs for VerificationArgs { "Conflicting options: --jobs requires `--output-format=terse`", )); } - if self.log_file.is_some() && self.output_format == OutputFormat::Old { + if self.log_file.is_some() && self.output_format() == OutputFormat::Old { // `old` runs CBMC with inherited stdio instead of piping it, so neither // `kani_cbmc_output_filter` nor `process_output` runs and nothing but the // per-harness "Checking harness ..." lines reaches the log. Accepting the diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 4367f9ad2957..007b1c558238 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -52,6 +52,7 @@ pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> { /// Execute autoharness-specific KaniSession configuration. fn setup_session(session: &mut KaniSession, common_autoharness_args: &CommonAutoharnessArgs) { + session.args.apply_autoharness_parallel_defaults(); session.enable_autoharness(); session.add_default_bounds(); session.add_auto_harness_args( diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index b06a2c2362a2..760e94723026 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -225,7 +225,7 @@ impl KaniSession { let mut cmd = TokioCommand::new("cbmc"); cmd.args(args); - let verification_results = if self.args.output_format == crate::args::OutputFormat::Old { + let verification_results = if self.args.output_format() == crate::args::OutputFormat::Old { if self.run_terminal_timeout(cmd).is_err() { VerificationResult::mock_failure() } else { @@ -267,7 +267,7 @@ impl KaniSession { i, self.args.extra_pointer_checks, self.args.common_args.quiet, - &self.args.output_format, + &self.args.output_format(), self.args.log_file.as_ref(), ) }), @@ -279,7 +279,7 @@ impl KaniSession { i, self.args.extra_pointer_checks, self.args.common_args.quiet, - &self.args.output_format, + &self.args.output_format(), self.args.log_file.as_ref(), ) }) diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 7731193acc94..f470e529bf6e 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -174,7 +174,7 @@ impl KaniSession { self.write_output_to_file(result, harness, thread_index); } - let output = result.render(&self.args.output_format, harness.attributes.should_panic); + let output = result.render(&self.args.output_format(), harness.attributes.should_panic); if rayon::current_num_threads() > 1 { self.emit_line(&format!("Thread {thread_index}: {output}")); @@ -200,7 +200,7 @@ impl KaniSession { } fn should_print_output(&self) -> bool { - !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old + !self.args.common_args.quiet && self.args.output_format() != OutputFormat::Old } fn write_output_to_file( diff --git a/tests/script-based-pre/autoharness-refs_immutable/run.sh b/tests/script-based-pre/autoharness-refs_immutable/run.sh index 2350c1bc9d76..37a0c620c2be 100755 --- a/tests/script-based-pre/autoharness-refs_immutable/run.sh +++ b/tests/script-based-pre/autoharness-refs_immutable/run.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -kani autoharness -Z autoharness immutable.rs +kani autoharness -Z autoharness --output-format=regular immutable.rs diff --git a/tests/script-based-pre/autoharness-refs_mutable/run.sh b/tests/script-based-pre/autoharness-refs_mutable/run.sh index 3fe10b1602e7..d5a3299e3e00 100755 --- a/tests/script-based-pre/autoharness-refs_mutable/run.sh +++ b/tests/script-based-pre/autoharness-refs_mutable/run.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -kani autoharness -Z autoharness mutable.rs +kani autoharness -Z autoharness --output-format=regular mutable.rs diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh b/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh index db4a99f8be09..16060e2fd373 100755 --- a/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness +cargo kani autoharness -Z autoharness --output-format=regular diff --git a/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh b/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh index 0e0f76e871ea..bf93a6c7f6d2 100755 --- a/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh +++ b/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness \ No newline at end of file +cargo kani autoharness -Z autoharness --output-format=regular \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh b/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh index a18bd9ad4e29..e6159acf42b0 100755 --- a/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh +++ b/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness --exclude-pattern exclude +cargo kani autoharness -Z autoharness --output-format=regular --exclude-pattern exclude diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.sh b/tests/script-based-pre/cargo_autoharness_filter/filter.sh index db4a99f8be09..16060e2fd373 100755 --- a/tests/script-based-pre/cargo_autoharness_filter/filter.sh +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness +cargo kani autoharness -Z autoharness --output-format=regular diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh index 0e0f76e871ea..bf93a6c7f6d2 100755 --- a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness \ No newline at end of file +cargo kani autoharness -Z autoharness --output-format=regular \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoharness_include/include.sh b/tests/script-based-pre/cargo_autoharness_include/include.sh index a731584349bf..373f4fff000a 100755 --- a/tests/script-based-pre/cargo_autoharness_include/include.sh +++ b/tests/script-based-pre/cargo_autoharness_include/include.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness --include-pattern cargo_autoharness_include::include +cargo kani autoharness -Z autoharness --output-format=regular --include-pattern cargo_autoharness_include::include diff --git a/tests/script-based-pre/cargo_autoharness_parallel/Cargo.toml b/tests/script-based-pre/cargo_autoharness_parallel/Cargo.toml new file mode 100644 index 000000000000..e5ac92256cd8 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_parallel/Cargo.toml @@ -0,0 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "cargo_autoharness_parallel" +version = "0.1.0" +edition = "2021" diff --git a/tests/script-based-pre/cargo_autoharness_parallel/config.yml b/tests/script-based-pre/cargo_autoharness_parallel/config.yml new file mode 100644 index 000000000000..ff48e66defb8 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_parallel/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: parallel.sh +expected: parallel.expected diff --git a/tests/script-based-pre/cargo_autoharness_parallel/parallel.expected b/tests/script-based-pre/cargo_autoharness_parallel/parallel.expected new file mode 100644 index 000000000000..82c766c76965 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_parallel/parallel.expected @@ -0,0 +1,6 @@ +PARALLEL: yes +| f1 | #[kani::proof] | Success +| f2 | #[kani::proof] | Success +| f3 | #[kani::proof] | Success +| f4 | #[kani::proof] | Success +Complete - 4 successfully verified functions, 0 failures, 4 total. diff --git a/tests/script-based-pre/cargo_autoharness_parallel/parallel.sh b/tests/script-based-pre/cargo_autoharness_parallel/parallel.sh new file mode 100755 index 000000000000..7f49424112b0 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_parallel/parallel.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Autoharness defaults to parallel verification (-j) with terse output. Harness results +# arrive in nondeterministic order, so assert on order-independent evidence: the thread +# prefixes, the (sorted) per-function summary lines, and the totals line. +output=$(cargo kani autoharness -Z autoharness 2>&1) + +if echo "$output" | grep -q "Thread [0-9]*:"; then + echo "PARALLEL: yes" +else + echo "PARALLEL: no" + echo "$output" +fi + +echo "$output" | grep -oE '\| f[0-9] .*(Success|Failure)' | tr -s ' ' | sort +echo "$output" | grep "^Complete - " diff --git a/tests/script-based-pre/cargo_autoharness_parallel/src/lib.rs b/tests/script-based-pre/cargo_autoharness_parallel/src/lib.rs new file mode 100644 index 000000000000..7c801d4f995a --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_parallel/src/lib.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that autoharness defaults to parallel harness verification with terse output +//! (users can opt back into sequential verification with --output-format=regular). + +pub fn f1(x: u8) -> u8 { + x.wrapping_add(1) +} + +pub fn f2(x: u16) -> u16 { + x.wrapping_mul(2) +} + +pub fn f3(x: u32) -> u32 { + x ^ 0xdead_beef +} + +pub fn f4(x: bool) -> bool { + !x +} diff --git a/tests/script-based-pre/cargo_autoharness_termination_timeout/termination_timeout.sh b/tests/script-based-pre/cargo_autoharness_termination_timeout/termination_timeout.sh index db4a99f8be09..16060e2fd373 100755 --- a/tests/script-based-pre/cargo_autoharness_termination_timeout/termination_timeout.sh +++ b/tests/script-based-pre/cargo_autoharness_termination_timeout/termination_timeout.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness +cargo kani autoharness -Z autoharness --output-format=regular diff --git a/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.sh b/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.sh index b197c0b1e077..09f2741de15f 100755 --- a/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.sh +++ b/tests/script-based-pre/cargo_autoharness_termination_unwind/termination_unwind.sh @@ -4,4 +4,4 @@ # Set the timeout to 5m to ensure that the gcd_recursion test gets killed because of the unwind bound # and not because CBMC times out. -cargo kani autoharness -Z autoharness --harness-timeout 5m -Z unstable-options +cargo kani autoharness -Z autoharness --output-format=regular --harness-timeout 5m -Z unstable-options diff --git a/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.sh b/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.sh index db4a99f8be09..16060e2fd373 100755 --- a/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.sh +++ b/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness +cargo kani autoharness -Z autoharness --output-format=regular From d342cec9bdbb2ac30928300cfcb9e71bcdba1b11 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 5 Aug 2026 09:45:30 +0000 Subject: [PATCH 2/2] Pin --output-format=regular in the autoderive tests too They assert on ordered per-harness regular output, like the autoharness tests pinned previously; missed because their directory names do not match the autoharness glob. Co-authored-by: Kiro --- .../src/reference/experimental/autoharness.md | 24 ++++-- kani-driver/src/args/mod.rs | 75 +++++++++++++++++-- kani-driver/src/autoharness/mod.rs | 3 + kani-driver/src/main.rs | 14 +++- .../autoderive_arbitrary_enums/enums.sh | 2 +- .../autoderive_arbitrary_structs/structs.sh | 2 +- .../cargo_autoharness_bounded/bounded.sh | 2 +- .../dependencies.sh | 2 +- .../harnesses_fail.sh | 2 +- .../parallel.expected | 1 + .../cargo_autoharness_parallel/parallel.sh | 23 +++++- .../cargo_autoharness_slices/slices.sh | 2 +- .../smart-pointers.sh | 2 +- 13 files changed, 131 insertions(+), 23 deletions(-) diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index 6f0666c569f3..6a5750de9dbf 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -82,10 +82,21 @@ For a full list of options, run `kani autoharness --help`. ### Parallel verification Since autoharness typically generates many harnesses, it verifies them in parallel by default, -using the `--jobs` option with the thread pool's default number of threads and -`--output-format=terse`. Pass `-j ` to control the number of threads, or -`--output-format=regular` to verify harnesses sequentially with Kani's default, more detailed -output. +i.e. as if `--jobs` (the thread pool's default number of threads, normally one per logical CPU) +and `--output-format=terse` had been passed. Note that plain `kani`/`cargo kani` verification is +unaffected and remains sequential by default. + +To override the default: +- `-j ` / `--jobs=` caps the number of harnesses verified concurrently. Each thread runs + its own CBMC process, so peak memory grows with the number of threads; lower `` if a run + exhausts the available memory. `--jobs=1` keeps the terse output but verifies sequentially. +- `--output-format=regular` verifies harnesses sequentially, with Kani's default, more detailed + per-check output. (Parallel verification requires terse output, because interleaved detailed + output is hard to read; passing `--jobs` together with `--output-format=regular` is therefore + an error.) + +In parallel runs each harness result line is prefixed with the thread that produced it, and +results arrive in nondeterministic order; the summary table printed at the end is always sorted. ## Example Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again: @@ -93,10 +104,11 @@ Using the `estimate_size` example from [First Steps](../../tutorial-first-steps. {{#include ../../tutorial/first-steps-v1/src/lib.rs:code}} ``` -We get: +We get (passing `--output-format=regular` so that the per-check detail is shown, c.f. +[Parallel verification](#parallel-verification)): ``` -# cargo kani autoharness -Z autoharness +# cargo kani autoharness -Z autoharness --output-format=regular Autoharness: Checking function estimate_size against all possible inputs... RESULTS: Check 3: estimate_size.assertion.1 diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 14c6e173d0c3..3f4bdf05b8fe 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -508,14 +508,22 @@ impl VerificationArgs { /// Default to parallel harness verification with terse output for `autoharness`, which /// typically generates hundreds of harnesses; sequential verification is a poor fit. - /// Explicit user choices are always preserved, and the parse-time validation that - /// `--jobs` requires `--output-format=terse` is unaffected (these defaults are applied - /// after it, and only when neither option was passed). + /// + /// Explicit user choices are preserved: `--output-format` is only defaulted when the user + /// did not pass it, and `--jobs` is only defaulted when the user did not pass it *and* the + /// resulting format is `terse` (parallel verification requires terse output, c.f. + /// `validate`). Consequently `--output-format=regular` (or `old`) opts back into sequential + /// verification, while a bare `--jobs=N` still gets the terse output it needs. + /// + /// This must run *before* argument validation, so that validation sees the options the run + /// will actually use; it is idempotent, so calling it again later is harmless. pub fn apply_autoharness_parallel_defaults(&mut self) { - if self.jobs.is_none() && self.output_format.is_none() { - self.jobs = Some(None); // `-j`: the thread pool's default thread count + if self.output_format.is_none() { self.output_format = Some(OutputFormat::Terse); } + if self.jobs.is_none() && self.output_format() == OutputFormat::Terse { + self.jobs = Some(None); // `-j`: the thread pool's default thread count + } } /// Computes how many threads should be used to verify harnesses. @@ -1406,4 +1414,61 @@ mod tests { let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err(); assert_eq!(err.kind(), ErrorKind::MissingRequiredArgument); } + + /// `autoharness` verifies harnesses in parallel by default, which requires terse output. + /// Check each combination of explicitly passed / defaulted `--jobs` and `--output-format`. + #[test] + fn check_autoharness_parallel_defaults() { + let effective = |extra: &str| { + let args = format!("kani autoharness -Z autoharness {extra} input.rs"); + let parsed = StandaloneArgs::try_parse_from(args.split_whitespace()).unwrap(); + let Some(StandaloneSubcommand::Autoharness(mut autoharness)) = parsed.command else { + panic!("expected the autoharness subcommand"); + }; + autoharness.verify_opts.apply_autoharness_parallel_defaults(); + (autoharness.verify_opts.jobs(), autoharness.verify_opts.output_format()) + }; + + // Neither option passed: parallel with terse output. + assert_eq!(effective(""), (NumThreads::ThreadPoolDefault, OutputFormat::Terse)); + // Only `--jobs`: the user's thread count, plus the terse output it requires. + assert_eq!(effective("--jobs=4"), (NumThreads::UserSpecified(4), OutputFormat::Terse)); + // Only `--output-format=terse`: parallel, since terse is what parallel needs. + assert_eq!( + effective("--output-format=terse"), + (NumThreads::ThreadPoolDefault, OutputFormat::Terse) + ); + // A more verbose format opts back into sequential verification. + assert_eq!( + effective("--output-format=regular"), + (NumThreads::NoMultithreading, OutputFormat::Regular) + ); + assert_eq!( + effective("--output-format=old"), + (NumThreads::NoMultithreading, OutputFormat::Old) + ); + + // Applying the defaults is idempotent, and plain verification is unaffected. + let args = "kani input.rs".split_whitespace(); + let parsed = StandaloneArgs::try_parse_from(args).unwrap(); + assert_eq!(parsed.verify_opts.jobs(), NumThreads::NoMultithreading); + assert_eq!(parsed.verify_opts.output_format(), OutputFormat::Regular); + } + + /// `--jobs` with an explicitly requested non-terse format stays an error, for `autoharness` + /// (where the defaults cannot silently override the user) as well as plain verification. + #[test] + fn check_jobs_still_requires_terse() { + for args in [ + "kani autoharness -Z autoharness --jobs=4 --output-format=regular input.rs", + "kani --jobs=4 input.rs", + ] { + let mut parsed = StandaloneArgs::try_parse_from(args.split_whitespace()).unwrap(); + if let Some(StandaloneSubcommand::Autoharness(autoharness)) = &mut parsed.command { + autoharness.verify_opts.apply_autoharness_parallel_defaults(); + } + let err = parsed.validate().unwrap_err(); + assert_eq!(err.kind(), ErrorKind::ArgumentConflict, "for `{args}`"); + } + } } diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 007b1c558238..6edd62d769c6 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -52,6 +52,9 @@ pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> { /// Execute autoharness-specific KaniSession configuration. fn setup_session(session: &mut KaniSession, common_autoharness_args: &CommonAutoharnessArgs) { + // `main` already applies these before validating the arguments (so that validation sees the + // options the run will actually use); repeat it here -- the call is idempotent -- so that the + // session is configured correctly regardless of how it was constructed. session.args.apply_autoharness_parallel_defaults(); session.enable_autoharness(); session.add_default_bounds(); diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 7c28dbf7090b..e6ed618e1baf 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -82,7 +82,13 @@ fn main() -> ExitCode { /// The main function for the `cargo kani` command. fn cargokani_main(input_args: Vec) -> Result<()> { let input_args = join_args(input_args)?; - let args = args::CargoKaniArgs::parse_from(&input_args); + let mut args = args::CargoKaniArgs::parse_from(&input_args); + // Apply the autoharness defaults before validating, so that validation sees the options the + // run will actually use (e.g. `--jobs=N` must not be rejected for lacking + // `--output-format=terse` when autoharness supplies exactly that default). + if let Some(CargoKaniSubcommand::Autoharness(autoharness_args)) = &mut args.command { + autoharness_args.verify_opts.apply_autoharness_parallel_defaults(); + } check_is_valid(&args); // Handle version flag @@ -117,7 +123,11 @@ fn cargokani_main(input_args: Vec) -> Result<()> { /// The main function for the `kani` command. fn standalone_main() -> Result<()> { - let args = args::StandaloneArgs::parse(); + let mut args = args::StandaloneArgs::parse(); + // See the comment in `cargokani_main`. + if let Some(StandaloneSubcommand::Autoharness(autoharness_args)) = &mut args.command { + autoharness_args.verify_opts.apply_autoharness_parallel_defaults(); + } check_is_valid(&args); // Handle version flag diff --git a/tests/script-based-pre/autoderive_arbitrary_enums/enums.sh b/tests/script-based-pre/autoderive_arbitrary_enums/enums.sh index db4a99f8be09..16060e2fd373 100755 --- a/tests/script-based-pre/autoderive_arbitrary_enums/enums.sh +++ b/tests/script-based-pre/autoderive_arbitrary_enums/enums.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness +cargo kani autoharness -Z autoharness --output-format=regular diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/structs.sh b/tests/script-based-pre/autoderive_arbitrary_structs/structs.sh index db4a99f8be09..16060e2fd373 100755 --- a/tests/script-based-pre/autoderive_arbitrary_structs/structs.sh +++ b/tests/script-based-pre/autoderive_arbitrary_structs/structs.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness +cargo kani autoharness -Z autoharness --output-format=regular diff --git a/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh b/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh index 581b26d5f7df..cb81911f0171 100755 --- a/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh +++ b/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh @@ -15,4 +15,4 @@ echo "[with --bounded-arguments]" # `String`, which is expensive; on slower CI runners it can exceed the autoharness default # 60s harness timeout, so raise it here to keep these harnesses from spuriously timing out. # This run reports failures (`vec_first`/`string_first_byte`), so it exits non-zero (see config.yml). -cargo kani autoharness -Z autoharness -Z unstable-options --bounded-arguments --harness-timeout 5m +cargo kani autoharness -Z autoharness -Z unstable-options --output-format=regular --bounded-arguments --harness-timeout 5m diff --git a/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh b/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh index bf93a6c7f6d2..16060e2fd373 100755 --- a/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh +++ b/tests/script-based-pre/cargo_autoharness_dependencies/dependencies.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness --output-format=regular \ No newline at end of file +cargo kani autoharness -Z autoharness --output-format=regular diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh index bf93a6c7f6d2..16060e2fd373 100755 --- a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness --output-format=regular \ No newline at end of file +cargo kani autoharness -Z autoharness --output-format=regular diff --git a/tests/script-based-pre/cargo_autoharness_parallel/parallel.expected b/tests/script-based-pre/cargo_autoharness_parallel/parallel.expected index 82c766c76965..4457b761b021 100644 --- a/tests/script-based-pre/cargo_autoharness_parallel/parallel.expected +++ b/tests/script-based-pre/cargo_autoharness_parallel/parallel.expected @@ -1,3 +1,4 @@ +TERSE: yes PARALLEL: yes | f1 | #[kani::proof] | Success | f2 | #[kani::proof] | Success diff --git a/tests/script-based-pre/cargo_autoharness_parallel/parallel.sh b/tests/script-based-pre/cargo_autoharness_parallel/parallel.sh index 7f49424112b0..eeead1b5c576 100755 --- a/tests/script-based-pre/cargo_autoharness_parallel/parallel.sh +++ b/tests/script-based-pre/cargo_autoharness_parallel/parallel.sh @@ -3,10 +3,27 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT # Autoharness defaults to parallel verification (-j) with terse output. Harness results -# arrive in nondeterministic order, so assert on order-independent evidence: the thread -# prefixes, the (sorted) per-function summary lines, and the totals line. -output=$(cargo kani autoharness -Z autoharness 2>&1) +# arrive in nondeterministic order, so assert on order-independent evidence: the absence of +# per-check detail, the thread prefixes, the (sorted) per-function summary lines, and the +# totals line. +# +# RAYON_NUM_THREADS pins the pool size, so the thread prefixes below appear regardless of how +# much parallelism the machine (or its cgroup/CPU affinity) actually offers. This still checks +# the default: rayon only consults the environment variable when the thread count is left +# unset, which is exactly what the defaulted `--jobs` does -- sequential verification passes an +# explicit `num_threads(1)` that overrides it. +output=$(RAYON_NUM_THREADS=2 cargo kani autoharness -Z autoharness 2>&1) +# Terse output omits the per-check detail that `--output-format=regular` prints. +if echo "$output" | grep -qE '^Check [0-9]+:'; then + echo "TERSE: no" + echo "$output" +else + echo "TERSE: yes" +fi + +# Harness results are prefixed with the thread that produced them when the pool has more than +# one thread. if echo "$output" | grep -q "Thread [0-9]*:"; then echo "PARALLEL: yes" else diff --git a/tests/script-based-pre/cargo_autoharness_slices/slices.sh b/tests/script-based-pre/cargo_autoharness_slices/slices.sh index c82faf7be78f..7782ab7ec1ec 100755 --- a/tests/script-based-pre/cargo_autoharness_slices/slices.sh +++ b/tests/script-based-pre/cargo_autoharness_slices/slices.sh @@ -15,4 +15,4 @@ echo "[with --bounded-arguments]" # reason about; on slower CI runners it can exceed the autoharness default 60s harness timeout, # so raise it here to keep this (genuinely passing) harness from spuriously timing out. # This run reports failures (`first`/`first_byte`), so it exits non-zero (see config.yml). -cargo kani autoharness -Z autoharness -Z unstable-options --bounded-arguments --harness-timeout 5m +cargo kani autoharness -Z autoharness -Z unstable-options --output-format=regular --bounded-arguments --harness-timeout 5m diff --git a/tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.sh b/tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.sh index db4a99f8be09..16060e2fd373 100755 --- a/tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.sh +++ b/tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness +cargo kani autoharness -Z autoharness --output-format=regular