benchcomp: scale the solver-time threshold to whether the SAT instance changed

tools/benchcomp/benchcomp/parsers/kani_perf.py

@@ -30,6 +30,28 @@ def _get_metrics():
             "pat": re.compile(r"Runtime Solver: (?P<value>[-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, 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<value>.+)"),
+            "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<value>\d+) variables, \d+ clauses"),
+            "parse": int,
+            "first_only": True,
+        },
+        "solver_clauses": {
+            "pat": re.compile(r"\d+ variables, (?P<value>\d+) clauses"),
+            "parse": int,
+            "first_only": True,
+        },
         "removed_program_steps": {
             "pat": re.compile(r"slicing removed (?P<value>\d+) assignments"),
             "parse": int,
@@ -57,13 +79,17 @@ 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
     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
 
 
@@ -90,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():
@@ -108,6 +138,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,

tools/benchcomp/benchcomp/visualizers/__init__.py

@@ -79,6 +79,23 @@ 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 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:
+    - 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

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,20 @@ 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]
-
-                if has_regressed(old, new):
+                old_metrics = bench["variants"][old_variant]["metrics"]
+                new_metrics = bench["variants"][new_variant]["metrics"]
+                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)

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,41 @@ 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"
+
+      # 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.
+      # 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).
+      #
+      # 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 (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
-        test: "lambda old, new: False if new < 10 else new/old > 1.5"
+        all_metrics: true
+        test: >
+          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
         test: "lambda old, new: False if new < 10 else new/old > 1.5"

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"""
 

tools/benchcomp/test/unit/test_kani_perf_parser.py

@@ -0,0 +1,77 @@
+# 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...
+            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
+            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)
+        # 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)
+        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)
+        self.assertNotIn("solver_variables", metrics)