Fail a zero-match harness filter before codegen and export

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)),
             };
         }
 

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!([]));
         }

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,23 +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::<Vec<String>>()
-                .join("`, `");
+            let harnesses_missing: Vec<String> =
+                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, before codegen and export.
+        if !harness_filters.is_empty() && compiler_filtered_harnesses.is_empty() {
+            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)

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.

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.

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

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);
+}

tests/script-based-pre/harness_filter_no_match/no_match.expected

@@ -0,0 +1 @@
+SUCCESS: zero-match filters fail before exit and before export

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 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.
+
+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 "Failed to match the following harness(es):" <<< "${OUT}"; then
+    echo "FAIL: expected the zero-match 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 '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"

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.