From eb9be597a35664e3b1b1457bf82120bc5106ed08 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 5 Sep 2023 19:26:58 -0500 Subject: [PATCH 01/30] Add option to split into subproofs when a branching threshold is reached --- src/pyk/proof/reachability.py | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 3a20026a5..6563375ae 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -627,6 +627,7 @@ def advance_proof( cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), fail_fast: bool = False, + max_branches: int | None = 1, ) -> None: iterations = 0 @@ -634,6 +635,13 @@ def advance_proof( while self.proof.pending: self.proof.write_proof_data() + + if len(self.proof.pending) > max_branches: + _LOGGER.info(f'Reached max_branches bound on number of pending nodes. Nodes {self.proof.pending} will be turned into subproofs.') + for pending_node in self.proof.pending: + self.delegate_to_subproof(pending_node) + break + if fail_fast and self.proof.failed: _LOGGER.warning( f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}' @@ -661,6 +669,29 @@ def advance_proof( self.proof.write_proof_data() + def delegate_to_subproof(self, node: KCFG.Node) -> None: + _LOGGER.info(f'Delegating node {node.id} to a new proof.') + subproof = self.construct_node_subproof(node) + self.proof.add_subproof(subproof) + self.proof.kcfg.add_stuck(node.id) + + def construct_node_subproof(self, node: KCFG.Node) -> APRProof: + + kcfg = KCFG(self.proof.proof_dir) + kcfg.add_node(node) + target_node = self.proof.kcfg.node(self.proof.target) + kcfg.add_node(target_node) + + return APRProof( + id=f'{self.proof.id}_node_{node.id}', + kcfg=kcfg, + terminal=[], + init=node.id, + target=target_node.id, + logs=[], + proof_dir=self.proof.proof_dir, + ) + def refute_node(self, node: KCFG.Node) -> RefutationProof | None: _LOGGER.info(f'Attempting to refute node {node.id}') refutation = self.construct_node_refutation(node) From c1ce99589967842cb7c59886bb22f167a7ad1ecc Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 6 Sep 2023 12:55:14 -0500 Subject: [PATCH 02/30] Make max_iterations disabled by default --- src/pyk/proof/reachability.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 6563375ae..1fa4eed0a 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -627,7 +627,7 @@ def advance_proof( cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), fail_fast: bool = False, - max_branches: int | None = 1, + max_branches: int | None = None, ) -> None: iterations = 0 @@ -636,7 +636,7 @@ def advance_proof( while self.proof.pending: self.proof.write_proof_data() - if len(self.proof.pending) > max_branches: + if max_branches is not None and len(self.proof.pending) > max_branches: _LOGGER.info(f'Reached max_branches bound on number of pending nodes. Nodes {self.proof.pending} will be turned into subproofs.') for pending_node in self.proof.pending: self.delegate_to_subproof(pending_node) From 5d6cfb3d11cf4b010f3bb640e9137a46cdf48ad9 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 6 Sep 2023 13:24:07 -0500 Subject: [PATCH 03/30] Add test for subproof delegation --- src/pyk/proof/reachability.py | 2 +- src/tests/integration/kcfg/test_imp.py | 35 ++++++++++++++++++++++++++ 2 files changed, 36 insertions(+), 1 deletion(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 1fa4eed0a..096e41af8 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -637,7 +637,7 @@ def advance_proof( self.proof.write_proof_data() if max_branches is not None and len(self.proof.pending) > max_branches: - _LOGGER.info(f'Reached max_branches bound on number of pending nodes. Nodes {self.proof.pending} will be turned into subproofs.') + _LOGGER.info(f'Reached max_branches={max_branches} bound on number of pending nodes. Nodes {self.proof.pending} will be turned into subproofs.') for pending_node in self.proof.pending: self.delegate_to_subproof(pending_node) break diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index 24e89f750..e8dee8fa1 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -1242,6 +1242,41 @@ def test_anti_unify_forget_values( assert anti_unifier.kast == expected_anti_unifier.kast + def test_delegate_to_subproof( + self, + kcfg_explore: KCFGExplore, + proof_dir: Path, + kprove: KProve, + ): + claim = single( + kprove.get_claims( + K_FILES / 'imp-simple-spec.k', + spec_module_name='IMP-SIMPLE-SPEC', + claim_labels=['IMP-SIMPLE-SPEC.failing-if'], + ) + ) + + proof = APRProof.from_claim( + kprove.definition, + claim, + logs={}, + proof_dir=proof_dir, + ) + + prover = APRProver( + proof, + kcfg_explore=kcfg_explore, + ) + + assert len(proof.subproofs) == 0 + assert len(proof.pending) == 1 + + prover.advance_proof(max_branches=1) + + assert len(proof.subproofs) == 2 + assert len(proof.pending) == 0 + + def test_anti_unify_keep_values( self, kcfg_explore: KCFGExplore, From 9379310c36e0f607550124cada5dc7c478881c46 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 6 Sep 2023 18:27:24 +0000 Subject: [PATCH 04/30] Set Version: 0.1.434 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 0e0e00d48..22eec624e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.433 +0.1.434 diff --git a/pyproject.toml b/pyproject.toml index 56784b98c..9623aec11 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.433" +version = "0.1.434" description = "" authors = [ "Runtime Verification, Inc. ", From efe6cebcbfa174bef91f1a92d5f3b861b609e2f1 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 6 Sep 2023 18:28:44 +0000 Subject: [PATCH 05/30] Set Version: 0.1.435 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 22eec624e..ebdbbb84d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.434 +0.1.435 diff --git a/pyproject.toml b/pyproject.toml index 9623aec11..dd96b1445 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.434" +version = "0.1.435" description = "" authors = [ "Runtime Verification, Inc. ", From 43953f4a64dd5eaafbe38904e3879a26097c671b Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 6 Sep 2023 13:30:57 -0500 Subject: [PATCH 06/30] Fix formatting and typing --- src/pyk/proof/reachability.py | 11 ++++++----- src/tests/integration/kcfg/test_imp.py | 7 +++---- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 096e41af8..c7c7c61a8 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -637,11 +637,13 @@ def advance_proof( self.proof.write_proof_data() if max_branches is not None and len(self.proof.pending) > max_branches: - _LOGGER.info(f'Reached max_branches={max_branches} bound on number of pending nodes. Nodes {self.proof.pending} will be turned into subproofs.') + _LOGGER.info( + f'Reached max_branches={max_branches} bound on number of pending nodes. Nodes {self.proof.pending} will be turned into subproofs.' + ) for pending_node in self.proof.pending: - self.delegate_to_subproof(pending_node) + self.delegate_to_subproof(pending_node) break - + if fail_fast and self.proof.failed: _LOGGER.warning( f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}' @@ -676,7 +678,6 @@ def delegate_to_subproof(self, node: KCFG.Node) -> None: self.proof.kcfg.add_stuck(node.id) def construct_node_subproof(self, node: KCFG.Node) -> APRProof: - kcfg = KCFG(self.proof.proof_dir) kcfg.add_node(node) target_node = self.proof.kcfg.node(self.proof.target) @@ -688,7 +689,7 @@ def construct_node_subproof(self, node: KCFG.Node) -> APRProof: terminal=[], init=node.id, target=target_node.id, - logs=[], + logs={}, proof_dir=self.proof.proof_dir, ) diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index e8dee8fa1..cec7077fe 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -1247,7 +1247,7 @@ def test_delegate_to_subproof( kcfg_explore: KCFGExplore, proof_dir: Path, kprove: KProve, - ): + ) -> None: claim = single( kprove.get_claims( K_FILES / 'imp-simple-spec.k', @@ -1268,15 +1268,14 @@ def test_delegate_to_subproof( kcfg_explore=kcfg_explore, ) - assert len(proof.subproofs) == 0 + assert len(list(proof.subproofs)) == 0 assert len(proof.pending) == 1 prover.advance_proof(max_branches=1) - assert len(proof.subproofs) == 2 + assert len(list(proof.subproofs)) == 2 assert len(proof.pending) == 0 - def test_anti_unify_keep_values( self, kcfg_explore: KCFGExplore, From dd18600ab0b47cfe0ca742a1111a980401f87c8f Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 7 Sep 2023 17:47:38 -0500 Subject: [PATCH 07/30] Add new APRProof-level node status for nodes that have been subproofed --- src/pyk/proof/reachability.py | 29 +++++++++++++++++++++++++++-- src/tests/unit/test_proof.py | 4 ++++ 2 files changed, 31 insertions(+), 2 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index c7c7c61a8..fabccaedb 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -43,6 +43,7 @@ class APRProof(Proof, KCFGExploration): """ node_refutations: dict[int, RefutationProof] # TODO _node_refutatations + subproof_nodes: set[int] init: int target: int logs: dict[int, tuple[LogEntry, ...]] @@ -57,6 +58,7 @@ def __init__( target: NodeIdLike, logs: dict[int, tuple[LogEntry, ...]], proof_dir: Path | None = None, + subproof_nodes: Iterable[int] | None = None, node_refutations: dict[int, str] | None = None, subproof_ids: Iterable[str] = (), circularity: bool = False, @@ -76,6 +78,8 @@ def __init__( ensure_dir_path(self.proof_dir) ensure_dir_path(self.proof_subdir) + self.subproof_nodes = set(subproof_nodes) if subproof_nodes is not None else set() + if node_refutations is not None: refutations_not_in_subprroofs = set(node_refutations.values()).difference( set(subproof_ids if subproof_ids else []) @@ -101,11 +105,19 @@ def is_refuted(self, node_id: NodeIdLike) -> bool: return self.kcfg._resolve(node_id) in self.node_refutations.keys() def is_pending(self, node_id: NodeIdLike) -> bool: - return self.is_explorable(node_id) and not self.is_target(node_id) and not self.is_refuted(node_id) + return ( + self.is_explorable(node_id) + and not self.is_target(node_id) + and not self.is_refuted(node_id) + and not self.is_subproof_node(node_id) + ) def is_init(self, node_id: NodeIdLike) -> bool: return self.kcfg._resolve(node_id) == self.kcfg._resolve(self.init) + def is_subproof_node(self, node_id: NodeIdLike) -> bool: + return self.kcfg._resolve(node_id) in self.subproof_nodes + def is_target(self, node_id: NodeIdLike) -> bool: return self.kcfg._resolve(node_id) == self.kcfg._resolve(self.target) @@ -115,8 +127,12 @@ def is_failing(self, node_id: NodeIdLike) -> bool: and not self.is_explorable(node_id) and not self.is_target(node_id) and not self.is_refuted(node_id) + and not self.is_subproof_node(node_id) ) + def add_subproof_node(self, node_id: int) -> None: + self.subproof_nodes.add(node_id) + def shortest_path_to(self, node_id: NodeIdLike) -> tuple[KCFG.Successor, ...]: spb = self.kcfg.shortest_path_between(self.init, node_id) assert spb is not None @@ -155,6 +171,7 @@ def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | Non id = dct['id'] circularity = dct.get('circularity', False) admitted = dct.get('admitted', False) + subproof_nodes = dct['subproof_nodes'] if 'subproof_nodes' in dct else [] subproof_ids = dct['subproof_ids'] if 'subproof_ids' in dct else [] node_refutations: dict[int, str] = {} if 'node_refutation' in dct: @@ -174,6 +191,7 @@ def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | Non circularity=circularity, admitted=admitted, proof_dir=proof_dir, + subproof_nodes=subproof_nodes, subproof_ids=subproof_ids, node_refutations=node_refutations, ) @@ -228,6 +246,7 @@ def dict(self) -> dict[str, Any]: dct['terminal'] = sorted(self._terminal) dct['init'] = self.init dct['target'] = self.target + dct['subproof_nodes'] = sorted(self.subproof_nodes) dct['node_refutations'] = {node_id: proof.id for (node_id, proof) in self.node_refutations.items()} dct['circularity'] = self.circularity logs = {int(k): [l.to_dict() for l in ls] for k, ls in self.logs.items()} @@ -249,6 +268,7 @@ def summary(self) -> CompositeSummary: len(self.kcfg.stuck), len(self._terminal), len(self.node_refutations), + len(self.subproof_nodes), len(self.subproof_ids), ), *subproofs_summaries, @@ -517,6 +537,7 @@ def summary(self) -> CompositeSummary: len(self.kcfg.stuck), len(self._terminal), len(self.node_refutations), + len(self.subproof_nodes), len(self._bounded), len(self.subproof_ids), ), @@ -675,7 +696,7 @@ def delegate_to_subproof(self, node: KCFG.Node) -> None: _LOGGER.info(f'Delegating node {node.id} to a new proof.') subproof = self.construct_node_subproof(node) self.proof.add_subproof(subproof) - self.proof.kcfg.add_stuck(node.id) + self.proof.add_subproof_node(node.id) def construct_node_subproof(self, node: KCFG.Node) -> APRProof: kcfg = KCFG(self.proof.proof_dir) @@ -774,6 +795,7 @@ class APRSummary(ProofSummary): stuck: int terminal: int refuted: int + subproof_nodes: int subproofs: int @property @@ -788,6 +810,7 @@ def lines(self) -> list[str]: f' stuck: {self.stuck}', f' terminal: {self.terminal}', f' refuted: {self.refuted}', + f' subproof_nodes: {self.subproof_nodes}', f'Subproofs: {self.subproofs}', ] @@ -948,6 +971,7 @@ class APRBMCSummary(ProofSummary): stuck: int terminal: int refuted: int + subproof_nodes: int bounded: int subproofs: int @@ -962,6 +986,7 @@ def lines(self) -> list[str]: f' stuck: {self.stuck}', f' terminal: {self.terminal}', f' refuted: {self.refuted}', + f' subproof_nodes: {self.subproof_nodes}', f' bounded: {self.bounded}', f'Subproofs: {self.subproofs}', ] diff --git a/src/tests/unit/test_proof.py b/src/tests/unit/test_proof.py index 471bc1de1..2753ba8e8 100644 --- a/src/tests/unit/test_proof.py +++ b/src/tests/unit/test_proof.py @@ -341,6 +341,7 @@ def test_apr_proof_summary(proof_dir: Path) -> None: failing=0, stuck=0, terminal=0, + subproof_nodes=0, refuted=0, subproofs=0, ) @@ -363,6 +364,7 @@ def test_aprbmc_proof_summary(proof_dir: Path) -> None: failing=0, stuck=0, terminal=0, + subproof_nodes=0, refuted=0, subproofs=0, bounded=0, @@ -399,6 +401,7 @@ def test_apr_proof_summary_subproofs(proof_dir: Path) -> None: failing=0, stuck=0, terminal=0, + subproof_nodes=0, refuted=0, subproofs=1, ) @@ -414,6 +417,7 @@ def test_apr_proof_summary_subproofs(proof_dir: Path) -> None: failing=0, stuck=0, terminal=0, + subproof_nodes=0, refuted=0, subproofs=1, ), From 5a768d4e4d9ddcd32998bb7eb33c25522cb3734f Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 7 Sep 2023 22:50:26 +0000 Subject: [PATCH 08/30] Set Version: 0.1.437 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 486fb4628..88491bbf1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.436 \ No newline at end of file +0.1.437 diff --git a/pyproject.toml b/pyproject.toml index 507ec6429..77f588ae5 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.436" +version = "0.1.437" description = "" authors = [ "Runtime Verification, Inc. ", From 0d125941c4d7c596d7b049bf51ec9cc0ce16fa17 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 12 Sep 2023 20:56:00 -0500 Subject: [PATCH 09/30] Add custom function arg to determine IDs of generated subproofs --- src/pyk/kcfg/kcfg.py | 2 ++ src/pyk/kcfg/show.py | 11 +++++++++++ src/pyk/proof/reachability.py | 24 ++++++++++++++++++------ 3 files changed, 31 insertions(+), 6 deletions(-) diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index ba6539476..76361031f 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -445,6 +445,8 @@ def create_node(self, cterm: CTerm) -> Node: term = cterm.kast term = remove_source_attributes(term) cterm = CTerm.from_kast(term) + while self._node_id in self._nodes: + self._node_id += 1 node = KCFG.Node(self._node_id, cterm) self._node_id += 1 self._nodes[node.id] = node diff --git a/src/pyk/kcfg/show.py b/src/pyk/kcfg/show.py index 5aba44f11..3d661e93d 100644 --- a/src/pyk/kcfg/show.py +++ b/src/pyk/kcfg/show.py @@ -280,6 +280,17 @@ def _sorted_init_nodes() -> tuple[list[KCFG.Node], list[KCFG.Node]]: return (init_nodes + init_leaf_nodes, remaining_nodes) init, _ = _sorted_init_nodes() + + # print([node.id for node in kcfg.nodes]) + # print([node.id for node in processed_nodes]) + + # for node in kcfg.nodes: + # print(kcfg.is_root(node.id)) + # print(kcfg.is_leaf(node.id)) + # print('') + # + # print(init) + # while init: ret_lines.append(('unknown', [''])) _print_subgraph('', init[0], []) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index fabccaedb..b3d878875 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -3,7 +3,7 @@ import json import logging from dataclasses import dataclass -from typing import TYPE_CHECKING +from typing import TYPE_CHECKING, Callable from pyk.kore.rpc import LogEntry @@ -48,6 +48,7 @@ class APRProof(Proof, KCFGExploration): target: int logs: dict[int, tuple[LogEntry, ...]] circularity: bool + generate_subproof_name: Callable[[int], str] | None def __init__( self, @@ -63,6 +64,7 @@ def __init__( subproof_ids: Iterable[str] = (), circularity: bool = False, admitted: bool = False, + generate_subproof_name: Callable[[int], str] | None = None, ): Proof.__init__(self, id, proof_dir=proof_dir, subproof_ids=subproof_ids, admitted=admitted) KCFGExploration.__init__(self, kcfg, terminal) @@ -73,6 +75,7 @@ def __init__( self.circularity = circularity self.node_refutations = {} self.kcfg.cfg_dir = self.proof_subdir / 'kcfg' if self.proof_subdir else None + self.generate_subproof_name = generate_subproof_name if self.proof_dir is not None and self.proof_subdir is not None: ensure_dir_path(self.proof_dir) @@ -700,16 +703,25 @@ def delegate_to_subproof(self, node: KCFG.Node) -> None: def construct_node_subproof(self, node: KCFG.Node) -> APRProof: kcfg = KCFG(self.proof.proof_dir) - kcfg.add_node(node) target_node = self.proof.kcfg.node(self.proof.target) - kcfg.add_node(target_node) + + node_cterm, _ = self.kcfg_explore.cterm_simplify(node.cterm) + ( + target_node_cterm, + _, + ) = self.kcfg_explore.cterm_simplify(target_node.cterm) + + new_init = kcfg.create_node(node_cterm) + new_target = kcfg.create_node(target_node_cterm) + + assert self.proof.generate_subproof_name is not None return APRProof( - id=f'{self.proof.id}_node_{node.id}', + id=self.proof.generate_subproof_name(node.id), kcfg=kcfg, terminal=[], - init=node.id, - target=target_node.id, + init=new_init.id, + target=new_target.id, logs={}, proof_dir=self.proof.proof_dir, ) From d259f23fe282348402f9fd018d567959460004d0 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 13 Sep 2023 16:30:05 -0500 Subject: [PATCH 10/30] Make branch extraction more intelligent --- src/pyk/kcfg/explore.py | 30 +++++++++++++++++++++--------- src/pyk/kcfg/kcfg.py | 9 ++++++--- 2 files changed, 27 insertions(+), 12 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 3f69a26d9..329663b60 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -377,14 +377,24 @@ def extend( if self._check_abstract(node, kcfg): return - if not kcfg.splits(target_id=node.id): - branches = self.kcfg_semantics.extract_branches(node.cterm) - if branches: - kcfg.split_on_constraints(node.id, branches) - _LOGGER.info( - f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}' - ) - return + branches = self.kcfg_semantics.extract_branches(node.cterm) + + branch_conditions = [] + branch_cterms = [] + + for constraint in branches: + cterm = node.cterm.add_constraint(constraint) + cterm, _ = self.cterm_simplify(cterm) + if not cterm.is_bottom: + branch_conditions.append(constraint) + branch_cterms.append(cterm) + + if len(branch_cterms) > 1 and branches: + kcfg.branch(node.id, zip(branch_cterms, branch_conditions, strict=True)) + _LOGGER.info( + f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}' + ) + return _LOGGER.info(f'Extending KCFG from node {self.id}: {shorten_hashes(node.id)}') _is_vacuous, depth, cterm, next_cterms, next_node_logs = self.cterm_execute( @@ -437,7 +447,9 @@ def extend( # Split on branch patterns if any(branch_pattern.match(branch_and) for branch_pattern in branch_patterns): - kcfg.split_on_constraints(node.id, branches) + branch_cterms = [node.cterm.add_constraint(branch) for branch in branches] + + kcfg.branch(node.id, zip(branch_cterms, branches, strict=True)) _LOGGER.info( f'Found {len(branches)} branches for node {self.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}' ) diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index 3aafd55f7..2a0f70859 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -724,10 +724,13 @@ def create_ndbranch(self, source_id: NodeIdLike, ndbranches: Iterable[NodeIdLike ndbranch = KCFG.NDBranch(self.node(source_id), tuple(self.node(nid) for nid in ndbranches)) self._ndbranches[source_id] = ndbranch - def split_on_constraints(self, source_id: NodeIdLike, constraints: Iterable[KInner]) -> list[int]: + def branch(self, source_id: NodeIdLike, splits: Iterable[tuple[CTerm, KInner]]) -> list[int]: source = self.node(source_id) - branch_node_ids = [self.create_node(source.cterm.add_constraint(c)).id for c in constraints] - csubsts = [CSubst(constraints=flatten_label('#And', constraint)) for constraint in constraints] + branch_node_ids = [] + csubsts = [] + for cterm, constraint in splits: + branch_node_ids.append(self.create_node(cterm).id) + csubsts.append(CSubst(constraints=flatten_label('#And', constraint))) self.create_split(source.id, zip(branch_node_ids, csubsts, strict=True)) return branch_node_ids From 2863769bbc53f68990ab2de1af0d9e39e062ff2e Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 13 Sep 2023 21:37:41 +0000 Subject: [PATCH 11/30] Set Version: 0.1.440 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 84ea58b9e..c2d2e179c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.439 +0.1.440 diff --git a/pyproject.toml b/pyproject.toml index a7ee1be7b..4e93eb47a 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.439" +version = "0.1.440" description = "" authors = [ "Runtime Verification, Inc. ", From 2826395adab1f23b16fc05ea4e50fb89baa89760 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 13 Sep 2023 17:33:53 -0500 Subject: [PATCH 12/30] Do not immediately apply simplifications, only count non-bottom nodes --- src/pyk/kcfg/explore.py | 40 ++++++++++++++++++++++++++-------------- src/pyk/kcfg/kcfg.py | 9 +++------ 2 files changed, 29 insertions(+), 20 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 329663b60..5db733200 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -377,20 +377,34 @@ def extend( if self._check_abstract(node, kcfg): return - branches = self.kcfg_semantics.extract_branches(node.cterm) - - branch_conditions = [] - branch_cterms = [] - - for constraint in branches: + # branches = self.kcfg_semantics.extract_branches(node.cterm) + # + # branch_conditions = [] + # branch_cterms = [] + # + # for constraint in branches: + # cterm = node.cterm.add_constraint(constraint) + # cterm, _ = self.cterm_simplify(cterm) + # if not cterm.is_bottom: + # branch_conditions.append(constraint) + # branch_cterms.append(cterm) + # + # if len(branch_cterms) > 1 and branches: + # kcfg.branch(node.id, zip(branch_cterms, branch_conditions, strict=True)) + # _LOGGER.info( + # f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}' + # ) + # return + + _branches = self.kcfg_semantics.extract_branches(node.cterm) + branches = [] + for constraint in _branches: cterm = node.cterm.add_constraint(constraint) cterm, _ = self.cterm_simplify(cterm) if not cterm.is_bottom: - branch_conditions.append(constraint) - branch_cterms.append(cterm) - - if len(branch_cterms) > 1 and branches: - kcfg.branch(node.id, zip(branch_cterms, branch_conditions, strict=True)) + branches.append(constraint) + if len(branches) > 1: + kcfg.split_on_constraints(node.id, branches) _LOGGER.info( f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}' ) @@ -447,9 +461,7 @@ def extend( # Split on branch patterns if any(branch_pattern.match(branch_and) for branch_pattern in branch_patterns): - branch_cterms = [node.cterm.add_constraint(branch) for branch in branches] - - kcfg.branch(node.id, zip(branch_cterms, branches, strict=True)) + kcfg.split_on_constraints(node.id, branches) _LOGGER.info( f'Found {len(branches)} branches for node {self.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}' ) diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index 2a0f70859..3aafd55f7 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -724,13 +724,10 @@ def create_ndbranch(self, source_id: NodeIdLike, ndbranches: Iterable[NodeIdLike ndbranch = KCFG.NDBranch(self.node(source_id), tuple(self.node(nid) for nid in ndbranches)) self._ndbranches[source_id] = ndbranch - def branch(self, source_id: NodeIdLike, splits: Iterable[tuple[CTerm, KInner]]) -> list[int]: + def split_on_constraints(self, source_id: NodeIdLike, constraints: Iterable[KInner]) -> list[int]: source = self.node(source_id) - branch_node_ids = [] - csubsts = [] - for cterm, constraint in splits: - branch_node_ids.append(self.create_node(cterm).id) - csubsts.append(CSubst(constraints=flatten_label('#And', constraint))) + branch_node_ids = [self.create_node(source.cterm.add_constraint(c)).id for c in constraints] + csubsts = [CSubst(constraints=flatten_label('#And', constraint)) for constraint in constraints] self.create_split(source.id, zip(branch_node_ids, csubsts, strict=True)) return branch_node_ids From 07574aa687bd10f4c62dbb1647126ac2cd949d18 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 13 Sep 2023 17:52:03 -0500 Subject: [PATCH 13/30] Use kast_simplify --- src/pyk/kcfg/explore.py | 25 +++---------------------- 1 file changed, 3 insertions(+), 22 deletions(-) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 5db733200..57d06c7e1 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -377,31 +377,12 @@ def extend( if self._check_abstract(node, kcfg): return - # branches = self.kcfg_semantics.extract_branches(node.cterm) - # - # branch_conditions = [] - # branch_cterms = [] - # - # for constraint in branches: - # cterm = node.cterm.add_constraint(constraint) - # cterm, _ = self.cterm_simplify(cterm) - # if not cterm.is_bottom: - # branch_conditions.append(constraint) - # branch_cterms.append(cterm) - # - # if len(branch_cterms) > 1 and branches: - # kcfg.branch(node.id, zip(branch_cterms, branch_conditions, strict=True)) - # _LOGGER.info( - # f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}' - # ) - # return - _branches = self.kcfg_semantics.extract_branches(node.cterm) branches = [] for constraint in _branches: - cterm = node.cterm.add_constraint(constraint) - cterm, _ = self.cterm_simplify(cterm) - if not cterm.is_bottom: + kast = mlAnd(list(node.cterm.constraints) + [constraint]) + kast, _ = self.kast_simplify(kast) + if not CTerm._is_bottom(kast): branches.append(constraint) if len(branches) > 1: kcfg.split_on_constraints(node.id, branches) From 6abe235f413b1aa5e318e77dacf03518ab84cecb Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 15 Sep 2023 21:25:24 +0000 Subject: [PATCH 14/30] Set Version: 0.1.443 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index eb2eadbed..5abb16f50 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.442 \ No newline at end of file +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. ", From 5bf02dd7ab54aa4a035a6043ce6fe2b898c54cdd Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 15 Sep 2023 23:54:02 +0000 Subject: [PATCH 15/30] Set Version: 0.1.444 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 5abb16f50..8cc010e6a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.443 +0.1.444 diff --git a/pyproject.toml b/pyproject.toml index 73447ac3a..7dcb3ba3c 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.443" +version = "0.1.444" description = "" authors = [ "Runtime Verification, Inc. ", From 8b267aa0c83d7d78071203db80e0b0aa8c4f1b5e Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 15 Sep 2023 21:01:37 -0500 Subject: [PATCH 16/30] Fix subproof_nodes not being saved/loaded --- src/pyk/kcfg/show.py | 10 ---------- src/pyk/proof/proof.py | 4 ++++ src/pyk/proof/reachability.py | 8 ++++++++ src/pyk/proof/show.py | 2 ++ 4 files changed, 14 insertions(+), 10 deletions(-) diff --git a/src/pyk/kcfg/show.py b/src/pyk/kcfg/show.py index b485670d8..c6c25379b 100644 --- a/src/pyk/kcfg/show.py +++ b/src/pyk/kcfg/show.py @@ -283,16 +283,6 @@ def _sorted_init_nodes() -> tuple[list[KCFG.Node], list[KCFG.Node]]: init, _ = _sorted_init_nodes() - # print([node.id for node in kcfg.nodes]) - # print([node.id for node in processed_nodes]) - - # for node in kcfg.nodes: - # print(kcfg.is_root(node.id)) - # print(kcfg.is_leaf(node.id)) - # print('') - # - # print(init) - # while init: ret_lines.append(('unknown', [''])) _print_subgraph('', init[0], []) diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index f4d0558c5..f487c5d01 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -182,6 +182,10 @@ def failed(self) -> bool: def passed(self) -> bool: return self.status == ProofStatus.PASSED + @property + def is_pending(self) -> bool: + return self.status == ProofStatus.PENDING + @property def dict(self) -> dict[str, Any]: return { diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 535047143..b1328159e 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -294,6 +294,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRProof: kcfg = KCFG.read_cfg_data(cfg_dir, id) init = int(proof_dict['init']) target = int(proof_dict['target']) + subproof_nodes = proof_dict['subproof_nodes'] circularity = bool(proof_dict['circularity']) admitted = bool(proof_dict['admitted']) terminal = proof_dict['terminal'] @@ -307,6 +308,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRProof: terminal=terminal, init=init, target=target, + subproof_nodes=subproof_nodes, logs=logs, circularity=circularity, admitted=admitted, @@ -330,6 +332,7 @@ def write_proof_data(self) -> None: dct['type'] = 'APRProof' dct['init'] = self.kcfg._resolve(self.init) dct['target'] = self.kcfg._resolve(self.target) + dct['subproof_nodes'] = sorted(self.subproof_nodes) dct['terminal'] = sorted(self._terminal) dct['node_refutations'] = { self.kcfg._resolve(node_id): proof.id for (node_id, proof) in self.node_refutations.items() @@ -360,6 +363,7 @@ def __init__( bmc_depth: int, bounded: Iterable[int] | None = None, proof_dir: Path | None = None, + subproof_nodes: Iterable[int] | None = None, subproof_ids: Iterable[str] = (), node_refutations: dict[int, str] | None = None, circularity: bool = False, @@ -373,6 +377,7 @@ def __init__( target, logs, proof_dir=proof_dir, + subproof_nodes=subproof_nodes, subproof_ids=subproof_ids, node_refutations=node_refutations, circularity=circularity, @@ -390,6 +395,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRBMCProof: kcfg = KCFG.read_cfg_data(cfg_dir, id) init = int(proof_dict['init']) target = int(proof_dict['target']) + subproof_nodes = proof_dict['subproof_nodes'] circularity = bool(proof_dict['circularity']) terminal = proof_dict['terminal'] admitted = bool(proof_dict['admitted']) @@ -405,6 +411,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRBMCProof: terminal=terminal, init=init, target=target, + subproof_nodes=subproof_nodes, logs=logs, circularity=circularity, admitted=admitted, @@ -430,6 +437,7 @@ def write_proof_data(self) -> None: dct['type'] = 'APRBMCProof' dct['init'] = self.kcfg._resolve(self.init) dct['target'] = self.kcfg._resolve(self.target) + dct['subproof_nodes'] = sorted(self.subproof_nodes) dct['node_refutations'] = { self.kcfg._resolve(node_id): proof.id for (node_id, proof) in self.node_refutations.items() } diff --git a/src/pyk/proof/show.py b/src/pyk/proof/show.py index 20747610e..55ac591db 100644 --- a/src/pyk/proof/show.py +++ b/src/pyk/proof/show.py @@ -36,6 +36,8 @@ def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]: attrs.append('target') if self.proof.is_pending(node.id): attrs.append('pending') + if self.proof.is_subproof_node(node.id): + attrs.append('subproof') if self.proof.is_terminal(node.id): attrs.append('terminal') if 'stuck' in attrs: From 96285856d9bfdd62c547a210fe48732c226ff1be Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 18 Sep 2023 19:03:19 +0000 Subject: [PATCH 17/30] Set Version: 0.1.446 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index ba5a30436..8c0b74dcf 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.445 \ No newline at end of file +0.1.446 diff --git a/pyproject.toml b/pyproject.toml index e08017619..41d9fc234 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.445" +version = "0.1.446" description = "" authors = [ "Runtime Verification, Inc. ", From 11072b5addae0bc3481593d4c479cda9fd58bbd6 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 18 Sep 2023 18:30:37 -0500 Subject: [PATCH 18/30] Fix is_pending name conflict --- src/pyk/proof/proof.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index f487c5d01..df2a7a34d 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -183,7 +183,7 @@ def passed(self) -> bool: return self.status == ProofStatus.PASSED @property - def is_pending(self) -> bool: + def is_proof_pending(self) -> bool: return self.status == ProofStatus.PENDING @property From 286b04e04982cb56caf9e628a875ac046ab57929 Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Mon, 18 Sep 2023 18:37:12 -0500 Subject: [PATCH 19/30] Update src/pyk/kcfg/show.py --- src/pyk/kcfg/show.py | 1 - 1 file changed, 1 deletion(-) diff --git a/src/pyk/kcfg/show.py b/src/pyk/kcfg/show.py index c6c25379b..596bbcff8 100644 --- a/src/pyk/kcfg/show.py +++ b/src/pyk/kcfg/show.py @@ -282,7 +282,6 @@ def _sorted_init_nodes() -> tuple[list[KCFG.Node], list[KCFG.Node]]: return (init_nodes + init_leaf_nodes, remaining_nodes) init, _ = _sorted_init_nodes() - while init: ret_lines.append(('unknown', [''])) _print_subgraph('', init[0], []) From 88dfe83614d714a8998cd5760cd0098c7d4f9a63 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 18 Sep 2023 18:45:35 -0500 Subject: [PATCH 20/30] Fix formatting --- src/pyk/proof/reachability.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index b1328159e..5ccb2022b 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -3,7 +3,7 @@ import json import logging from dataclasses import dataclass -from typing import TYPE_CHECKING, Callable +from typing import TYPE_CHECKING from pyk.kore.rpc import LogEntry @@ -19,7 +19,7 @@ from .proof import CompositeSummary, Proof, ProofStatus if TYPE_CHECKING: - from collections.abc import Iterable, Mapping + from collections.abc import Callable, Iterable, Mapping from pathlib import Path from typing import Any, Final, TypeVar From 0d95e58bcfa01b5f71109194225769dd97a36425 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 18 Sep 2023 19:23:24 -0500 Subject: [PATCH 21/30] fix test --- src/tests/integration/kcfg/test_imp.py | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index 2280636eb..27c10df98 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -1261,6 +1261,7 @@ def test_delegate_to_subproof( claim, logs={}, proof_dir=proof_dir, + generate_subproof_name=(lambda proof, node_id: str(node_id)), ) prover = APRProver( From 2a99cfc791fc72a7d478152d0cc7005c32b88e25 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 20 Sep 2023 18:54:56 +0000 Subject: [PATCH 22/30] Set Version: 0.1.448 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 00c8b42f0..44516207b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.447 \ No newline at end of file +0.1.448 diff --git a/pyproject.toml b/pyproject.toml index 4bd4491d8..412c91ea1 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.447" +version = "0.1.448" description = "" authors = [ "Runtime Verification, Inc. ", From b4d0c8a15aa892220753041b42fbd8cf07ae5ba8 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 21 Sep 2023 10:21:47 -0500 Subject: [PATCH 23/30] Add generate_subproof_name to APRBMCProof --- src/pyk/proof/reachability.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 5ccb2022b..652de52a0 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -368,6 +368,7 @@ def __init__( node_refutations: dict[int, str] | None = None, circularity: bool = False, admitted: bool = False, + generate_subproof_name: Callable[[APRProof, int], str] | None = None, ): super().__init__( id, @@ -382,6 +383,7 @@ def __init__( node_refutations=node_refutations, circularity=circularity, admitted=admitted, + generate_subproof_name=generate_subproof_name, ) self.bmc_depth = bmc_depth self._bounded = set(bounded) if bounded is not None else set() From b63fe599c74938cff80c5a1fe52e460e6cab5a5e Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 22 Sep 2023 15:54:21 -0500 Subject: [PATCH 24/30] Make subproof loading more lazy --- src/pyk/proof/proof.py | 32 ++++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index df2a7a34d..0e6684e1d 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -33,9 +33,19 @@ class Proof(ABC): id: str proof_dir: Path | None - _subproofs: dict[str, Proof] + _subproofs: dict[str, Proof | None] admitted: bool + def get_subproof(self, proof_id: str) -> Proof: + if proof_id not in self._subproofs: + raise ValueError(f'subproof: {proof_id} not found in subproofs of {self.id}') + proof = self._subproofs[proof_id] + if proof is None: + proof = self.fetch_subproof_data(proof_id) + + assert isinstance(proof, Proof) + return proof + @property def proof_subdir(self) -> Path | None: if self.proof_dir is None: @@ -57,7 +67,7 @@ def __init__( raise ValueError(f'Cannot read subproofs {subproof_ids} of proof {self.id} with no proof_dir') if len(list(subproof_ids)) > 0: for proof_id in subproof_ids: - self.fetch_subproof_data(proof_id, force_reread=True) + self._subproofs[proof_id] = None if proof_dir is not None: ensure_dir_path(proof_dir) if self.proof_dir is not None: @@ -68,7 +78,7 @@ def admit(self) -> None: @property def subproof_ids(self) -> list[str]: - return [sp.id for sp in self._subproofs.values()] + return list(self._subproofs.keys()) def write_proof(self, subproofs: bool = False) -> None: if not self.proof_dir: @@ -136,29 +146,35 @@ def fetch_subproof( ) -> Proof: """Get a subproof, re-reading from disk if it's not up-to-date""" - if self.proof_dir is not None and (force_reread or not self._subproofs[proof_id].up_to_date): + if self.proof_dir is not None and (force_reread or not self.get_subproof(proof_id).up_to_date): updated_subproof = Proof.read_proof(proof_id, self.proof_dir) self._subproofs[proof_id] = updated_subproof return updated_subproof else: - return self._subproofs[proof_id] + return self.get_subproof(proof_id) def fetch_subproof_data( self, proof_id: str, force_reread: bool = False, uptodate_check_method: str = 'timestamp' ) -> Proof: """Get a subproof, re-reading from disk if it's not up-to-date""" - if self.proof_dir is not None and (force_reread or not self._subproofs[proof_id].up_to_date): + if self.proof_dir is not None and (force_reread or not self.get_subproof(proof_id).up_to_date): updated_subproof = Proof.read_proof_data(self.proof_dir, proof_id) self._subproofs[proof_id] = updated_subproof return updated_subproof else: - return self._subproofs[proof_id] + return self.get_subproof(proof_id) @property def subproofs(self) -> Iterable[Proof]: """Return the subproofs, re-reading from disk the ones that changed""" - return self._subproofs.values() + for subproof_id in self._subproofs.keys(): + self.fetch_subproof_data(subproof_id) + subproofs_all_loaded: list[Proof] = [] + for subproof in self._subproofs.values(): + assert subproof is not None + subproofs_all_loaded.append(subproof) + return subproofs_all_loaded @property def subproofs_status(self) -> ProofStatus: From c6e8aea8559b3c00a37cd91cd2d0fed42a97471f Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 22 Sep 2023 16:57:18 -0500 Subject: [PATCH 25/30] Fix infinite recursion --- src/pyk/proof/proof.py | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index 0e6684e1d..ca691c493 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -146,24 +146,32 @@ def fetch_subproof( ) -> Proof: """Get a subproof, re-reading from disk if it's not up-to-date""" - if self.proof_dir is not None and (force_reread or not self.get_subproof(proof_id).up_to_date): + assert self.proof_dir is not None + + subproof = self._subproofs[proof_id] + + if force_reread or subproof is None or subproof.up_to_date: updated_subproof = Proof.read_proof(proof_id, self.proof_dir) self._subproofs[proof_id] = updated_subproof return updated_subproof else: - return self.get_subproof(proof_id) + return subproof def fetch_subproof_data( self, proof_id: str, force_reread: bool = False, uptodate_check_method: str = 'timestamp' ) -> Proof: """Get a subproof, re-reading from disk if it's not up-to-date""" - if self.proof_dir is not None and (force_reread or not self.get_subproof(proof_id).up_to_date): + assert self.proof_dir is not None + + subproof = self._subproofs[proof_id] + + if force_reread or subproof is None or subproof.up_to_date: updated_subproof = Proof.read_proof_data(self.proof_dir, proof_id) self._subproofs[proof_id] = updated_subproof return updated_subproof else: - return self.get_subproof(proof_id) + return subproof @property def subproofs(self) -> Iterable[Proof]: From fe2849b3a92696967e94f5b82f3dc2df67d64392 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 22 Sep 2023 17:18:28 -0500 Subject: [PATCH 26/30] Fix _subproofs map key error --- src/pyk/proof/proof.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index ca691c493..0aa3fbde4 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -164,7 +164,7 @@ def fetch_subproof_data( assert self.proof_dir is not None - subproof = self._subproofs[proof_id] + subproof = self._subproofs[proof_id] if proof_id in self._subproofs else None if force_reread or subproof is None or subproof.up_to_date: updated_subproof = Proof.read_proof_data(self.proof_dir, proof_id) From fa20b9b206117a6d341e4d6ff8a0b024e5ce01ad Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 22 Sep 2023 17:53:50 -0500 Subject: [PATCH 27/30] Remove guard on create_node --- src/pyk/kcfg/kcfg.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index 143ce5361..a6b4bae32 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -459,8 +459,6 @@ def create_node(self, cterm: CTerm) -> Node: term = cterm.kast term = remove_source_attributes(term) cterm = CTerm.from_kast(term) - while self._node_id in self._nodes: - self._node_id += 1 node = KCFG.Node(self._node_id, cterm) self._node_id += 1 self._nodes[node.id] = node From a31554754f169b2cc6fb667e74e1a54c33c9048a Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 22 Sep 2023 17:55:07 -0500 Subject: [PATCH 28/30] readd guard on create_node --- src/pyk/kcfg/kcfg.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index a6b4bae32..143ce5361 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -459,6 +459,8 @@ def create_node(self, cterm: CTerm) -> Node: term = cterm.kast term = remove_source_attributes(term) cterm = CTerm.from_kast(term) + while self._node_id in self._nodes: + self._node_id += 1 node = KCFG.Node(self._node_id, cterm) self._node_id += 1 self._nodes[node.id] = node From 694f2a5178ac1bc71b1e7c6ed4f714a0be55368e Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 25 Sep 2023 17:19:44 +0000 Subject: [PATCH 29/30] Set Version: 0.1.449 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 44516207b..868227d78 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.448 +0.1.449 diff --git a/pyproject.toml b/pyproject.toml index 412c91ea1..a9928acb2 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.448" +version = "0.1.449" description = "" authors = [ "Runtime Verification, Inc. ", From 5c188fd416887d2f78aed097a396c5ffbdb2acc1 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 25 Sep 2023 12:21:47 -0500 Subject: [PATCH 30/30] Make add_node private --- src/pyk/kcfg/kcfg.py | 8 +++----- src/tests/unit/test_kcfg.py | 10 +++++----- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index 143ce5361..aa5426656 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -351,7 +351,7 @@ def from_dict(dct: Mapping[str, Any]) -> KCFG: max_id = max(max_id, node_id) cterm = CTerm.from_dict(node_dict['cterm']) node = KCFG.Node(node_id, cterm) - cfg.add_node(node) + cfg._add_node(node) cfg._node_id = dct.get('next', max_id + 1) @@ -449,7 +449,7 @@ def get_node(self, node_id: NodeIdLike) -> Node | None: def contains_node(self, node: Node) -> bool: return bool(self.get_node(node.id)) - def add_node(self, node: Node) -> None: + def _add_node(self, node: Node) -> None: if node.id in self._nodes: raise ValueError(f'Node with id already exists: {node.id}') self._nodes[node.id] = node @@ -459,8 +459,6 @@ def create_node(self, cterm: CTerm) -> Node: term = cterm.kast term = remove_source_attributes(term) cterm = CTerm.from_kast(term) - while self._node_id in self._nodes: - self._node_id += 1 node = KCFG.Node(self._node_id, cterm) self._node_id += 1 self._nodes[node.id] = node @@ -984,7 +982,7 @@ def read_cfg_data(cfg_dir: Path, id: str) -> KCFG: node_dict = json.loads(node_json.read_text()) cterm = CTerm.from_dict(node_dict['cterm']) node = KCFG.Node(node_id, cterm) - cfg.add_node(node) + cfg._add_node(node) cfg._node_id = dct.get('next', max_id + 1) diff --git a/src/tests/unit/test_kcfg.py b/src/tests/unit/test_kcfg.py index 7e4c10f6e..b5703c8f9 100644 --- a/src/tests/unit/test_kcfg.py +++ b/src/tests/unit/test_kcfg.py @@ -435,9 +435,9 @@ def delete_node_data(node_id: int) -> None: monkeypatch.setattr(kcfg, '_write_node_data', write_node_data) monkeypatch.setattr(kcfg, '_delete_node_data', delete_node_data) - kcfg.add_node(node(1)) - kcfg.add_node(node(2)) - kcfg.add_node(node(3)) + kcfg._add_node(node(1)) + kcfg._add_node(node(2)) + kcfg._add_node(node(3)) assert written_nodes == set() assert deleted_nodes == set() @@ -449,11 +449,11 @@ def delete_node_data(node_id: int) -> None: written_nodes.clear() - kcfg.add_node(node(4)) + kcfg._add_node(node(4)) kcfg.remove_node(1) kcfg.remove_node(2) kcfg.replace_node(3, node(3).cterm) - kcfg.add_node(node(2)) + kcfg._add_node(node(2)) assert written_nodes == set() assert deleted_nodes == set()