From 3a5f83638171bdc39eeeed4ee7c7a79b9b0bf495 Mon Sep 17 00:00:00 2001 From: Martin Velay Date: Wed, 2 Sep 2026 08:56:54 +0200 Subject: [PATCH] fix: report the formal coverage columns the engine actually measured MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit get_coverage read formal_coverage["formal"], ["stimuli"] and ["checker"], which are the columns a JasperGold run reports. A VC Formal run reports stimuli, coi and proof, so reporting one raised KeyError: 'formal' and took dvsim down with a traceback after the build job had already passed and written its results. The columns are now taken from the report the tool's own parser wrote, and summary_header follows them, so the cross-cfg summary table names the columns the cfg's engine filled in rather than another engine's. Only stimuli is common to the two engines, so neither set can stand in for the other and there is nothing to harmonise onto. This was reachable only once an OpenTitan-side bug was fixed. The vcformal parse-formal-report.py rejects the --exp-fail-path that common_formal_cfg.hjson always passes, so make failed, no results.hjson was written, result.get("coverage") returned None, and get_coverage took its "No coverage information found" branch instead. tests/flow/ is new; nothing covered this module before. AI-assisted (Claude Code) — reviewed and approved by author Signed-off-by: Martin Velay --- src/dvsim/flow/formal.py | 90 +++++++++++---- tests/flow/__init__.py | 5 + tests/flow/test_formal.py | 223 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 296 insertions(+), 22 deletions(-) create mode 100644 tests/flow/__init__.py create mode 100644 tests/flow/test_formal.py diff --git a/src/dvsim/flow/formal.py b/src/dvsim/flow/formal.py index 71677596..2b624ed8 100644 --- a/src/dvsim/flow/formal.py +++ b/src/dvsim/flow/formal.py @@ -4,6 +4,7 @@ from collections.abc import Sequence from pathlib import Path +from typing import cast import hjson from tabulate import tabulate @@ -41,6 +42,10 @@ def __init__(self, flow_cfg_file, hjson_data, args, mk_config) -> None: # Default not to publish child cfg results. self.publish_report = hjson_data.get("publish_report", False) self.sub_flow = hjson_data["sub_flow"] + # The coverage columns this cfg's tool measured, filled in by get_coverage once a report + # has been read. Empty until then, and on a cfg whose flow collects no coverage at all, + # which is what makes summary_header below the fallback rather than the answer. + self.cov_header: list[str] = [] self.summary_header = ["name", "pass_rate", "formal_cov", "stimuli_cov", "checker_cov"] self.results_title = self.name.upper() + " Formal " + self.sub_flow.upper() + " Results" @@ -123,33 +128,70 @@ def get_coverage(self, result): results_str = "No coverage information found\n" summary = ["N/A", "N/A", "N/A"] else: - cov_header = ["formal", "stimuli", "checker"] + # The columns are whatever the tool's own report parser wrote, not a fixed set. + # A formal engine reports the coverage it measures under its own names: JasperGold + # gives formal, stimuli and checker, VC Formal gives stimuli, coi and proof, and only + # stimuli is common. Naming them here fixed one engine's vocabulary and raised + # KeyError: 'formal' on every VC Formal run with cov: true, after the job had already + # passed and written its results. + cov_header = list(formal_coverage) + if not cov_header: + # A parser that wrote the key and no columns measured nothing, which is the same + # thing to report as no key at all. Falling through instead would tabulate an + # empty table and contribute no cells to a row the summary expects three of. + return "No coverage information found\n", ["N/A", "N/A", "N/A"] + cov_colalign = ("center",) * len(cov_header) - cov_table = [cov_header] - cov_table.append( - [formal_coverage["formal"], formal_coverage["stimuli"], formal_coverage["checker"]], + cov_table = [cov_header, [formal_coverage[name] for name in cov_header]] + summary.extend(formal_coverage[name] for name in cov_header) + # The cross-cfg summary table is one row per cfg under one header, so the columns this + # cfg's tool measured have to reach the primary cfg that renders it. Setting + # self.summary_header would not: get_coverage runs on a child cfg and + # gen_results_summary reads the header off the primary, which no child touches. + self.cov_header = list(cov_header) + results_str = tabulate( + cov_table, + headers="firstrow", + tablefmt="pipe", + colalign=cov_colalign, ) - summary.append(formal_coverage["formal"]) - summary.append(formal_coverage["stimuli"]) - summary.append(formal_coverage["checker"]) + return results_str, summary - if len(cov_table) > 1: - results_str = tabulate( - cov_table, - headers="firstrow", - tablefmt="pipe", - colalign=cov_colalign, - ) + def formal_cfgs(self) -> "Sequence[FormalCfg]": + """Return this cfg's children as the formal cfgs they are. - else: - results_str = "No content in formal_coverage\n" - summary = ["N/A", "N/A", "N/A"] - return results_str, summary + `FlowCfg` types the list for every flow, so the formal-only attributes the two methods + below read off a child are invisible to a type checker without narrowing it here. + """ + return cast("Sequence[FormalCfg]", self.cfgs) + + def resolve_summary_header(self) -> list[str]: + """Return the summary header naming the coverage columns the cfgs actually measured. + + Each cfg's own tool decides what it measures and under what names, and get_coverage + records that on the cfg. One table cannot carry two vocabularies, so cfgs disagreeing is + reported rather than silently resolved in favour of whichever came first: a single `-t` + makes them agree today, and the error is what says so if that ever stops being true. + """ + cfgs = self.formal_cfgs() + measured = {tuple(cfg.cov_header) for cfg in cfgs if cfg.cov_header} + if not measured: + return self.summary_header + if len(measured) > 1: + log.error( + "The cfgs of %s measured different coverage columns, %s, so one summary header " + "cannot name them all. Reporting the columns of %s.", + self.name, + sorted(measured), + cfgs[0].name, + ) + columns = next(iter(measured)) if len(measured) == 1 else tuple(cfgs[0].cov_header) + return ["name", "pass_rate", *(f"{name}_cov" for name in columns)] def gen_results_summary(self): # Gathers the aggregated results from all sub configs - # The results_summary will only contain the passing rate and - # percentages of the stimuli, coi, and proven coverage + # The results_summary will only contain the passing rate and the coverage percentages the + # cfgs' own tool measured, under the names that tool's report parser wrote. results_str = "## " + self.results_title + " (Summary)\n\n" results_str += "### " + self.timestamp_long + "\n" if self.revision: @@ -157,13 +199,17 @@ def gen_results_summary(self): results_str += "### Branch: " + self.branch + "\n" results_str += "\n" + self.summary_header = self.resolve_summary_header() colalign = ("center",) * len(self.summary_header) table = [self.summary_header] - for cfg in self.cfgs: + # One cell per column beyond name, so a missing result stays aligned with a header whose + # width follows the tool rather than being three coverage columns wide by assumption. + missing = ["N/A"] * (len(self.summary_header) - 2) + for cfg in self.formal_cfgs(): try: table.append(cfg.result_summary[cfg.name]) except KeyError as e: - table.append([cfg.name, "ERROR", "N/A", "N/A", "N/A"]) + table.append([cfg.name, "ERROR", *missing]) log.exception("cfg: %s could not find generated results_summary: %s", cfg.name, e) if len(table) > 1: self.results_summary_md = results_str + tabulate( diff --git a/tests/flow/__init__.py b/tests/flow/__init__.py new file mode 100644 index 00000000..3cd84c9d --- /dev/null +++ b/tests/flow/__init__.py @@ -0,0 +1,5 @@ +# Copyright lowRISC contributors (OpenTitan project). +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 + +"""Tests for the flow configurations.""" diff --git a/tests/flow/test_formal.py b/tests/flow/test_formal.py new file mode 100644 index 00000000..12e7b1f8 --- /dev/null +++ b/tests/flow/test_formal.py @@ -0,0 +1,223 @@ +# Copyright lowRISC contributors (OpenTitan project). +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 + +"""Test reporting a formal run. + +The two methods under test are exercised on stand-ins rather than on a `FormalCfg`, because +building one needs a config tree, and between them they touch only the handful of attributes the +fakes below carry. The stand-ins borrow the real methods, so what runs is the shipped code. + +The distinction the fakes preserve is the one that matters here: `get_coverage` runs on a child +cfg and `gen_results_summary` on the primary that renders the cross-cfg table. A test that drives +only the child cannot see whether a column name reaches the table at all. +""" + +import logging +from collections.abc import Iterator + +import pytest +from hamcrest import assert_that, contains_string, equal_to, has_length, is_not + +from dvsim.flow.formal import FormalCfg + +__all__ = () + +# The proof-completeness columns each engine measures, under the names its own report parser +# writes. Only stimuli is common, so neither set can stand in for the other. +JASPERGOLD = {"formal": "79.44 %", "stimuli": "96.06 %", "checker": "78.75 %"} +VCFORMAL = {"stimuli": "12.00 %", "coi": "34.00 %", "proof": "56.00 %"} + +# What the VC Formal flow reports today: its fpv.tcl collects nothing, so the parser answers N/A +# under all three of its own column names. Kept distinct from VCFORMAL because all-N/A values +# coincide with the no-coverage fallback and cannot on their own show which branch ran. +VCFORMAL_COLLECTED_NOTHING = {"stimuli": "N/A", "coi": "N/A", "proof": "N/A"} + +FALLBACK_HEADER = ["name", "pass_rate", "formal_cov", "stimuli_cov", "checker_cov"] + + +class FakeChildCfg: + """A child cfg, carrying only what `get_coverage` reads and writes.""" + + get_coverage = FormalCfg.get_coverage + + def __init__(self, name: str = "hmac") -> None: + """Initialise a child cfg as `FormalCfg.__init__` leaves one.""" + self.name = name + self.cov_header: list[str] = [] + self.summary_header = list(FALLBACK_HEADER) + self.result_summary: dict[str, list[str]] = {} + + def report(self, result: dict[str, dict[str, str]]) -> list[str]: + """Read a run's result the way `_gen_results_for_cfg` does, and return the summary row.""" + _, summary = self.get_coverage(result) + self.result_summary[self.name] = [self.name, "89.36 %", *summary] + return summary + + +class FakePrimaryCfg: + """A primary cfg, carrying only what `gen_results_summary` reads.""" + + formal_cfgs = FormalCfg.formal_cfgs + gen_results_summary = FormalCfg.gen_results_summary + resolve_summary_header = FormalCfg.resolve_summary_header + + def __init__(self, cfgs: list[FakeChildCfg]) -> None: + """Initialise a primary cfg over already-reported children.""" + self.name = "top_earlgrey_fpv_ip" + self.cfgs = cfgs + self.summary_header = list(FALLBACK_HEADER) + self.results_title = "TOP_EARLGREY_FPV_IP Formal FPV Results" + self.timestamp_long = "timestamp" + self.revision = "" + self.branch = "master" + self.results_summary_md = "" + + +@pytest.fixture +def dvsim_log(caplog: pytest.LogCaptureFixture) -> Iterator[pytest.LogCaptureFixture]: + """Capture dvsim's own logger, which deliberately does not propagate.""" + logger = logging.getLogger("dvsim") + logger.addHandler(caplog.handler) + caplog.set_level(logging.ERROR, logger="dvsim") + yield caplog + logger.removeHandler(caplog.handler) + + +def reported(*results: dict[str, dict[str, str]]) -> FakePrimaryCfg: + """Return a primary cfg whose children have each reported one run.""" + children = [] + for index, result in enumerate(results): + child = FakeChildCfg(name=f"cfg{index}") + child.report(result) + children.append(child) + return FakePrimaryCfg(children) + + +class TestCoverageColumns: + """Test that a run's own coverage columns are what gets reported.""" + + @staticmethod + @pytest.mark.parametrize( + ("engine", "coverage"), + [("jaspergold", JASPERGOLD), ("vcformal", VCFORMAL)], + ) + def test_reports_the_columns_a_run_measured( + engine: str, + coverage: dict[str, str], + ) -> None: + """Naming the columns in dvsim fixed one engine's vocabulary and raised KeyError.""" + results_str, summary = FakeChildCfg().get_coverage({"coverage": coverage}) + + assert_that(summary, equal_to(list(coverage.values())), engine) + for column in coverage: + assert_that(results_str, contains_string(column), engine) + + @staticmethod + def test_records_the_columns_for_the_table_the_primary_cfg_renders() -> None: + """The child is where the columns are known and the primary is where they are needed.""" + child = FakeChildCfg() + + child.get_coverage({"coverage": VCFORMAL}) + + assert_that(child.cov_header, equal_to(["stimuli", "coi", "proof"])) + + @staticmethod + def test_says_so_when_a_run_measured_no_coverage() -> None: + """A formal flow that collects nothing leaves the key out entirely.""" + results_str, summary = FakeChildCfg().get_coverage({}) + + assert_that(results_str, contains_string("No coverage information found")) + assert_that(summary, equal_to(["N/A", "N/A", "N/A"])) + + @staticmethod + def test_says_so_when_a_run_reported_no_columns() -> None: + """An empty coverage key measured nothing, so it reports as nothing rather than as a row. + + Falling through would tabulate an empty table and contribute no cells at all to a summary + row, leaving it short of the header instead of saying the run collected nothing. + """ + child = FakeChildCfg() + + results_str, summary = child.get_coverage({"coverage": {}}) + + assert_that(results_str, contains_string("No coverage information found")) + assert_that(summary, equal_to(["N/A", "N/A", "N/A"])) + assert_that(child.cov_header, equal_to([])) + + +class TestSummaryTable: + """Test the cross-cfg summary table, which is where a column name is finally read.""" + + @staticmethod + @pytest.mark.parametrize( + ("engine", "coverage", "columns"), + [ + ("jaspergold", JASPERGOLD, ["formal_cov", "stimuli_cov", "checker_cov"]), + ("vcformal", VCFORMAL, ["stimuli_cov", "coi_cov", "proof_cov"]), + ( + "vcformal collecting nothing", + VCFORMAL_COLLECTED_NOTHING, + ["stimuli_cov", "coi_cov", "proof_cov"], + ), + ], + ) + def test_names_the_columns_the_cfgs_tool_measured( + engine: str, + coverage: dict[str, str], + columns: list[str], + ) -> None: + """Recording the header on the child alone left this table naming another engine's columns. + + `get_coverage` runs on the child and this table is rendered by the primary, so a header + set on the child never reached it and VC Formal's stimuli, coi and proof figures were + printed under JasperGold's formal, stimuli and checker headings. Both engines report three + columns, so nothing misaligned and nothing failed. + """ + primary = reported({"coverage": coverage}) + + table = primary.gen_results_summary() + + assert_that(primary.summary_header, equal_to(["name", "pass_rate", *columns]), engine) + for value in coverage.values(): + assert_that(table, contains_string(value), engine) + + @staticmethod + def test_keeps_the_fallback_header_when_no_cfg_measured_coverage() -> None: + """Nothing to follow, so the header stays as `__init__` set it.""" + primary = reported({}) + + primary.gen_results_summary() + + assert_that(primary.summary_header, equal_to(FALLBACK_HEADER)) + + @staticmethod + def test_reports_cfgs_that_measured_different_columns( + dvsim_log: pytest.LogCaptureFixture, + ) -> None: + """One table cannot carry two vocabularies, so a clash is said rather than resolved. + + A single `-t` makes every cfg in a run share an engine today. This is what says so if + that ever stops being true, instead of labelling one engine's figures with the other's + column names. + """ + primary = reported({"coverage": JASPERGOLD}, {"coverage": VCFORMAL}) + + primary.gen_results_summary() + + assert_that(dvsim_log.text, contains_string("different coverage columns")) + assert_that(primary.summary_header, has_length(len(FALLBACK_HEADER))) + + @staticmethod + def test_a_cfg_missing_its_results_stays_aligned_with_the_header( + dvsim_log: pytest.LogCaptureFixture, + ) -> None: + """The placeholder row follows the header's width rather than assuming three columns.""" + primary = reported({"coverage": VCFORMAL}) + primary.cfgs[0].result_summary.clear() + + table = primary.gen_results_summary() + + assert_that(dvsim_log.text, contains_string("could not find generated results_summary")) + assert_that(table, contains_string("ERROR")) + assert_that(table, is_not(contains_string("formal_cov")))