From 1390cdbb6767cb8cb16e644dd6a232a5ddc40fb6 Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Thu, 24 Sep 2026 00:14:26 +0000 Subject: [PATCH 1/4] benchcomp: judge solver time only when the formula changed MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `error_on_regression` failed a PR whenever a harness's summed solver time was 1.5x its `main`-side value, which fires on runs that changed nothing about the harness. Measuring seven `main` runs of the perf suite bears that out: across 910 (benchmark, run) pairs whose VCC *and* step counts were identical on both sides -- the same formula, by construction -- the old→new solver-time ratio had a median of 0.99x but a range of 0.41x to 2.41x, and `inet::checksum::tests::differential` alone ranged 38.8s to 116.0s on the `main` side. The 2.41x pair failed a run; #4801, #4804 and #4820 failed the same way without touching the harnesses involved. Two changes, both from #4822: `solver_runtime` sums over the several calls CBMC makes per harness, and that count is not stable across runs of the same code (#4821), so the sum is not a comparable quantity. Count the calls (`solver_calls`) and derive `solver_runtime_per_call`, which is what the two sides share; the call count also shows up in the results table, where a differing count explains a differing sum at a glance. The regression rule now compares per-call time *and* requires that the VCC or step count moved. When those counts match, both sides are solving the same problem and the difference cannot be attributed to the change. Expressing that needed a way for a check to see more than one metric, so `error_on_regression` gained an `all_metrics` option. Replaying the seven runs through the new rule: the one that failed now passes, the other six are unaffected, and a synthetic change that grows the formula and triples solver time is still caught. The deliberate blind spot is a change that makes the *same* formula slower, which the results table still shows. --- .../benchcomp/benchcomp/parsers/kani_perf.py | 19 +++++ .../benchcomp/visualizers/__init__.py | 15 ++++ .../benchcomp/benchcomp/visualizers/utils.py | 15 ++-- tools/benchcomp/configs/perf-regression.yaml | 35 +++++++++- tools/benchcomp/test/test_regression.py | 62 +++++++++++++++++ .../test/unit/test_kani_perf_parser.py | 69 +++++++++++++++++++ 6 files changed, 209 insertions(+), 6 deletions(-) create mode 100644 tools/benchcomp/test/unit/test_kani_perf_parser.py diff --git a/tools/benchcomp/benchcomp/parsers/kani_perf.py b/tools/benchcomp/benchcomp/parsers/kani_perf.py index 76a4fd90af30..11b5fa9ed818 100755 --- a/tools/benchcomp/benchcomp/parsers/kani_perf.py +++ b/tools/benchcomp/benchcomp/parsers/kani_perf.py @@ -30,6 +30,14 @@ def _get_metrics(): "pat": re.compile(r"Runtime Solver: (?P[-e\d\.]+)s"), "parse": float, }, + # CBMC solves a harness in several calls, and the number of calls is not stable across + # runs of the same code (https://github.com/model-checking/kani/issues/4821). Counting + # them makes that visible, and turns `solver_runtime` -- a sum over a varying number of + # calls -- into something comparable: see `solver_runtime_per_call` below. + "solver_calls": { + "pat": re.compile(r"Solving with (?P.+)"), + "parse": lambda _: 1, + }, "removed_program_steps": { "pat": re.compile(r"slicing removed (?P\d+) assignments"), "parse": int, @@ -64,6 +72,10 @@ def get_metrics(): # the number_program_steps metric metrics.pop("removed_program_steps", None) + # Derived in `main` from `solver_runtime` and `solver_calls` rather than parsed from a line, + # so it has no pattern to strip. + metrics["solver_runtime_per_call"] = {} + return metrics @@ -108,6 +120,13 @@ def main(root_dir): except KeyError: pass + try: + calls = bench_info["metrics"]["solver_calls"] + runtime = bench_info["metrics"]["solver_runtime"] + bench_info["metrics"]["solver_runtime_per_call"] = runtime / calls + except (KeyError, ZeroDivisionError): + pass + return { "metrics": get_metrics(), "benchmarks": benchmarks, diff --git a/tools/benchcomp/benchcomp/visualizers/__init__.py b/tools/benchcomp/benchcomp/visualizers/__init__.py index 5700e049b8b8..f4fa8b318d5c 100644 --- a/tools/benchcomp/benchcomp/visualizers/__init__.py +++ b/tools/benchcomp/benchcomp/visualizers/__init__.py @@ -79,6 +79,21 @@ class error_on_regression: test: "lambda old, new: False if not old else not new" ``` + A check may instead set `all_metrics: true`, in which case the test receives the two + variants' entire metric dicts rather than a single metric's values. `metric` is then only + used to label the warning that the check prints: + + ``` + visualize: + - type: error_on_regression + variant_pairs: + - [variant_1, variant_2] + checks: + - metric: runtime + all_metrics: true + test: "lambda old, new: new['runtime'] / old['runtime'] > 1.1 and old['steps'] != new['steps']" + ``` + This says to check whether any benchmark regressed when run under variant_2 compared to variant_1. A benchmark is considered to have regressed if the value of the 'runtime' metric under variant_2 is 10% higher than the value diff --git a/tools/benchcomp/benchcomp/visualizers/utils.py b/tools/benchcomp/benchcomp/visualizers/utils.py index bbd927034ef5..24bbf67923da 100644 --- a/tools/benchcomp/benchcomp/visualizers/utils.py +++ b/tools/benchcomp/benchcomp/visualizers/utils.py @@ -24,10 +24,14 @@ class SingleRegressionCheck: metric: str test: typing.Callable + all_metrics: bool - def __init__(self, metric, test_program): + def __init__(self, metric, test_program, all_metrics=False): self.metric = metric + # When set, the test receives the two variants' whole metric dicts instead of a single + # metric's values, so it can judge one metric in the light of the others. + self.all_metrics = all_metrics try: self.test = eval(test_program) except SyntaxError: @@ -79,10 +83,13 @@ def __call__(self, results): bench_name, self.metric, variant) continue - old = bench["variants"][old_variant]["metrics"][self.metric] - new = bench["variants"][new_variant]["metrics"][self.metric] + old_metrics = bench["variants"][old_variant]["metrics"] + new_metrics = bench["variants"][new_variant]["metrics"] + old = old_metrics[self.metric] + new = new_metrics[self.metric] - if has_regressed(old, new): + if has_regressed(old_metrics, new_metrics) if has_regressed.all_metrics \ + else has_regressed(old, new): logging.warning( "Benchmark '%s' regressed on metric '%s' (%s -> %s)", bench_name, self.metric, old, new) diff --git a/tools/benchcomp/configs/perf-regression.yaml b/tools/benchcomp/configs/perf-regression.yaml index d1e65b24ca2c..6a82867a87de 100644 --- a/tools/benchcomp/configs/perf-regression.yaml +++ b/tools/benchcomp/configs/perf-regression.yaml @@ -82,6 +82,13 @@ visualize: + "%.3f%%" % ((b["kani_new"] - b["kani_old"]) * 100 / b["kani_old"]) + ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.5 else "") + solver_calls: + - column_name: diff old → new + text: > + lambda b: "" if b["kani_new"] == b["kani_old"] + else ("+" if b["kani_new"] > b["kani_old"] else "") + + str(b["kani_new"] - b["kani_old"]) + # For success metric, display some text if success has changed success: - column_name: change @@ -97,7 +104,31 @@ visualize: # Compare the old and new variants of each benchmark. The # benchmark has regressed if the lambda returns true. test: "lambda old, new: False if not old else not new" - - metric: solver_runtime - test: "lambda old, new: False if new < 10 else new/old > 1.5" + + # Solver time is only attributable to a change when the change altered the formula, so + # require that the VCC or step count moved before calling a slowdown a regression. On + # identical counts the two sides are solving the same problem, and measurements of the + # perf suite's heavy harnesses spread far too wide to read anything into the difference: + # over seven `main` runs, 910 (benchmark, run) pairs with identical VCC *and* step counts + # had a median old→new ratio of 0.99x but a range of 0.41x to 2.41x, and + # `inet::checksum::tests::differential` alone ranged 38.8s to 116.0s on the `main` side. + # That is what tripped this check on #4801, #4804 and #4820, none of which touched the + # harnesses involved (https://github.com/model-checking/kani/issues/4822). + # + # `solver_runtime` also sums over a number of solver calls that is not stable across runs + # of the same code (https://github.com/model-checking/kani/issues/4821), so compare the + # per-call time, which is the quantity the two sides share. + - metric: solver_runtime_per_call + all_metrics: true + test: > + lambda old, new: False if ( + old["number_vccs"] == new["number_vccs"] + and old["number_program_steps"] == new["number_program_steps"] + ) else ( + new["solver_runtime"] >= 10 + and new["solver_runtime_per_call"] / old["solver_runtime_per_call"] > 1.5 + ) + + # Symex time is deterministic given the formula, so it keeps the simple rule. - metric: symex_runtime test: "lambda old, new: False if new < 10 else new/old > 1.5" diff --git a/tools/benchcomp/test/test_regression.py b/tools/benchcomp/test/test_regression.py index 00256aa891ab..3173b28c3659 100644 --- a/tools/benchcomp/test/test_regression.py +++ b/tools/benchcomp/test/test_regression.py @@ -228,6 +228,68 @@ def test_error_on_regression_two_benchmarks_one_failed(self): run_bc.proc.returncode, 1, msg=run_bc.stderr) + def test_error_on_regression_all_metrics(self): + """Ensure that a check with `all_metrics` judges one metric in the light of another: a + slowdown only counts when the `steps` metric moved too.""" + + def config(new_steps): + return { + "variants": { + "old": { + "config": { + "directory": str(self.tmp), + "command_line": + "mkdir bench_1 && " + "echo 10 > bench_1/runtime && " + "echo 100 > bench_1/steps" + }, + }, + "new": { + "config": { + "directory": str(self.tmp), + "command_line": + "mkdir bench_1 && " + "echo 30 > bench_1/runtime && " + f"echo {new_steps} > bench_1/steps" + } + } + }, + "run": { + "suites": { + "suite_1": { + "parser": {"module": "test_file_to_metric"}, + "variants": ["old", "new"] + } + } + }, + "visualize": [{ + "type": "error_on_regression", + "variant_pairs": [["old", "new"]], + "checks": [{ + "metric": "runtime", + "all_metrics": True, + "test": + "lambda old, new: old['steps'] != new['steps'] " + "and new['runtime'] / old['runtime'] > 1.5" + }] + }] + } + + # Three times slower, but on the same number of steps: not attributable, so no error. + with tempfile.TemporaryDirectory() as tmp: + self.tmp = tmp + run_bc = Benchcomp(config(new_steps=100)) + run_bc() + self.assertEqual(run_bc.proc.returncode, 0, msg=run_bc.stderr) + + # Three times slower on a different number of steps: a regression. + with tempfile.TemporaryDirectory() as tmp: + self.tmp = tmp + run_bc = Benchcomp(config(new_steps=500)) + run_bc() + self.assertEqual(run_bc.proc.returncode, 1, msg=run_bc.stderr) + + def test_error_on_regression_visualization_success_regressed(self): """Ensure that benchcomp terminates with exit of 1 when the "error_on_regression" visualization is configured and one of the benchmarks' success metric has regressed""" diff --git a/tools/benchcomp/test/unit/test_kani_perf_parser.py b/tools/benchcomp/test/unit/test_kani_perf_parser.py new file mode 100644 index 000000000000..babb10d15cdc --- /dev/null +++ b/tools/benchcomp/test/unit/test_kani_perf_parser.py @@ -0,0 +1,69 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + + +import pathlib +import tempfile +import textwrap +import unittest + +import benchcomp.parsers.kani_perf as kani_perf + + +class TestKaniPerfParser(unittest.TestCase): + def parse(self, expected_out): + """Run the parser over a single fake `expected.out` and return its benchmarks""" + + with tempfile.TemporaryDirectory() as tmp: + out_dir = pathlib.Path(tmp) / "build" / "tests" / "perf" / "demo" / "expected" + out_dir.mkdir(parents=True) + (out_dir / "expected.out").write_text(textwrap.dedent(expected_out)) + return kani_perf.main(pathlib.Path(tmp))["benchmarks"] + + def test_solver_calls_are_counted(self): + """CBMC solves a harness in several calls; count them and average the time over them. + + `solver_runtime` sums a number of calls that is not stable across runs of the same code + (https://github.com/model-checking/kani/issues/4821), so the per-call time is what two + runs can be compared on. + """ + + benchmarks = self.parse("""\ + Checking harness demo::check... + Solving with CaDiCaL 3.0.0 + Runtime Solver: 2.0s + Solving with CaDiCaL 3.0.0 + Runtime Solver: 4.0s + size of program expression: 100 steps + slicing removed 10 assignments + Generated 20 VCC(s), 7 remaining after simplification + Runtime Symex: 1.5s + Verification Time: 8.0s + VERIFICATION:- SUCCESSFUL + """) + + metrics = benchmarks["demo/demo::check"]["metrics"] + self.assertEqual(metrics["solver_calls"], 2) + self.assertEqual(metrics["solver_runtime"], 6.0) + self.assertEqual(metrics["solver_runtime_per_call"], 3.0) + # unchanged by this addition + self.assertEqual(metrics["number_program_steps"], 90) + self.assertEqual(metrics["number_vccs"], 7) + self.assertTrue(metrics["success"]) + + def test_harness_without_solver_output(self): + """A harness whose properties are all decided before solving has no solver metrics""" + + benchmarks = self.parse("""\ + Checking harness demo::check... + size of program expression: 10 steps + slicing removed 2 assignments + Generated 4 VCC(s), 0 remaining after simplification + Runtime Symex: 0.1s + Verification Time: 0.2s + VERIFICATION:- SUCCESSFUL + """) + + metrics = benchmarks["demo/demo::check"]["metrics"] + self.assertNotIn("solver_calls", metrics) + self.assertNotIn("solver_runtime_per_call", metrics) From 7f7ae6cb381f20c49ac3c3063a45f943a251175a Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Wed, 30 Sep 2026 04:30:48 +0000 Subject: [PATCH 2/4] benchcomp: keep a same-instance backstop and judge total solver time Address review on #4846: - Compare total solver time again, so extra solver calls count as a regression even at an unchanged per-call time. - Never exempt a harness: use 1.5x when the SAT instance changed and a 4x backstop when it did not (widest same-instance spread seen: 2.41x). - Pin the instance with the first solver call's variable and clause counts in addition to the VCC and step counts. - In all_metrics mode, do not require the label metric to exist. --- .../benchcomp/benchcomp/parsers/kani_perf.py | 26 ++++- .../benchcomp/visualizers/__init__.py | 6 +- .../benchcomp/benchcomp/visualizers/utils.py | 17 ++- tools/benchcomp/configs/perf-regression.yaml | 36 +++--- .../test/unit/test_kani_perf_parser.py | 8 ++ .../test/unit/test_perf_regression_config.py | 108 ++++++++++++++++++ 6 files changed, 172 insertions(+), 29 deletions(-) create mode 100644 tools/benchcomp/test/unit/test_perf_regression_config.py diff --git a/tools/benchcomp/benchcomp/parsers/kani_perf.py b/tools/benchcomp/benchcomp/parsers/kani_perf.py index 11b5fa9ed818..636c389a7ef2 100755 --- a/tools/benchcomp/benchcomp/parsers/kani_perf.py +++ b/tools/benchcomp/benchcomp/parsers/kani_perf.py @@ -38,6 +38,20 @@ def _get_metrics(): "pat": re.compile(r"Solving with (?P.+)"), "parse": lambda _: 1, }, + # The size of the SAT instance CBMC hands its built-in solver. Later calls in the same + # harness solve that instance incrementally, one clause and variable at a time, so only + # the first call is recorded: it pins the instance more tightly than the VCC and step + # counts do, without inheriting the instability of the call count. + "solver_variables": { + "pat": re.compile(r"(?P\d+) variables, \d+ clauses"), + "parse": int, + "first_only": True, + }, + "solver_clauses": { + "pat": re.compile(r"\d+ variables, (?P\d+) clauses"), + "parse": int, + "first_only": True, + }, "removed_program_steps": { "pat": re.compile(r"slicing removed (?P\d+) assignments"), "parse": int, @@ -65,8 +79,8 @@ def _get_metrics(): def get_metrics(): metrics = dict(_get_metrics()) for metric, info in metrics.items(): - for field in ("pat", "parse"): - info.pop(field) + for field in ("pat", "parse", "first_only"): + info.pop(field, None) # This is not a metric we return; it is used to find the correct value for # the number_program_steps metric @@ -102,13 +116,17 @@ def main(root_dir): continue parse = metric_info["parse"] + bench_metrics = benchmarks[bench_name]["metrics"] + if metric_info.get("first_only"): + bench_metrics.setdefault(metric, parse(m["value"])) + continue try: # CBMC prints out some metrics more than once, e.g. # "Solver" and "decision procedure". Add those # values together - benchmarks[bench_name]["metrics"][metric] += parse(m["value"]) + bench_metrics[metric] += parse(m["value"]) except (KeyError, TypeError): - benchmarks[bench_name]["metrics"][metric] = parse(m["value"]) + bench_metrics[metric] = parse(m["value"]) break for bench_name, bench_info in benchmarks.items(): diff --git a/tools/benchcomp/benchcomp/visualizers/__init__.py b/tools/benchcomp/benchcomp/visualizers/__init__.py index f4fa8b318d5c..8d03b77cb303 100644 --- a/tools/benchcomp/benchcomp/visualizers/__init__.py +++ b/tools/benchcomp/benchcomp/visualizers/__init__.py @@ -80,8 +80,10 @@ class error_on_regression: ``` A check may instead set `all_metrics: true`, in which case the test receives the two - variants' entire metric dicts rather than a single metric's values. `metric` is then only - used to label the warning that the check prints: + variants' entire metric dicts rather than a single metric's values. `metric` is still + required, but is then only used to label the warning that the check prints; a benchmark + that lacks it is still passed to the test, which must handle missing metrics itself (e.g. + with `dict.get`): ``` visualize: diff --git a/tools/benchcomp/benchcomp/visualizers/utils.py b/tools/benchcomp/benchcomp/visualizers/utils.py index 24bbf67923da..65dad05e7915 100644 --- a/tools/benchcomp/benchcomp/visualizers/utils.py +++ b/tools/benchcomp/benchcomp/visualizers/utils.py @@ -85,11 +85,18 @@ def __call__(self, results): old_metrics = bench["variants"][old_variant]["metrics"] new_metrics = bench["variants"][new_variant]["metrics"] - old = old_metrics[self.metric] - new = new_metrics[self.metric] - - if has_regressed(old_metrics, new_metrics) if has_regressed.all_metrics \ - else has_regressed(old, new): + if has_regressed.all_metrics: + # `metric` only labels the warning here, so a benchmark that lacks it is + # still judged: the test decides what the absence of a metric means. + old = old_metrics.get(self.metric) + new = new_metrics.get(self.metric) + regressed = has_regressed(old_metrics, new_metrics) + else: + old = old_metrics[self.metric] + new = new_metrics[self.metric] + regressed = has_regressed(old, new) + + if regressed: logging.warning( "Benchmark '%s' regressed on metric '%s' (%s -> %s)", bench_name, self.metric, old, new) diff --git a/tools/benchcomp/configs/perf-regression.yaml b/tools/benchcomp/configs/perf-regression.yaml index 6a82867a87de..10acc6b93999 100644 --- a/tools/benchcomp/configs/perf-regression.yaml +++ b/tools/benchcomp/configs/perf-regression.yaml @@ -105,29 +105,29 @@ visualize: # benchmark has regressed if the lambda returns true. test: "lambda old, new: False if not old else not new" - # Solver time is only attributable to a change when the change altered the formula, so - # require that the VCC or step count moved before calling a slowdown a regression. On - # identical counts the two sides are solving the same problem, and measurements of the - # perf suite's heavy harnesses spread far too wide to read anything into the difference: - # over seven `main` runs, 910 (benchmark, run) pairs with identical VCC *and* step counts - # had a median old→new ratio of 0.99x but a range of 0.41x to 2.41x, and + # Solver time on the perf suite's heavy harnesses is noisy even when nothing changed: over + # seven `main` runs, 910 (benchmark, run) pairs with identical VCC *and* step counts had a + # median old→new ratio of 0.99x but a range of 0.41x to 2.41x, and # `inet::checksum::tests::differential` alone ranged 38.8s to 116.0s on the `main` side. - # That is what tripped this check on #4801, #4804 and #4820, none of which touched the + # A flat 1.5x therefore tripped on #4801, #4804 and #4820, none of which touched the # harnesses involved (https://github.com/model-checking/kani/issues/4822). # - # `solver_runtime` also sums over a number of solver calls that is not stable across runs - # of the same code (https://github.com/model-checking/kani/issues/4821), so compare the - # per-call time, which is the quantity the two sides share. - - metric: solver_runtime_per_call + # So the threshold depends on whether the SAT instance moved. When the VCC and step counts + # and the size of the first solver call's instance all match, the two sides are very + # likely solving the same problem, and only a slowdown well past the observed noise (4x) + # counts: that still catches, e.g., a change to the solver options Kani passes. Otherwise + # the original 1.5x applies. Both compare the *total* solver time, so a change that adds + # solver calls is caught even if each call is as fast as before; `solver_calls` and + # `solver_runtime_per_call` are in the results table to explain a differing total. + - metric: solver_runtime all_metrics: true test: > - lambda old, new: False if ( - old["number_vccs"] == new["number_vccs"] - and old["number_program_steps"] == new["number_program_steps"] - ) else ( - new["solver_runtime"] >= 10 - and new["solver_runtime_per_call"] / old["solver_runtime_per_call"] > 1.5 - ) + lambda old, new: bool(old.get("solver_runtime")) + and new.get("solver_runtime", 0) >= 10 + and new["solver_runtime"] / old["solver_runtime"] > ( + 4 if all(old.get(k) == new.get(k) for k in ( + "number_vccs", "number_program_steps", "solver_variables", "solver_clauses")) + else 1.5) # Symex time is deterministic given the formula, so it keeps the simple rule. - metric: symex_runtime diff --git a/tools/benchcomp/test/unit/test_kani_perf_parser.py b/tools/benchcomp/test/unit/test_kani_perf_parser.py index babb10d15cdc..1ce44b0c687c 100644 --- a/tools/benchcomp/test/unit/test_kani_perf_parser.py +++ b/tools/benchcomp/test/unit/test_kani_perf_parser.py @@ -30,9 +30,13 @@ def test_solver_calls_are_counted(self): benchmarks = self.parse("""\ Checking harness demo::check... + Running propositional reduction Solving with CaDiCaL 3.0.0 + 20705 variables, 30763 clauses Runtime Solver: 2.0s + Running propositional reduction Solving with CaDiCaL 3.0.0 + 20706 variables, 30764 clauses Runtime Solver: 4.0s size of program expression: 100 steps slicing removed 10 assignments @@ -46,6 +50,9 @@ def test_solver_calls_are_counted(self): self.assertEqual(metrics["solver_calls"], 2) self.assertEqual(metrics["solver_runtime"], 6.0) self.assertEqual(metrics["solver_runtime_per_call"], 3.0) + # The instance size is the first call's: later calls extend it incrementally. + self.assertEqual(metrics["solver_variables"], 20705) + self.assertEqual(metrics["solver_clauses"], 30763) # unchanged by this addition self.assertEqual(metrics["number_program_steps"], 90) self.assertEqual(metrics["number_vccs"], 7) @@ -67,3 +74,4 @@ def test_harness_without_solver_output(self): metrics = benchmarks["demo/demo::check"]["metrics"] self.assertNotIn("solver_calls", metrics) self.assertNotIn("solver_runtime_per_call", metrics) + self.assertNotIn("solver_variables", metrics) diff --git a/tools/benchcomp/test/unit/test_perf_regression_config.py b/tools/benchcomp/test/unit/test_perf_regression_config.py new file mode 100644 index 000000000000..051dc907de45 --- /dev/null +++ b/tools/benchcomp/test/unit/test_perf_regression_config.py @@ -0,0 +1,108 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + + +import pathlib +import unittest + +import yaml + +import benchcomp.visualizers.utils as utils + + +CONFIG = pathlib.Path(__file__).parents[2] / "configs" / "perf-regression.yaml" + + +def solver_runtime_check(): + """The `solver_runtime` check exactly as CI runs it""" + + with open(CONFIG) as handle: + config = yaml.safe_load(handle) + for viz in config["visualize"]: + if viz["type"] != "error_on_regression": + continue + for check in viz["checks"]: + if check["metric"] == "solver_runtime": + return utils.SingleRegressionCheck( + check["metric"], check["test"], check.get("all_metrics", False)) + raise AssertionError("no solver_runtime check in perf-regression.yaml") + + +def metrics(solver_runtime, solver_calls=2, **overrides): + result = { + "number_vccs": 2399, + "number_program_steps": 58765, + "solver_variables": 20705, + "solver_clauses": 30763, + "solver_runtime": solver_runtime, + "solver_calls": solver_calls, + "solver_runtime_per_call": solver_runtime / solver_calls, + } + result.update(overrides) + return result + + +class TestSolverRuntimeCheck(unittest.TestCase): + def setUp(self): + self.regressed = solver_runtime_check() + + def test_same_instance_noise_is_tolerated(self): + """The widest same-instance spread seen on `main` (2.41x) must not fail a PR""" + + self.assertFalse(self.regressed(metrics(11.2), metrics(11.2 * 2.41))) + + def test_same_instance_large_slowdown_is_caught(self): + """Identical counts do not exempt a harness: e.g. a solver-option change""" + + self.assertTrue(self.regressed(metrics(12.0), metrics(12.0 * 4.5))) + + def test_more_calls_at_the_same_per_call_time_is_caught(self): + """The total is compared, so extra calls count even if each one is no slower""" + + self.assertTrue(self.regressed( + metrics(12.0, solver_calls=2), metrics(60.0, solver_calls=10))) + + def test_changed_instance_uses_the_strict_threshold(self): + for key, value in (("number_vccs", 2400), ("number_program_steps", 58766), + ("solver_variables", 20706), ("solver_clauses", 30764)): + with self.subTest(changed=key): + self.assertTrue(self.regressed( + metrics(12.0), metrics(12.0 * 1.6, **{key: value}))) + self.assertFalse(self.regressed( + metrics(12.0), metrics(12.0 * 1.4, **{key: value}))) + + def test_short_runs_are_ignored(self): + self.assertFalse(self.regressed( + metrics(1.0, number_vccs=1), metrics(9.0, number_vccs=2))) + + def test_harness_without_solver_output(self): + """All properties decided before solving: no solver metrics, no regression, no crash""" + + bare = {"number_vccs": 0, "number_program_steps": 10} + self.assertFalse(self.regressed(bare, bare)) + self.assertFalse(self.regressed(bare, metrics(30.0))) + + +class TestAllMetricsChecker(unittest.TestCase): + def test_missing_label_metric_is_not_a_key_error(self): + """With `all_metrics`, `metric` only labels the warning, so a benchmark that lacks it is + still judged rather than aborting the whole check""" + + results = {"benchmarks": { + "no_solver": {"variants": { + "old": {"metrics": {"number_vccs": 0}}, + "new": {"metrics": {"number_vccs": 0}}, + }}, + "slow": {"variants": { + "old": {"metrics": {"solver_runtime": 10.0}}, + "new": {"metrics": {"solver_runtime": 50.0}}, + }}, + }} + checker = utils.AnyBenchmarkRegressedChecker( + [["old", "new"]], "solver_runtime", + "lambda old, new: new.get('solver_runtime', 0) > 2 * old.get('solver_runtime', 0)", + all_metrics=True) + with self.assertLogs(level="WARNING") as logs: + self.assertTrue(checker(results)) + self.assertEqual(len(logs.output), 1) + self.assertIn("'slow'", logs.output[0]) From 89cb1e18c0ff7c1377e05c8796aac41ab8abbf4b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Sep 2026 10:54:17 +0000 Subject: [PATCH 3/4] benchcomp: flag a harness that newly needs the solver The solver-time rule returned False whenever the `main` side had no `Runtime Solver:` line, so a harness whose properties `main` decides without the solver, but which the change sends to the solver for 10s or more, passed. Treat a missing or zero old solver time as a regression once the new time reaches the 10s floor; there is no ratio to take in that case. A harness without solver output on both sides, or only on the new side, still passes. Co-authored-by: Kiro --- tools/benchcomp/configs/perf-regression.yaml | 12 ++++++------ .../test/unit/test_perf_regression_config.py | 11 ++++++++++- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/tools/benchcomp/configs/perf-regression.yaml b/tools/benchcomp/configs/perf-regression.yaml index 10acc6b93999..bba1627003bd 100644 --- a/tools/benchcomp/configs/perf-regression.yaml +++ b/tools/benchcomp/configs/perf-regression.yaml @@ -122,12 +122,12 @@ visualize: - metric: solver_runtime all_metrics: true test: > - lambda old, new: bool(old.get("solver_runtime")) - and new.get("solver_runtime", 0) >= 10 - and new["solver_runtime"] / old["solver_runtime"] > ( - 4 if all(old.get(k) == new.get(k) for k in ( - "number_vccs", "number_program_steps", "solver_variables", "solver_clauses")) - else 1.5) + lambda old, new: new.get("solver_runtime", 0) >= 10 and ( + not old.get("solver_runtime") + or new["solver_runtime"] / old["solver_runtime"] > ( + 4 if all(old.get(k) == new.get(k) for k in ( + "number_vccs", "number_program_steps", "solver_variables", "solver_clauses")) + else 1.5)) # Symex time is deterministic given the formula, so it keeps the simple rule. - metric: symex_runtime diff --git a/tools/benchcomp/test/unit/test_perf_regression_config.py b/tools/benchcomp/test/unit/test_perf_regression_config.py index 051dc907de45..68e1b3053abf 100644 --- a/tools/benchcomp/test/unit/test_perf_regression_config.py +++ b/tools/benchcomp/test/unit/test_perf_regression_config.py @@ -80,7 +80,16 @@ def test_harness_without_solver_output(self): bare = {"number_vccs": 0, "number_program_steps": 10} self.assertFalse(self.regressed(bare, bare)) - self.assertFalse(self.regressed(bare, metrics(30.0))) + self.assertFalse(self.regressed(metrics(30.0), bare)) + self.assertFalse(self.regressed(bare, metrics(9.0))) + + def test_newly_needing_the_solver_is_caught(self): + """A harness that `main` decides without the solver but the change sends to it for 10s + or more has regressed, although there is no old solver time to take a ratio of""" + + bare = {"number_vccs": 0, "number_program_steps": 10} + self.assertTrue(self.regressed(bare, metrics(30.0))) + self.assertTrue(self.regressed(metrics(0.0), metrics(30.0))) class TestAllMetricsChecker(unittest.TestCase): From 5cf8ed62f9d1f2622b896aa199de8fb72b510dec Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Sep 2026 10:55:06 +0000 Subject: [PATCH 4/4] benchcomp: say what the solver-time rule gives up Address review on #4846: - Equal VCC, step, variable and clause counts make the same instance likely, not certain; say so. - Note that CBMC prints the instance size only for its built-in solvers, so for kissat the rule compares VCC and step counts only. - State what the rule gives up (a same-size slowdown between 1.5x and 4x passes) and what would let the 4x come down (#4821, #4918). - The parser comment on `solver_calls` still said per-call time is what gets compared; it now only explains a differing total. Co-authored-by: Kiro --- .../benchcomp/benchcomp/parsers/kani_perf.py | 4 ++-- tools/benchcomp/configs/perf-regression.yaml | 22 ++++++++++++++----- 2 files changed, 18 insertions(+), 8 deletions(-) diff --git a/tools/benchcomp/benchcomp/parsers/kani_perf.py b/tools/benchcomp/benchcomp/parsers/kani_perf.py index 636c389a7ef2..4dcf00fe3c26 100755 --- a/tools/benchcomp/benchcomp/parsers/kani_perf.py +++ b/tools/benchcomp/benchcomp/parsers/kani_perf.py @@ -32,8 +32,8 @@ def _get_metrics(): }, # CBMC solves a harness in several calls, and the number of calls is not stable across # runs of the same code (https://github.com/model-checking/kani/issues/4821). Counting - # them makes that visible, and turns `solver_runtime` -- a sum over a varying number of - # calls -- into something comparable: see `solver_runtime_per_call` below. + # them, and deriving `solver_runtime_per_call` in `main`, explains a differing + # `solver_runtime`, which sums over all calls. "solver_calls": { "pat": re.compile(r"Solving with (?P.+)"), "parse": lambda _: 1, diff --git a/tools/benchcomp/configs/perf-regression.yaml b/tools/benchcomp/configs/perf-regression.yaml index bba1627003bd..b33d892cc5e6 100644 --- a/tools/benchcomp/configs/perf-regression.yaml +++ b/tools/benchcomp/configs/perf-regression.yaml @@ -113,12 +113,22 @@ visualize: # harnesses involved (https://github.com/model-checking/kani/issues/4822). # # So the threshold depends on whether the SAT instance moved. When the VCC and step counts - # and the size of the first solver call's instance all match, the two sides are very - # likely solving the same problem, and only a slowdown well past the observed noise (4x) - # counts: that still catches, e.g., a change to the solver options Kani passes. Otherwise - # the original 1.5x applies. Both compare the *total* solver time, so a change that adds - # solver calls is caught even if each call is as fast as before; `solver_calls` and - # `solver_runtime_per_call` are in the results table to explain a differing total. + # and the size of the first solver call's instance all match (CBMC prints that size only + # for its built-in solvers, so for an external solver such as kissat it is absent on both + # sides), the two sides are likely, not certainly, solving the same instance, and only a + # slowdown well past the observed noise (4x) counts: that still catches a large slowdown + # from, e.g., a change to the solver options Kani passes. Otherwise the original 1.5x + # applies. Both compare the *total* solver time, so a change that adds solver calls is + # caught even if each call is as fast as before; `solver_calls` and + # `solver_runtime_per_call` are in the results table to explain a differing total. A + # harness that newly needs 10s or more of solver time also counts. + # + # What this gives up: a slowdown between 1.5x and 4x on an instance of unchanged size + # passes. Much of the noise comes from symbol names that depend on rustc allocation + # order, which changes the variable order the solver sees + # (https://github.com/model-checking/kani/issues/4821). Fixing that, or re-running a + # tripped harness on both sides (https://github.com/model-checking/kani/issues/4918), + # would let the 4x come down. - metric: solver_runtime all_metrics: true test: >