From 8084232bc77676bcca5c256ee9c858bfd25815ac Mon Sep 17 00:00:00 2001 From: Ivo Matijasevic Date: Mon, 17 Aug 2026 22:53:47 +0200 Subject: [PATCH 1/2] Fail a zero-match harness filter before codegen and export A `--harness` filter that matches no harness only fails in the final summary. `--quiet` skips that summary, so the run exits 0. With `--export-json`, the run also writes a file that reports a clean, empty run. Bail out in `determine_targets` instead. This runs before codegen and before any export. The final-summary check stays as a last guard for paths that skip harness filtering. Add a script-based regression test covering the `--quiet` exit code, the absent export file, and the several-filters error message. Resolves the first driver bug from #4731. --- kani-driver/src/main.rs | 5 +- kani-driver/src/metadata.rs | 10 ++++ .../harness_filter_no_match/config.yml | 4 ++ .../harness_filter_no_match/fixture.rs | 10 ++++ .../harness_filter_no_match/no_match.expected | 1 + .../harness_filter_no_match/no_match.sh | 55 +++++++++++++++++++ 6 files changed, 82 insertions(+), 3 deletions(-) create mode 100644 tests/script-based-pre/harness_filter_no_match/config.yml create mode 100644 tests/script-based-pre/harness_filter_no_match/fixture.rs create mode 100644 tests/script-based-pre/harness_filter_no_match/no_match.expected create mode 100755 tests/script-based-pre/harness_filter_no_match/no_match.sh diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index e8a1ba11033d..7c28dbf7090b 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -174,9 +174,8 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> { handler.add_item("tools", create_tool_versions_json(&session, &harnesses)); // The per-harness arrays are filled in lazily below and by the harness runner, so declare - // them up front. A run with no matching harnesses would otherwise omit them entirely and - // write a document missing four of its documented keys -- and the "no harnesses matched" - // error is only reported after the export, so a consumer sees the malformed file first. + // them up front: a run that selects no harnesses (a crate with none) would otherwise + // write a document missing four of its documented keys. for key in ["harness_metadata", "error_details", "property_details", "cbmc"] { handler.add_item(key, json!([])); } diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index ef9472f4a9cf..e8b9cab91731 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -127,6 +127,16 @@ impl KaniSession { ); } + // A `--harness` filter that matches nothing must fail here + if !harness_filters.is_empty() && compiler_filtered_harnesses.is_empty() { + match self.args.harnesses.as_slice() { + [harness] => bail!("no harnesses matched the harness filter: `{harness}`"), + harnesses => { + bail!("no harnesses matched the harness filters: `{}`", harnesses.join("`, `")) + } + } + } + Ok(compiler_filtered_harnesses) } } diff --git a/tests/script-based-pre/harness_filter_no_match/config.yml b/tests/script-based-pre/harness_filter_no_match/config.yml new file mode 100644 index 000000000000..754a5f9f1214 --- /dev/null +++ b/tests/script-based-pre/harness_filter_no_match/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: no_match.sh +expected: no_match.expected diff --git a/tests/script-based-pre/harness_filter_no_match/fixture.rs b/tests/script-based-pre/harness_filter_no_match/fixture.rs new file mode 100644 index 000000000000..e01d74d43acc --- /dev/null +++ b/tests/script-based-pre/harness_filter_no_match/fixture.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// A crate with exactly one real proof harness. The test drives it with a +// `--harness` filter that matches nothing, so verification never runs. + +#[kani::proof] +fn existing_harness() { + assert!(1 + 1 == 2); +} diff --git a/tests/script-based-pre/harness_filter_no_match/no_match.expected b/tests/script-based-pre/harness_filter_no_match/no_match.expected new file mode 100644 index 000000000000..fc5dcf5ee8fe --- /dev/null +++ b/tests/script-based-pre/harness_filter_no_match/no_match.expected @@ -0,0 +1 @@ +SUCCESS: zero-match filters fail before exit and before export diff --git a/tests/script-based-pre/harness_filter_no_match/no_match.sh b/tests/script-based-pre/harness_filter_no_match/no_match.sh new file mode 100755 index 000000000000..08be37ae8bef --- /dev/null +++ b/tests/script-based-pre/harness_filter_no_match/no_match.sh @@ -0,0 +1,55 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Regression test for https://github.com/model-checking/kani/issues/4731: +# a `--harness` filter that matches no harness must fail (non-zero exit + an +# error) *before* codegen/export -- even under `--quiet`, which suppresses the +# end-of-run summary where the "no harnesses matched" error is otherwise raised. +# Previously such a run exited 0 and, with `--export-json`, wrote a document +# that serialized an empty run as a clean pass. + +set +e + +# 1. Under `--quiet`, a non-matching filter must still fail with an error. +OUT=$(kani fixture.rs --quiet --harness does_not_exist 2>&1) +CODE=$? +if [[ ${CODE} -eq 0 ]]; then + echo "FAIL: zero-match run under --quiet exited 0" + exit 1 +fi +if ! grep -q "no harnesses matched" <<< "${OUT}"; then + echo "FAIL: expected a 'no harnesses matched' error, got:" + echo "${OUT}" + exit 1 +fi + +# 2. With `--export-json`, a non-matching filter must fail and must not write a +# document (the run must fail before the export is written). +rm -f out.json +kani fixture.rs -Z unstable-options --harness does_not_exist --export-json out.json >/dev/null 2>&1 +CODE=$? +if [[ ${CODE} -eq 0 ]]; then + echo "FAIL: zero-match run with --export-json exited 0" + exit 1 +fi +if [[ -f out.json ]]; then + echo "FAIL: --export-json wrote a document for a zero-match run" + rm -f out.json + exit 1 +fi + +# 3. Several non-matching filters must all be named in the error. +OUT=$(kani fixture.rs --harness does_not_exist_a --harness does_not_exist_b 2>&1) +CODE=$? +if [[ ${CODE} -eq 0 ]]; then + echo "FAIL: zero-match run with two filters exited 0" + exit 1 +fi +if ! grep -q 'no harnesses matched the harness filters: `does_not_exist_a`, `does_not_exist_b`' <<< "${OUT}"; then + echo "FAIL: expected both filters in the error, got:" + echo "${OUT}" + exit 1 +fi + +echo "SUCCESS: zero-match filters fail before exit and before export" From ae183059e884998cabb65f2b4f2b6e0b0da57307 Mon Sep 17 00:00:00 2001 From: Ivo Matijasevic Date: Tue, 18 Aug 2026 19:54:29 +0200 Subject: [PATCH 2/2] Address review: one zero-match error for every filter site Extract the zero-match filter error into `no_harness_match_error` and use it from both `determine_targets` and the summary-stage guard, so the two sites cannot drift. The wording unifies with the `--exact` message. The summary-stage arm now carries its narrowed scope: `determine_targets` fails a zero-match filter before codegen, so the arm only guards paths that skip harness filtering. Tests that pinned the old wording are updated. --- kani-driver/src/harness_runner.rs | 11 +++---- kani-driver/src/metadata.rs | 33 +++++++++---------- .../simple-proof-annotation/main.expected | 4 ++- .../function-stubbing-no-harness/expected | 4 ++- .../harness_filter_no_match/no_match.sh | 8 ++--- .../no_matching_harness/expected | 4 ++- 6 files changed, 32 insertions(+), 32 deletions(-) diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index d904dd3d87c9..149138a64816 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use anyhow::{Error, Result, bail}; +use anyhow::{Error, Result}; use kani_metadata::{ArtifactType, HarnessKind, HarnessMetadata}; use rayon::prelude::*; use std::fs::File; @@ -344,12 +344,9 @@ impl KaniSession { "No proof harnesses (functions with #[kani::proof]) were found to verify." ) } - [harness] => { - bail!("no harnesses matched the harness filter: `{harness}`") - } - harnesses => { - bail!("no harnesses matched the harness filters: `{}`", harnesses.join("`, `")) - } + // `determine_targets` fails a zero-match filter before codegen, so this arm + // only guards paths that skip harness filtering. + _ => return Err(crate::metadata::no_harness_match_error(&self.args.harnesses)), }; } diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index e8b9cab91731..94b4a75a5b78 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use anyhow::{Result, bail}; +use anyhow::Result; use std::path::Path; use kani_metadata::{ @@ -114,33 +114,30 @@ impl KaniSession { compiler_filtered_harnesses.iter().map(|&h| &h.pretty_name).collect(); // Check which harnesses are missing from the difference of targets and all_harnesses - let harnesses_missing: Vec<&String> = - harness_filters.difference(&harness_found_names).cloned().collect(); - let joined_string = harnesses_missing - .iter() - .map(|&s| (*s).clone()) - .collect::>() - .join("`, `"); + let harnesses_missing: Vec = + harness_filters.difference(&harness_found_names).map(|&s| s.clone()).collect(); - bail!( - "Failed to match the following harness(es):\n{joined_string}\nPlease specify the fully-qualified name of a harness.", - ); + return Err(no_harness_match_error(&harnesses_missing)); } - // A `--harness` filter that matches nothing must fail here + // A `--harness` filter that matches nothing must fail here, before codegen and export. if !harness_filters.is_empty() && compiler_filtered_harnesses.is_empty() { - match self.args.harnesses.as_slice() { - [harness] => bail!("no harnesses matched the harness filter: `{harness}`"), - harnesses => { - bail!("no harnesses matched the harness filters: `{}`", harnesses.join("`, `")) - } - } + return Err(no_harness_match_error(&self.args.harnesses)); } Ok(compiler_filtered_harnesses) } } +/// The error for a harness filter that failed to match. Every zero-match site reports +/// through this one function, so the wordings cannot drift. +pub(crate) fn no_harness_match_error(missing: &[String]) -> anyhow::Error { + anyhow::anyhow!( + "Failed to match the following harness(es):\n{}\nPlease specify the fully-qualified name of a harness.", + missing.join("`, `") + ) +} + /// Sort harnesses such that for two harnesses in the same file, it is guaranteed that later /// appearing harnesses get processed earlier. /// This is necessary for the concrete playback feature (with in-place unit test modification) diff --git a/tests/cargo-kani/simple-proof-annotation/main.expected b/tests/cargo-kani/simple-proof-annotation/main.expected index 1a0db0160d5c..729c89fbfc05 100644 --- a/tests/cargo-kani/simple-proof-annotation/main.expected +++ b/tests/cargo-kani/simple-proof-annotation/main.expected @@ -1 +1,3 @@ -error: no harnesses matched the harness filter: `main` +error: Failed to match the following harness(es): +main +Please specify the fully-qualified name of a harness. diff --git a/tests/expected/function-stubbing-no-harness/expected b/tests/expected/function-stubbing-no-harness/expected index 47dea3fe757d..f8a7796e40d3 100644 --- a/tests/expected/function-stubbing-no-harness/expected +++ b/tests/expected/function-stubbing-no-harness/expected @@ -1 +1,3 @@ -error: no harnesses matched the harness filter: `foo` +error: Failed to match the following harness(es): +foo +Please specify the fully-qualified name of a harness. diff --git a/tests/script-based-pre/harness_filter_no_match/no_match.sh b/tests/script-based-pre/harness_filter_no_match/no_match.sh index 08be37ae8bef..cac63b1f8611 100755 --- a/tests/script-based-pre/harness_filter_no_match/no_match.sh +++ b/tests/script-based-pre/harness_filter_no_match/no_match.sh @@ -5,7 +5,7 @@ # Regression test for https://github.com/model-checking/kani/issues/4731: # a `--harness` filter that matches no harness must fail (non-zero exit + an # error) *before* codegen/export -- even under `--quiet`, which suppresses the -# end-of-run summary where the "no harnesses matched" error is otherwise raised. +# end-of-run summary where the zero-match error is otherwise raised. # Previously such a run exited 0 and, with `--export-json`, wrote a document # that serialized an empty run as a clean pass. @@ -18,8 +18,8 @@ if [[ ${CODE} -eq 0 ]]; then echo "FAIL: zero-match run under --quiet exited 0" exit 1 fi -if ! grep -q "no harnesses matched" <<< "${OUT}"; then - echo "FAIL: expected a 'no harnesses matched' error, got:" +if ! grep -q "Failed to match the following harness(es):" <<< "${OUT}"; then + echo "FAIL: expected the zero-match error, got:" echo "${OUT}" exit 1 fi @@ -46,7 +46,7 @@ if [[ ${CODE} -eq 0 ]]; then echo "FAIL: zero-match run with two filters exited 0" exit 1 fi -if ! grep -q 'no harnesses matched the harness filters: `does_not_exist_a`, `does_not_exist_b`' <<< "${OUT}"; then +if ! grep -q 'does_not_exist_a`, `does_not_exist_b' <<< "${OUT}"; then echo "FAIL: expected both filters in the error, got:" echo "${OUT}" exit 1 diff --git a/tests/ui/multiple-harnesses/no_matching_harness/expected b/tests/ui/multiple-harnesses/no_matching_harness/expected index d0eb27af10f8..c39e44f7c3f8 100644 --- a/tests/ui/multiple-harnesses/no_matching_harness/expected +++ b/tests/ui/multiple-harnesses/no_matching_harness/expected @@ -1 +1,3 @@ -error: no harnesses matched the harness filters: `non_existing`, `invalid` +error: Failed to match the following harness(es): +non_existing`, `invalid +Please specify the fully-qualified name of a harness.