Add #VCCs and #program steps benchcomp metrics (#2410)

This commit adds two new metrics to the benchcomp "kani perf" parser.
These metrics are recorded from each benchmark's output file but not
currently checked for regression.

Author: karkhaz

tools/benchcomp/benchcomp/parsers/kani_perf.py

@@ -25,6 +25,19 @@ def _get_metrics():
             "pat": re.compile(r"Runtime Solver: (?P<value>[-e\d\.]+)s"),
             "parse": float,
         },
+        "removed_program_steps": {
+            "pat": re.compile(r"slicing removed (?P<value>\d+) assignments"),
+            "parse": int,
+        },
+        "number_program_steps": {
+            "pat": re.compile(r"size of program expression: (?P<value>\d+) steps"),
+            "parse": int,
+        },
+        "number_vccs": {
+            "pat": re.compile(
+                r"Generated \d+ VCC\(s\), (?P<value>\d+) remaining after simplification"),
+            "parse": int,
+        },
         "symex_runtime": {
             "pat": re.compile(r"Runtime Symex: (?P<value>[-e\d\.]+)s"),
             "parse": float,
@@ -41,6 +54,11 @@ def get_metrics():
     for metric, info in metrics.items():
         for field in ("pat", "parse"):
             info.pop(field)
+
+    # 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)
+
     return metrics
 
 
@@ -76,6 +94,12 @@ def main(root_dir):
                         benchmarks[bench_name]["metrics"][metric] = parse(m["value"])
                     break
 
+    for bench_name, bench_info in benchmarks.items():
+        n_steps = bench_info["metrics"]["number_program_steps"]
+        rm_steps = bench_info["metrics"]["removed_program_steps"]
+        bench_info["metrics"]["number_program_steps"] = n_steps - rm_steps
+        bench_info["metrics"].pop("removed_program_steps", None)
+
     return {
         "metrics": get_metrics(),
         "benchmarks": benchmarks,

tools/benchcomp/test/test_regression.py

@@ -105,6 +105,8 @@ def _run_kani_perf_test(self, command, expected_pass):
             "symex_runtime": float,
             "verification_time": float,
             "success": bool,
+            "number_program_steps": int,
+            "number_vccs": int,
         }
 
         all_succeeded = True