Add JSON support for VerificationResults

autoverify/cli/main.py

@@ -4,13 +4,12 @@
 import sys
 
 from autoverify import __version__ as AV_VERSION
-from autoverify.util.verifiers import get_all_complete_verifier_names
-
-from .install import (
+from autoverify.cli.install import (
     check_commit_hashes,
     try_install_verifiers,
     try_uninstall_verifiers,
 )
+from autoverify.util.verifiers import get_all_complete_verifier_names
 
 
 def _build_arg_parser() -> argparse.ArgumentParser:

autoverify/portfolio/portfolio_runner.py

@@ -18,6 +18,7 @@
     VerificationDataResult,
     csv_append_verification_result,
     init_verification_result_csv,
+    json_write_verification_result,
 )
 from autoverify.util.proc import cpu_count, nvidia_gpu_count
 from autoverify.util.resources import to_allocation
@@ -219,6 +220,33 @@ def _csv_log_result(
         vdr = VerificationDataResult.from_verification_result(res_d, inst_d)
         csv_append_verification_result(vdr, out_csv)
 
+    @staticmethod
+    def _json_log_result(
+        out_json: Path,
+        result: CompleteVerificationResult,
+        instance: VerificationInstance,
+        verifier: str,
+        configuration: Configuration,
+    ):
+        if isinstance(result, Ok):
+            res_d = result.unwrap()
+            success = "OK"
+        elif isinstance(result, Err):
+            res_d = result.unwrap_err()
+            success = "ERR"
+
+        inst_d = {
+            "network": instance.network,
+            "property": instance.property,
+            "timeout": instance.timeout,
+            "verifier": verifier,
+            "config": configuration,
+            "success": success,
+        }
+
+        vdr = VerificationDataResult.from_verification_result(res_d, inst_d)
+        json_write_verification_result(vdr, out_json)
+
     @staticmethod
     def _vbs_from_cost_dict(cost_dict: _CostDict) -> _VbsResult:
         vbs: _VbsResult = {}
@@ -286,6 +314,7 @@ def verify_instances(
         instances: Iterable[VerificationInstance],
         *,
         out_csv: Path | None = None,
+        out_json: Path | None = None,
         vnncompat: bool = False,
         benchmark: str | None = None,
         verifier_kwargs: dict[str, dict[str, Any]] | None = None,
@@ -295,7 +324,8 @@ def verify_instances(
 
         Arguments:
             instances: Instances to evaluate.
-            out_csv: File where the results are written to.
+            out_csv: CSV File where the results are written to.
+            out_json: JSON File where the results are written to.
             vnncompat: Use some compat kwargs.
             benchmark: Only if vnncompat, benchmark name.
             verifier_kwargs: Kwargs passed to verifiers.
@@ -307,11 +337,14 @@ def verify_instances(
         if out_csv:
             out_csv = out_csv.expanduser().resolve()
 
+        if out_json:
+            out_json = out_json.expanduser().resolve()
+
         results: dict[VerificationInstance, VerificationDataResult] = {}
 
         with concurrent.futures.ThreadPoolExecutor() as executor:
-            for instance in instances:
-                logger.info(f"Running portfolio on {str(instance)}")
+            for index, instance in enumerate(instances):
+                logger.info(f"{index} - Running portfolio on {str(instance)}")
 
                 futures: dict[
                     Future[CompleteVerificationResult], ConfiguredVerifier
@@ -359,6 +392,15 @@ def verify_instances(
                                 fut_cv.configuration,
                             )
 
+                        if out_json:
+                            self._json_log_result(
+                                out_json,
+                                result,
+                                instance,
+                                fut_cv.verifier,
+                                fut_cv.configuration,
+                            )
+
         return results
 
     def _process_result(

autoverify/util/instances.py

@@ -3,6 +3,7 @@
 from __future__ import annotations
 
 import csv
+import json
 from collections.abc import Sequence
 from dataclasses import dataclass
 from pathlib import Path
@@ -22,6 +23,7 @@
 class VerificationDataResult:
     """_summary_."""
 
+    # TODO: Convert files to path objects
     network: str
     property: str
     timeout: int | None
@@ -30,9 +32,9 @@ class VerificationDataResult:
     success: Literal["OK", "ERR"]
     result: VerificationResultString
     took: float
-    counter_example: str | tuple[str, str] | None
-    stderr: str | None
-    stdout: str | None
+    counter_example: str | tuple[str, str] | None = None
+    stderr: str | None = None
+    stdout: str | None = None
 
     def __post_init__(self):
         """_summary_."""
@@ -58,6 +60,25 @@ def as_csv_row(self) -> list[str]:
             self.stdout or "",
         ]
 
+    def as_json_row(self) -> dict[str, Any]:
+        """Convert data to a json item."""
+        if isinstance(self.counter_example, tuple):
+            self.counter_example = "\n".join(self.counter_example)
+
+        return {
+            "network": str(self.network),
+            "property": str(self.property),
+            "timeout": str(self.timeout),
+            "verifier": self.verifier,
+            "config": str(self.config),
+            "success": self.success,
+            "result": self.result,
+            "took": str(self.took),
+            # "counter_example": self.counter_example or "",
+            "stderr": self.stderr or "",
+            "stdout": self.stdout or "",
+        }
+
     @classmethod
     def from_verification_result(
         cls,
@@ -97,6 +118,30 @@ def csv_append_verification_result(
         writer.writerow(verification_result.as_csv_row())
 
 
+def json_write_verification_result(
+    verification_result: VerificationDataResult, json_path: Path
+):
+    """_summary_."""
+    # Create json file if it does not exist
+    if not json_path.exists():
+        with open(str(json_path.expanduser()), "w") as json_file:
+            json.dump({"instances": []}, json_file)
+
+    # Append to json file
+    with open(str(json_path.expanduser()), "r+") as json_file:
+        try:
+            file_data = json.load(json_file)
+            # Check if file_data is empty
+            if not file_data:
+                file_data = {"instances": []}
+        except json.decoder.JSONDecodeError:
+            file_data = {"instances": []}
+
+        file_data["instances"].append(verification_result.as_json_row())
+        json_file.seek(0)
+        json.dump(file_data, json_file)
+
+
 def read_verification_result_from_csv(
     csv_path: Path,
 ) -> list[VerificationDataResult]:
@@ -111,6 +156,20 @@ def read_verification_result_from_csv(
     return verification_results
 
 
+def read_verification_result_from_json(
+    json_path: Path,
+) -> list[VerificationDataResult]:
+    """Reads a verification results json to a list of its dataclass."""
+    results = pd.read_json(json_path)["instances"].tolist()
+
+    verification_results: list[VerificationDataResult] = []
+
+    for res in results:
+        verification_results.append(VerificationDataResult(**res))
+
+    return verification_results
+
+
 def write_verification_results_to_csv(results: pd.DataFrame, csv_path: Path):
     """Writes a verification results df to a csv."""
     results.to_csv(csv_path, index=False)