From 2370f124f657f1e171bb6f3053b8d85adecdf9d8 Mon Sep 17 00:00:00 2001 From: TrisCC Date: Wed, 26 Jun 2024 14:43:10 +0200 Subject: [PATCH 1/3] Add JSON support and fix VeriNet installer --- .../installers/verinet/environment.yml | 2 +- autoverify/cli/main.py | 5 +- autoverify/portfolio/portfolio_runner.py | 48 +++++++++++++- autoverify/util/instances.py | 65 ++++++++++++++++++- 4 files changed, 110 insertions(+), 10 deletions(-) diff --git a/autoverify/cli/install/installers/verinet/environment.yml b/autoverify/cli/install/installers/verinet/environment.yml index 2cecdab..95328ad 100644 --- a/autoverify/cli/install/installers/verinet/environment.yml +++ b/autoverify/cli/install/installers/verinet/environment.yml @@ -56,7 +56,7 @@ dependencies: - markupsafe==2.1.3 - matplotlib==3.7.1 - mpmath==1.3.0 - - netron==7.0.0 + - netron==7.7.3 - networkx==3.1 - numpy==1.21.6 - nvidia-cublas-cu11==11.10.3.66 diff --git a/autoverify/cli/main.py b/autoverify/cli/main.py index 56ef70e..cc21159 100644 --- a/autoverify/cli/main.py +++ b/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: diff --git a/autoverify/portfolio/portfolio_runner.py b/autoverify/portfolio/portfolio_runner.py index b060a34..274553b 100644 --- a/autoverify/portfolio/portfolio_runner.py +++ b/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( diff --git a/autoverify/util/instances.py b/autoverify/util/instances.py index 94abecf..6ceb19b 100644 --- a/autoverify/util/instances.py +++ b/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": self.network, + "property": 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) From ab6b4b29c5262977a10373d03d2c34c7a5ae606a Mon Sep 17 00:00:00 2001 From: TrisCC Date: Tue, 2 Jul 2024 23:05:11 +0200 Subject: [PATCH 2/3] Fix type error --- autoverify/util/instances.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/autoverify/util/instances.py b/autoverify/util/instances.py index 6ceb19b..547dd9d 100644 --- a/autoverify/util/instances.py +++ b/autoverify/util/instances.py @@ -66,8 +66,8 @@ def as_json_row(self) -> dict[str, Any]: self.counter_example = "\n".join(self.counter_example) return { - "network": self.network, - "property": self.property, + "network": str(self.network), + "property": str(self.property), "timeout": str(self.timeout), "verifier": self.verifier, "config": str(self.config), From eebcd97b5312a4d09514454e2b094a6801bf3692 Mon Sep 17 00:00:00 2001 From: TrisCC Date: Tue, 16 Jul 2024 16:39:43 +0200 Subject: [PATCH 3/3] Revert Verinet update --- autoverify/cli/install/installers/verinet/environment.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/autoverify/cli/install/installers/verinet/environment.yml b/autoverify/cli/install/installers/verinet/environment.yml index 95328ad..2cecdab 100644 --- a/autoverify/cli/install/installers/verinet/environment.yml +++ b/autoverify/cli/install/installers/verinet/environment.yml @@ -56,7 +56,7 @@ dependencies: - markupsafe==2.1.3 - matplotlib==3.7.1 - mpmath==1.3.0 - - netron==7.7.3 + - netron==7.0.0 - networkx==3.1 - numpy==1.21.6 - nvidia-cublas-cu11==11.10.3.66