From 31ca5378c8cb2109ca245df4efb1b94423323166 Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Fri, 15 Sep 2023 18:43:26 -0500 Subject: [PATCH] Store failure info in `Proof` (#654) I'm trying to simplify the kontrol code that computes failure logs for each of the failing proofs, and I thought maybe it would be simpler if we could just pass around the Proof object and have any necessary info be available from there. We already have functions of `Proof` that pertain to the proof status. Currently in KEVM to get the failure log, we have to call a function separately when we detect a proof has failed that computes this log, which requires a `KCFGExplore`, and also takes a nontrivial amount of time. We then have to pass this around as part of a tuple. This makes the computing of the failure info automatically happen when a failing proof is detected, and saves the `APRFailureInfo` object as a field in the `APRProof`. The potential drawback I see to this is it would hurt performance on failing proofs if the user doesn't care about generating the `APRFailureInfo` for the proof. --------- Co-authored-by: devops --- package/version | 2 +- pyproject.toml | 2 +- src/pyk/proof/reachability.py | 15 ++++++++++++++- 3 files changed, 16 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index b67246167..5abb16f50 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.442 +0.1.443 diff --git a/pyproject.toml b/pyproject.toml index 946acbfa0..73447ac3a 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.442" +version = "0.1.443" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index f18999f0f..d3542944f 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -47,6 +47,7 @@ class APRProof(Proof, KCFGExploration): target: int logs: dict[int, tuple[LogEntry, ...]] circularity: bool + failure_info: APRFailureInfo | None def __init__( self, @@ -65,6 +66,7 @@ def __init__( Proof.__init__(self, id, proof_dir=proof_dir, subproof_ids=subproof_ids, admitted=admitted) KCFGExploration.__init__(self, kcfg, terminal) + self.failure_info = None self.init = kcfg._resolve(init) self.target = kcfg._resolve(target) self.logs = logs @@ -534,6 +536,7 @@ class APRProver(Prover): main_module_name: str dependencies_module_name: str circularities_module_name: str + counterexample_info: bool _checked_terminals: set[int] @@ -541,10 +544,12 @@ def __init__( self, proof: APRProof, kcfg_explore: KCFGExplore, + counterexample_info: bool = False, ) -> None: super().__init__(kcfg_explore) self.proof = proof self.main_module_name = self.kcfg_explore.kprint.definition.main_module_name + self.counterexample_info = counterexample_info subproofs: list[Proof] = ( [Proof.read_proof_data(proof.proof_dir, i) for i in proof.subproof_ids] @@ -662,6 +667,9 @@ def advance_proof( if self.proof.kcfg.is_leaf(node.id) and not self.proof.is_target(node.id): self._check_subsume(node) + if self.proof.failed: + self.save_failure_info() + self.proof.write_proof_data() def refute_node(self, node: KCFG.Node) -> RefutationProof | None: @@ -730,8 +738,11 @@ def construct_node_refutation(self, node: KCFG.Node) -> RefutationProof | None: self.proof.add_subproof(refutation) return refutation + def save_failure_info(self) -> None: + self.proof.failure_info = self.failure_info() + def failure_info(self) -> APRFailureInfo: - return APRFailureInfo.from_proof(self.proof, self.kcfg_explore) + return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info) @dataclass(frozen=True) @@ -869,10 +880,12 @@ def __init__( self, proof: APRBMCProof, kcfg_explore: KCFGExplore, + counterexample_info: bool = False, ) -> None: super().__init__( proof, kcfg_explore=kcfg_explore, + counterexample_info=counterexample_info, ) self._checked_nodes = []