Fix --export-json reporting a failed, skipped, or zero-match run as clean

kani-driver/src/call_cbmc.rs

@@ -37,10 +37,14 @@ pub struct CbmcInfo {
 #[derive(Debug, Clone, Default)]
 pub struct CbmcStats {
     pub runtime_symex_s: Option<f64>,
-    pub size_program_expression: Option<u32>,
-    pub slicing_removed_assignments: Option<u32>,
-    pub vccs_generated: Option<u32>,
-    pub vccs_remaining: Option<u32>,
+    // `u64`, not `u32`: these are unbounded counts scraped from CBMC's own text output (program
+    // expression size, VCCs, sliced assignments), and a sufficiently large real run overflowing
+    // `u32` used to collapse silently to `null` via `parse::<u32>().ok()` -- indistinguishable
+    // from "not measured".
+    pub size_program_expression: Option<u64>,
+    pub slicing_removed_assignments: Option<u64>,
+    pub vccs_generated: Option<u64>,
+    pub vccs_remaining: Option<u64>,
     pub runtime_postprocess_equation_s: Option<f64>,
     pub runtime_convert_ssa_s: Option<f64>,
     pub runtime_post_process_s: Option<f64>,
@@ -107,16 +111,22 @@ fn merge_cbmc_stats(items: &[ParserItem]) -> Option<CbmcStats> {
 /// Record the statistic a single CBMC status message carries, if it carries one. Later messages win,
 /// matching CBMC's own behaviour of reporting a running figure more than once.
 /// Returns whether this message was recognized.
+///
+/// Every field assignment below goes through [`record_stat`], which only overwrites a field when
+/// parsing succeeds. Without that, a later message that merely *resembles* a recognized label but
+/// fails to parse (a wording tweak, an unexpected unit, a truncated line) would silently erase an
+/// already-recorded valid measurement by assigning it `None` -- indistinguishable from "never
+/// measured" to a consumer of the export.
 fn record_cbmc_stat(message: &str, stats: &mut CbmcStats) -> bool {
     // "Generated 1 VCC(s), 1 remaining after simplification"
     if let Some(counts) = message
         .strip_prefix("Generated ")
         .and_then(|rest| rest.strip_suffix(" remaining after simplification"))
         && let Some((generated, remaining)) = counts.split_once(" VCC(s), ")
     {
-        stats.vccs_generated = generated.parse().ok();
-        stats.vccs_remaining = remaining.parse().ok();
-        return stats.vccs_generated.is_some() || stats.vccs_remaining.is_some();
+        let generated_ok = record_stat(&mut stats.vccs_generated, parse_leading_number(generated));
+        let remaining_ok = record_stat(&mut stats.vccs_remaining, parse_leading_number(remaining));
+        return generated_ok || remaining_ok;
     }
 
     // "slicing removed 81 assignments", or "simple slicing removed 5 assignments" when only the
@@ -126,8 +136,7 @@ fn record_cbmc_stat(message: &str, stats: &mut CbmcStats) -> bool {
             .strip_prefix("slicing removed ")
             .or_else(|| rest.strip_prefix("simple slicing removed "))
     {
-        stats.slicing_removed_assignments = count.parse().ok();
-        return stats.slicing_removed_assignments.is_some();
+        return record_stat(&mut stats.slicing_removed_assignments, parse_leading_number(count));
     }
 
     // Everything else is reported as "<label>: <value>".
@@ -137,9 +146,7 @@ fn record_cbmc_stat(message: &str, stats: &mut CbmcStats) -> bool {
     match label {
         // "150 steps"
         "size of program expression" => {
-            stats.size_program_expression =
-                value.strip_suffix(" steps").and_then(|steps| steps.parse().ok());
-            stats.size_program_expression.is_some()
+            record_stat(&mut stats.size_program_expression, parse_leading_number(value))
         }
         "Runtime Symex" => record_seconds(value, &mut stats.runtime_symex_s),
         "Runtime Postprocess Equation" => {
@@ -155,10 +162,60 @@ fn record_cbmc_stat(message: &str, stats: &mut CbmcStats) -> bool {
     }
 }
 
+/// Assign a freshly parsed value to `field` only when parsing succeeded. Never clobbers a
+/// previously recorded valid value with `None` -- a `parse` failure simply leaves whatever `field`
+/// already held. Returns whether this update recognized a value.
+fn record_stat<T>(field: &mut Option<T>, parsed: Option<T>) -> bool {
+    match parsed {
+        Some(value) => {
+            *field = Some(value);
+            true
+        }
+        None => false,
+    }
+}
+
+/// Parse the leading numeric token of `s` (optionally signed, with an optional decimal point and
+/// exponent), together with whatever non-numeric text remains afterwards, trimmed. A caller that
+/// does not care about the trailing text (a count, where the label alone already disambiguates
+/// the unit) can use [`parse_leading_number`]; a caller for which the unit is meaningful -- see
+/// [`record_seconds`] -- can inspect the remainder before trusting the value.
+fn parse_leading_number_with_remainder<T: std::str::FromStr>(s: &str) -> Option<(T, &str)> {
+    let s = s.trim();
+    let end = s
+        .find(|c: char| !(c.is_ascii_digit() || matches!(c, '.' | '-' | '+' | 'e' | 'E')))
+        .unwrap_or(s.len());
+    if end == 0 {
+        return None;
+    }
+    let value = s[..end].parse().ok()?;
+    Some((value, s[end..].trim()))
+}
+
+/// Parse the leading numeric token of `s`, ignoring anything that follows -- a trailing unit like
+/// `" steps"`, or any other suffix. This is more robust than matching an exact suffix: a harmless
+/// CBMC wording change to the text *after* the number (a new unit, a pluralization change, extra
+/// trailing detail) still lets the number itself be recovered, rather than silently collapsing
+/// the whole measurement to `null`. Only use this where the unit doesn't affect the *meaning* of
+/// the number -- for durations, see [`record_seconds`], which does check the unit.
+fn parse_leading_number<T: std::str::FromStr>(s: &str) -> Option<T> {
+    parse_leading_number_with_remainder(s).map(|(value, _)| value)
+}
+
 /// Record a duration CBMC reports as "0.00408627s" or "1.5416e-05s".
+///
+/// Unlike the count fields (see [`parse_leading_number`]), the unit here is meaningful: a value
+/// CBMC reported in another unit -- "5ms", say -- would have its leading number "5" extracted
+/// just as readily as "5s", but recording it as 5 *seconds* would silently misreport it by three
+/// orders of magnitude. So the value is only accepted when the text remaining after the leading
+/// number is exactly "s"; any other unit, or any other trailing text, is treated as a parse
+/// failure -- never as a number recorded in the wrong scale. See [`record_stat`] for why a parse
+/// failure never clobbers a previously recorded valid value.
 fn record_seconds(value: &str, field: &mut Option<f64>) -> bool {
-    *field = value.strip_suffix('s').and_then(|seconds| seconds.parse().ok());
-    field.is_some()
+    let parsed = parse_leading_number_with_remainder::<f64>(value)
+        .filter(|(_, remainder)| *remainder == "s")
+        .map(|(seconds, _)| seconds);
+    record_stat(field, parsed)
 }
 
 /// We will use Cadical by default since it performed better than MiniSAT in our analysis.
@@ -787,6 +844,56 @@ mod tests {
         assert!(merge_cbmc_stats(&warning).is_none());
     }
 
+    /// A later message that fails to parse must never erase an already-recorded valid value: the
+    /// gap between "not measured" and "we saw a value we couldn't parse" must stay visible as
+    /// "we kept the value we did successfully parse", not collapse to `null`.
+    #[test]
+    fn check_cbmc_stats_never_clobbers_valid_value() {
+        let mut stats = CbmcStats::default();
+        assert!(record_cbmc_stat("Runtime Solver: 4.1167e-05s", &mut stats));
+        assert_eq!(stats.runtime_solver_s, Some(4.1167e-05));
+
+        // A later malformed duplicate of the same label must not erase the value already
+        // recorded above.
+        assert!(!record_cbmc_stat("Runtime Solver: not-a-number", &mut stats));
+        assert_eq!(stats.runtime_solver_s, Some(4.1167e-05));
+    }
+
+    /// Parsing the leading numeric token (rather than requiring an exact suffix match) tolerates
+    /// harmless trailing text a suffix-based parser would reject outright.
+    #[test]
+    fn check_cbmc_stats_leading_number_tolerates_trailing_text() {
+        let mut stats = CbmcStats::default();
+        assert!(record_cbmc_stat(
+            "size of program expression: 21 steps (post-slicing)",
+            &mut stats
+        ));
+        assert_eq!(stats.size_program_expression, Some(21));
+    }
+
+    /// `record_seconds` must not mistake a value reported in another unit for seconds: the
+    /// leading number "5" is just as extractable from "5ms" as from "5s", but recording it as 5
+    /// seconds would misreport it by three orders of magnitude. Only an exact "s" suffix is
+    /// accepted; genuine second values, including exponent notation, still parse.
+    #[test]
+    fn check_record_seconds_is_unit_safe() {
+        let mut none = None;
+        assert!(!record_seconds("5ms", &mut none));
+        assert_eq!(none, None);
+
+        let mut none = None;
+        assert!(!record_seconds("5", &mut none));
+        assert_eq!(none, None);
+
+        let mut seconds = None;
+        assert!(record_seconds("0.004s", &mut seconds));
+        assert_eq!(seconds, Some(0.004));
+
+        let mut seconds = None;
+        assert!(record_seconds("1.5e-05s", &mut seconds));
+        assert_eq!(seconds, Some(1.5e-05));
+    }
+
     /// No statistics at all (CBMC died early, or verbosity hid them) must not fabricate a record.
     #[test]
     fn check_cbmc_stats_absent() {

kani-driver/src/frontend/schema_utils.rs

@@ -177,8 +177,9 @@ impl PropertyCounts {
         })
     }
 
-    /// The same shape, for a harness whose properties were never measured.
-    fn unmeasured_json() -> Value {
+    /// The same shape, for a harness whose properties were never measured, with a caller-supplied
+    /// explanation of why (e.g. a CBMC failure vs. never having run at all).
+    fn unmeasured_json_with_reason(reason: &str) -> Value {
         json!({
             "total_properties": null,
             "passed": null,
@@ -190,9 +191,16 @@ impl PropertyCounts {
             "unsatisfiable": null,
             "covered": null,
             "uncovered": null,
-            "error": "Could not extract property details due to verification failure"
+            "error": reason
         })
     }
+
+    /// The same shape, for a harness whose properties were never measured.
+    fn unmeasured_json() -> Value {
+        Self::unmeasured_json_with_reason(
+            "Could not extract property details due to verification failure",
+        )
+    }
 }
 
 /// Creates structured JSON metadata for the project
@@ -326,7 +334,12 @@ pub fn process_harness_results(
 ) -> Result<()> {
     // The main verification results are handled by the harness runner
     for h in harnesses {
-        let harness_result = results.iter().find(|r| r.harness.pretty_name == h.pretty_name);
+        // Joined on `mangled_name`, the unique identifier `harness_metadata` already carries,
+        // rather than `pretty_name`: two harnesses in different crates of the same workspace can
+        // share a `pretty_name`, and joining on that would attribute a result -- including a
+        // failure -- to the wrong harness. `harness_id` in the emitted JSON is unchanged; only
+        // the join predicate used to find the matching result moves to the unique key.
+        let harness_result = results.iter().find(|r| r.harness.mangled_name == h.mangled_name);
 
         // Add error details for this harness. This accumulates one entry per harness, keyed by
         // `harness_id`, the same way the `cbmc` array does: a single top-level object would let a
@@ -377,6 +390,40 @@ pub fn process_harness_results(
                     }
                 }),
             );
+        } else {
+            // This harness was selected (it has a `harness_metadata` entry) but has no entry in
+            // `results`. That is not always "never ran": under `--fail-fast`,
+            // `check_all_harnesses` collects harness futures into a single `Result<Vec<_>>`, and
+            // as soon as one harness fails, the whole collection short-circuits on that `Err` --
+            // discarding the `Ok` results of any other harness that had already completed
+            // (including a pass) but lost the race to be collected before the failure. So a
+            // harness landing in this branch may have genuinely been skipped, or may have run
+            // and even passed, with its result simply not retained. Without this branch the
+            // harness would be silently absent from both `error_details` and `property_details`,
+            // which a consumer correlating those arrays against `harness_metadata` (or checking
+            // "every detail entry is a Success") could easily misread as "nothing wrong with it".
+            // "skipped"/"not_run" would overclaim the former case for certain, so this reports
+            // the honest, disjunctive truth instead.
+            handler.add_harness_detail(
+                "error_details",
+                json!({
+                    "harness_id": h.pretty_name,
+                    "has_errors": true,
+                    "error_type": "not_reported",
+                    "exit_status": "unknown"
+                }),
+            );
+
+            handler.add_harness_detail(
+                "property_details",
+                json!({
+                    "harness_id": h.pretty_name,
+                    "property_details": PropertyCounts::unmeasured_json_with_reason(
+                        "No result was reported for this harness (e.g. skipped after \
+                         --fail-fast, or a completed result not retained)."
+                    )
+                }),
+            );
         }
     }
 
@@ -468,7 +515,10 @@ pub fn process_cbmc_results(
 ) -> Result<()> {
     let cbmc_info_opt = session.get_cbmc_info().ok();
     for h in harnesses {
-        let harness_result = results.iter().find(|r| r.harness.pretty_name == h.pretty_name);
+        // See the matching comment in `process_harness_results`: join on the unique
+        // `mangled_name` rather than `pretty_name`, which two harnesses in different crates of a
+        // workspace can share.
+        let harness_result = results.iter().find(|r| r.harness.mangled_name == h.mangled_name);
         handler.add_harness_detail("cbmc", json!({
             // basic name for harnesses
             "harness_id": h.pretty_name,

kani-driver/src/main.rs

@@ -147,6 +147,23 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
     // overhead for every other run, including a `cbmc --version` probe in `process_cbmc_results`.
     let mut handler =
         session.args.export_json.as_ref().map(|path| JsonHandler::new(Some(path.clone())));
+
+    // Invalidate any stale export at the target path immediately, before verification even
+    // starts. Without this, a run that dies before reaching the final `export()` below (a
+    // compile error, OOM, Ctrl-C, or a harness-level `Err` that propagates out of this function
+    // before that export runs) would leave a *previous* run's clean, complete-looking file at
+    // the target path -- and a consumer that trusts the file would read it as this run's
+    // result. Writing this marker first means the target can never be read as a stale clean pass
+    // again: it is either this incomplete marker, a genuinely complete export from this run, or
+    // absent. `write_sarif`/`print_final_summary` below run *after* the final `export()`, using
+    // the same `results` the export was built from, so a failure there leaves behind a complete
+    // export whose verification data is already accurate -- it is not a case this marker needs
+    // to guard against.
+    if let Some(handler) = handler.as_mut() {
+        handler.add_item("run_state", json!("incomplete"));
+        handler.export()?;
+    }
+
     let harnesses = session.determine_targets(project.get_all_harnesses())?;
     debug!(n = harnesses.len(), ?harnesses, "verify_project");
 
@@ -168,6 +185,41 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
         for h in &harnesses {
             handler.add_harness_detail("harness_metadata", create_harness_metadata_json(h));
         }
+
+        // Record what was requested and what was actually selected, so a filter typo that
+        // matches nothing is visible in the export itself rather than only in a log line the
+        // export's consumer never sees.
+        let requested_filters = &session.args.harnesses;
+        let unmatched_filters: Vec<&String> = if session.args.exact {
+            // `determine_targets` above already returns an error when an `--exact` filter
+            // matches nothing, so reaching this point means every exact filter matched.
+            vec![]
+        } else {
+            // Mirrors `find_proof_harnesses`'s non-exact matching closely enough to be a useful
+            // diagnostic (exact and unqualified-name matches are also substring matches of the
+            // full pretty name), without needing to re-run its full matching logic here.
+            requested_filters
+                .iter()
+                .filter(|filter| !harnesses.iter().any(|h| h.pretty_name.contains(filter.as_str())))
+                .collect()
+        };
+        handler.add_item(
+            "harness_selection",
+            json!({
+                "requested_filters": requested_filters,
+                "matched_count": harnesses.len(),
+                "unmatched_filters": unmatched_filters,
+            }),
+        );
+
+        if harnesses.is_empty() {
+            // A filter that matches zero harnesses must never export as a clean, completed run
+            // with `successful:0, failed:0` -- that is a vacuous pass, not evidence of anything.
+            // This overrides the "incomplete" marker written above; the final block below only
+            // promotes a run to "complete" when at least one harness was actually selected, so
+            // this state survives to the exported file.
+            handler.add_item("run_state", json!("no_harnesses_selected"));
+        }
     }
 
     // Verification
@@ -201,6 +253,17 @@ fn verify_project(project: Project, session: KaniSession) -> Result<()> {
 
     if let Some(handler) = handler.as_mut() {
         handler.add_item("coverage", json!({"enabled": session.args.coverage}));
+        // The terminal `run_state` must be authoritative about whether every selected harness
+        // actually ran: a zero-match run keeps the `no_harnesses_selected` state set above, and
+        // -- critically -- a non-empty selection is only "complete" when `results` accounts for
+        // every selected harness. Under `--fail-fast`, harnesses skipped after the first failure
+        // never produce a `HarnessResult`, so `results.len() < harnesses.len()`; reporting
+        // "complete" in that case would say a run that was intentionally aborted early finished
+        // normally. That case is reported as "partial" instead.
+        if !harnesses.is_empty() {
+            let run_state = if results.len() == harnesses.len() { "complete" } else { "partial" };
+            handler.add_item("run_state", json!(run_state));
+        }
         handler.export()?;
     }