Show only relevant benchmarks in CI summary

.github/workflows/bench.yml

@@ -10,7 +10,7 @@ name: Kani Performance Benchmarks
 on:
   push:
     branches:
-      - 'main'
+      - '*'
   workflow_call:
 
 jobs:

tools/benchcomp/benchcomp/visualizers/__init__.py

@@ -155,7 +155,9 @@ class dump_markdown_results_table:
     returns a string that is rendered in the benchmark's row in the new column.
     This allows you to emit arbitrary text or markdown formatting in response to
     particular combinations of values for different variants, such as
-    regressions or performance improvements.
+    regressions or performance improvements. If `delete_row_if_empty` is set to
+    `true` on the extra column, then benchmarks for which the extra row text
+    evaluates to an empty string will not be displayed in the table at all.
 
     'scatterplot' takes the values 'off' (default), 'linear' (linearly scaled
     axes), or 'log' (logarithmically scaled axes).
@@ -176,13 +178,16 @@ class dump_markdown_results_table:
             else "**" + str(b["variant_2"]/b["variant_1"]) + "**"
         success:
         - column_name: change
+          delete_row_if_empty: true
           text: >
             lambda b: "" if b["variant_2"] == b["variant_1"]
             else "newly passing" if b["variant_2"]
             else "regressed"
     ```
 
-    Example output:
+    Example output. Note that `bench_1` does not appear in the second table
+    because it neither regressed or is newly passing, so the text in the extra
+    column is empty, and `delete_row_if_empty` is set to `true`.
 
     ```
     ## runtime
@@ -196,7 +201,6 @@ class dump_markdown_results_table:
 
     | Benchmark |  variant_1 | variant_2 | change |
     | --- | --- | --- | --- |
-    | bench_1 | True | True |  |
     | bench_2 | True | False | regressed |
     | bench_3 | False | True | newly passing |
     ```
@@ -355,10 +359,18 @@ def _add_extra_columns(self, metrics):
                 columns = self.extra_columns[metric]
             except KeyError:
                 continue
+            to_delete = set()
             for bench, variants in benches.items():
                 tmp_variants = dict(variants)
                 for column in columns:
                     variants[column["column_name"]] = column["text"](tmp_variants)
+                    if all((
+                            column.get("delete_row_if_empty"),
+                            not variants[column["column_name"]])):
+                        to_delete.add(bench)
+                        break
+            for bench in to_delete:
+                benches.pop(bench)
 
 
     @staticmethod

tools/benchcomp/configs/perf-regression.yaml

@@ -40,6 +40,7 @@ visualize:
       # embolden if the absolute difference is more than 10% of the old value
       number_vccs:
       - column_name: diff old → new
+        delete_row_if_empty: true
         text: >
           lambda b: "" if b["kani_new"] == b["kani_old"]
           else ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.1 else "")
@@ -48,6 +49,7 @@ visualize:
           + ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.1 else "")
       number_program_steps:
       - column_name: diff old → new
+        delete_row_if_empty: true
         text: >
           lambda b: "" if b["kani_new"] == b["kani_old"]
           else ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.1 else "")
@@ -59,24 +61,27 @@ visualize:
       # cells whose absolute change is >50%
       solver_runtime:
       - column_name: "% change old → new"
+        delete_row_if_empty: true
         text: >
-          lambda b: "" if b["kani_new"] == b["kani_old"]
+          lambda b: "" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) < 0.1
           else ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.5 else "")
           + ("+" if b["kani_new"] > b["kani_old"] else "")
           + "%.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 "")
       verification_time:
       - column_name: "% change old → new"
+        delete_row_if_empty: true
         text: >
-          lambda b: "" if b["kani_new"] == b["kani_old"]
+          lambda b: "" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) < 0.1
           else ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.5 else "")
           + ("+" if b["kani_new"] > b["kani_old"] else "")
           + "%.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 "")
       symex_runtime:
       - column_name: "% change old → new"
+        delete_row_if_empty: true
         text: >
-          lambda b: "" if b["kani_new"] == b["kani_old"]
+          lambda b: "" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) < 0.1
           else ("**" if abs((b["kani_new"]-b["kani_old"])/b["kani_old"]) > 0.5 else "")
           + ("+" if b["kani_new"] > b["kani_old"] else "")
           + "%.3f%%" % ((b["kani_new"] - b["kani_old"]) * 100 / b["kani_old"])
@@ -85,6 +90,7 @@ visualize:
       # For success metric, display some text if success has changed
       success:
       - column_name: change
+        delete_row_if_empty: true
         text: >
           lambda b: "" if b["kani_new"] == b["kani_old"]
           else "❌ newly failing" if b["kani_old"]