From bd4ef0def3742ad3a98ba285293efcf610a0422f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Mon, 28 Aug 2023 17:04:18 +0200 Subject: [PATCH] Fixing incorrect removal of terminal nodes (https://github.com/runtimeverification/pyk/pull/626) This PR corrects an error that occurs when pruning a node from the `kcfg` - the node would be removed and *then* its `id` would be resolved, causing said error. --------- Co-authored-by: devops --- pyk/package/version | 2 +- pyk/pyproject.toml | 2 +- pyk/src/pyk/kcfg/exploration.py | 5 +++-- pyk/src/pyk/proof/reachability.py | 10 +++++++--- 4 files changed, 12 insertions(+), 7 deletions(-) diff --git a/pyk/package/version b/pyk/package/version index ae6c98f0772..74ef6681c10 100644 --- a/pyk/package/version +++ b/pyk/package/version @@ -1 +1 @@ -0.1.429 +0.1.430 diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index a583cf03a62..f33ea1870fa 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.429" +version = "0.1.430" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/pyk/src/pyk/kcfg/exploration.py b/pyk/src/pyk/kcfg/exploration.py index f86f9405f63..c10ce46aadf 100644 --- a/pyk/src/pyk/kcfg/exploration.py +++ b/pyk/src/pyk/kcfg/exploration.py @@ -54,8 +54,8 @@ def add_terminal(self, node_id: NodeIdLike) -> None: self._terminal.add(self.kcfg._resolve(node_id)) # Unmarking a given node as terminal - def remove_terminal(self, node_id: NodeIdLike) -> None: - self._terminal.discard(self.kcfg._resolve(node_id)) + def remove_terminal(self, node_id: int) -> None: + self._terminal.discard(node_id) # # Lifted KCFG functions that may affect terminal nodes @@ -63,6 +63,7 @@ def remove_terminal(self, node_id: NodeIdLike) -> None: # Removing a given node def remove_node(self, node_id: NodeIdLike) -> None: + node_id = self.kcfg._resolve(node_id) self.kcfg.remove_node(node_id) self.remove_terminal(node_id) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index ddbedb03d1d..3a20026a534 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -122,6 +122,10 @@ def shortest_path_to(self, node_id: NodeIdLike) -> tuple[KCFG.Successor, ...]: assert spb is not None return spb + def prune(self, node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) -> list[int]: + pruned_nodes = super().prune(node_id, keep_nodes=list(keep_nodes) + [self.init, self.target]) + return pruned_nodes + @staticmethod def read_proof(id: str, proof_dir: Path) -> APRProof: proof_path = proof_dir / f'{hash_str(id)}.json' @@ -427,7 +431,7 @@ def is_failing(self, node_id: NodeIdLike) -> bool: return super().is_failing(node_id) and not self.is_bounded(node_id) def prune(self, node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) -> list[int]: - pruned_nodes = self.prune(node_id, keep_nodes=keep_nodes) + pruned_nodes = super().prune(node_id, keep_nodes=keep_nodes) for nid in pruned_nodes: self.remove_bounded(nid) return pruned_nodes @@ -495,8 +499,8 @@ def from_claim_with_bmc_depth( def add_bounded(self, nid: NodeIdLike) -> None: self._bounded.add(self.kcfg._resolve(nid)) - def remove_bounded(self, node_id: NodeIdLike) -> None: - self._bounded.discard(self.kcfg._resolve(node_id)) + def remove_bounded(self, node_id: int) -> None: + self._bounded.discard(node_id) @property def summary(self) -> CompositeSummary: