Attribute checking on node insertion

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.779'
-release = '0.1.779'
+version = '0.1.780'
+release = '0.1.780'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.779
+0.1.780

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.779"
+version = "0.1.780"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/kcfg/exploration.py

@@ -18,8 +18,12 @@ class KCFGExplorationNodeAttr(NodeAttr):
 class KCFGExploration:
     kcfg: KCFG
 
+    def check_terminal(self, node: KCFG.Node) -> bool:
+        return self.kcfg_semantics.is_terminal(node.cterm)
+
     def __init__(self, kcfg: KCFG, terminal: Iterable[NodeIdLike] | None = None) -> None:
         self.kcfg = kcfg
+        self.kcfg._attribute_checkers[KCFGExplorationNodeAttr.TERMINAL] = self.check_terminal
         if terminal:
             for node_id in terminal:
                 self.add_terminal(node_id)

src/pyk/kcfg/kcfg.py

@@ -148,7 +148,7 @@ def remove_attr(self, attr: NodeAttr) -> KCFG.Node:
         def discard_attr(self, attr: NodeAttr) -> KCFG.Node:
             return KCFG.Node(self.id, self.cterm, self.attrs.difference([attr]))
 
-        def let(self, cterm: CTerm | None = None, attrs: Iterable[KCFGNodeAttr] | None = None) -> KCFG.Node:
+        def let(self, cterm: CTerm | None = None, attrs: Iterable[NodeAttr] | None = None) -> KCFG.Node:
             new_cterm = cterm if cterm is not None else self.cterm
             new_attrs = attrs if attrs is not None else self.attrs
             return KCFG.Node(self.id, new_cterm, new_attrs)
@@ -401,6 +401,8 @@ def replace_target(self, node: KCFG.Node) -> KCFG.NDBranch:
 
     _kcfg_store: KCFGStore | None
 
+    _attribute_checkers: dict[NodeAttr, Callable[[KCFG.Node], bool]]
+
     def __init__(self, cfg_dir: Path | None = None, optimize_memory: bool = True) -> None:
         self._node_id = 1
         if optimize_memory:
@@ -417,9 +419,22 @@ def __init__(self, cfg_dir: Path | None = None, optimize_memory: bool = True) ->
         self._ndbranches = {}
         self._aliases = {}
         self._lock = RLock()
+        self._attribute_checkers = {}
+        self._attribute_checkers[KCFGNodeAttr.STUCK] = self.check_stuck
+        self._attribute_checkers[KCFGNodeAttr.VACUOUS] = self.check_vacuous
         if cfg_dir is not None:
             self._kcfg_store = KCFGStore(cfg_dir)
 
+    def check_stuck(self, node: KCFG.Node) -> bool:
+        if self.get_node(node.id) is None:
+            return False
+        return self.is_stuck(node.id)
+
+    def check_vacuous(self, node: KCFG.Node) -> bool:
+        if self.get_node(node.id) is None:
+            return False
+        return self.is_vacuous(node.id)
+
     def __contains__(self, item: object) -> bool:
         if type(item) is KCFG.Node:
             return self.contains_node(item)
@@ -657,15 +672,20 @@ def contains_node(self, node: KCFG.Node) -> bool:
     def add_node(self, node: KCFG.Node) -> None:
         if node.id in self._nodes:
             raise ValueError(f'Node with id already exists: {node.id}')
-        self._nodes[node.id] = node
-        self._created_nodes.add(node.id)
+        self.replace_node(node)
 
     def create_node(self, cterm: CTerm) -> KCFG.Node:
         node = KCFG.Node(self._node_id, cterm)
         self._node_id += 1
-        self._nodes[node.id] = node
-        self._created_nodes.add(node.id)
+        self.replace_node(node)
         return node
+
+    def get_node_attrs(self, node: KCFG.Node) -> Iterable[NodeAttr]:
+        attrs = []
+        for attr, checker in self._attribute_checkers.items():
+            if checker(node):
+                attrs.append(attr)
+        return attrs
 
     def remove_node(self, node_id: NodeIdLike) -> None:
         node_id = self._resolve(node_id)
@@ -723,13 +743,14 @@ def add_attr(self, node_id: NodeIdLike, attr: NodeAttr) -> None:
         self.replace_node(new_node)
 
     def let_node(
-        self, node_id: NodeIdLike, cterm: CTerm | None = None, attrs: Iterable[KCFGNodeAttr] | None = None
+        self, node_id: NodeIdLike, cterm: CTerm | None = None, attrs: Iterable[NodeAttr] | None = None
     ) -> None:
         node = self.node(node_id)
         new_node = node.let(cterm=cterm, attrs=attrs)
         self.replace_node(new_node)
 
     def replace_node(self, node: KCFG.Node) -> None:
+        node = node.let(attrs=self.get_node_attrs(node))
         self._nodes[node.id] = node
         self._created_nodes.add(node.id)
         self._update_refs(node.id)

src/tests/integration/proof/test_imp.py

@@ -1057,8 +1057,8 @@ def test_failure_info_recomputed_on_proof_reinit(
         proof_dir: Path,
         fail_fast: bool,
     ) -> None:
-        if fail_fast:
-            pytest.skip()
+#          if fail_fast:
+#              pytest.skip()
 
         claim = single(
             kprove.get_claims(Path(spec_file), spec_module_name=spec_module, claim_labels=[f'{spec_module}.{claim_id}'])
@@ -1070,6 +1070,12 @@ def test_failure_info_recomputed_on_proof_reinit(
         prover = APRProver(proof, kcfg_explore=kcfg_explore)
         prover.advance_proof()
 
+        failure_info = proof.failure_info
+        assert isinstance(failure_info, APRFailureInfo)
+
+        actual_pending = len(failure_info.pending_nodes)
+        actual_failing = len(failure_info.failing_nodes)
+
         # reload proof from disk
         proof = APRProof.read_proof_data(proof_dir, proof_id)
         prover = APRProver(proof, kcfg_explore=kcfg_explore)
@@ -1173,6 +1179,7 @@ def test_fail_fast(
         assert len(proof.terminal_ids) == 2
         assert len(proof.failing) == 1
 
+
     def test_anti_unify_forget_values(
         self,
         kcfg_explore: KCFGExplore,