wip

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

.github/actions/cbmc/report.py

@@ -104,10 +104,14 @@ def classify_proof(r, baseline_runtimes, cfg):
     # Solver could not decide -- not a real failure, not a regression.
     if r.get("status") == "inconclusive":
         prev = (
-            f"{base_val}s" if base_val
-            else "failed" if base_failed
-            else "inconclusive" if base_inconclusive
-            else "omitted" if base_omitted
+            f"{base_val}s"
+            if base_val
+            else "failed"
+            if base_failed
+            else "inconclusive"
+            if base_inconclusive
+            else "omitted"
+            if base_omitted
             else "-"
         )
         # Was passing in the baseline, now inconclusive: surface as a warning.
@@ -165,8 +169,7 @@ def compute_total_runtime(data):
     return sum(
         r["value"]
         for r in data.get("runtimes", [])
-        if r.get("status") not in ("failed", "omitted", "inconclusive")
-        and "value" in r
+        if r.get("status") not in ("failed", "omitted", "inconclusive") and "value" in r
     )
 
 

flake.nix

@@ -23,8 +23,8 @@
         let
           pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.${system};
           util = pkgs.callPackage ./nix/util.nix {
-            inherit (pkgs) bitwuzla cvc5 z3;
-            inherit (pkgs-unstable) cbmc;
+            inherit (pkgs) bitwuzla z3;
+            inherit (pkgs-unstable) cbmc cvc5;
             # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11
             python3-for-slothy = pkgs-unstable.python3;
           };
@@ -232,8 +232,8 @@
             pkgs-unstable = inputs.nixpkgs-unstable.legacyPackages.x86_64-linux;
             util = pkgs.callPackage ./nix/util.nix {
               inherit pkgs;
-              inherit (pkgs) bitwuzla cvc5 z3;
-              inherit (pkgs-unstable) cbmc;
+              inherit (pkgs) bitwuzla z3;
+              inherit (pkgs-unstable) cbmc cvc5;
               # TODO: switch back to stable python3 for slothy once ortools is fixed in 25.11
               python3-for-slothy = pkgs-unstable.python3;
             };

nix/cbmc/default.nix

@@ -35,10 +35,9 @@ buildEnv {
           hash = "sha256-Lw037Z0t0ySxkgMXkbjNW5CB4QQLRrrSEBsLJqiomZ4=";
         };
       });
-
       inherit
         bitwuzla# 0.8.2
-        cvc5# 1.3.2
+        cvc5# 1.3.3 (taken from nixpkgs-unstable -- see flake.nix)
         ninja; # 1.13.2
     };
 }

proofs/cbmc/lib/summarize.py

@@ -122,9 +122,9 @@ def _parse_proof_pipeline(proof_pipeline):
             # wrapper_arguments (the args passed to `litani add-job`).
             wa = job.get("wrapper_arguments") or {}
             desc = wa.get("description") or ""
-            if desc.endswith(": checking safety properties") and _is_solver_inconclusive(
-                wa.get("stdout_file")
-            ):
+            if desc.endswith(
+                ": checking safety properties"
+            ) and _is_solver_inconclusive(wa.get("stdout_file")):
                 inconclusive = True
 
     if has_timeout: