Add is_loop predicate to KCFGSemantics and derived classes

pyk/src/pyk/kcfg/semantics.py

@@ -17,6 +17,9 @@ def abstract_node(self, c: CTerm) -> CTerm: ...
     @abstractmethod
     def same_loop(self, c1: CTerm, c2: CTerm) -> bool: ...
 
+    @abstractmethod
+    def is_loop(self, c1: CTerm) -> bool: ...
+
 
 class DefaultSemantics(KCFGSemantics):
     def is_terminal(self, c: CTerm) -> bool:
@@ -27,3 +30,6 @@ def abstract_node(self, c: CTerm) -> CTerm:
 
     def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         return False
+
+    def is_loop(self, c1: CTerm) -> bool:
+        return False

pyk/src/pyk/proof/reachability.py

@@ -743,11 +743,12 @@ def _check_subsume(self, node: KCFG.Node, target_node: KCFG.Node, proof_id: str)
     def step_proof(self, step: APRProofStep) -> list[APRProofResult]:
         prior_loops: tuple[int, ...] = ()
         if step.bmc_depth is not None:
-            for node in step.shortest_path_to_node:
-                if self.kcfg_explore.kcfg_semantics.same_loop(node.cterm, step.node.cterm):
-                    if node.id in step.prior_loops_cache:
-                        prior_loops = step.prior_loops_cache[node.id] + (node.id,)
-                        break
+            if self.kcfg_explore.kcfg_semantics.is_loop(step.node.cterm):
+                for node in step.shortest_path_to_node:
+                    if self.kcfg_explore.kcfg_semantics.same_loop(node.cterm, step.node.cterm):
+                        if node.id in step.prior_loops_cache:
+                            prior_loops = step.prior_loops_cache[node.id] + (node.id,)
+                            break
 
             _LOGGER.info(f'Prior loop heads for node {step.node.id}: {(step.node.id, prior_loops)}')
             if len(prior_loops) > step.bmc_depth:

pyk/src/tests/integration/ktool/test_imp.py

@@ -57,6 +57,12 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
             return k_cell_1[0].label.name == 'while(_)_'
         return False
 
+    def is_loop(self, c1: CTerm) -> bool:
+        k_cell_1 = c1.cell('K_CELL')
+        if type(k_cell_1) is KSequence and type(k_cell_1[0]) is KApply:
+            return k_cell_1[0].label.name == 'while(_)_'
+        return False
+
 
 PROVE_TEST_DATA: Iterable[tuple[str, Path, str, str, ProofStatus]] = (
     (

pyk/src/tests/integration/proof/test_goto.py

@@ -43,6 +43,12 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
             return k_cell[0].label.name == 'jumpi'
         return False
 
+    def is_loop(self, c1: CTerm) -> bool:
+        k_cell = c1.cell('K_CELL')
+        if type(k_cell) is KSequence and len(k_cell) > 0 and type(k_cell[0]) is KApply:
+            return k_cell[0].label.name == 'jumpi'
+        return False
+
 
 APRBMC_PROVE_TEST_DATA: Iterable[
     tuple[str, Path, str, str, int | None, int | None, int, Iterable[str], Iterable[str], ProofStatus, int]

pyk/src/tests/integration/proof/test_imp.py

@@ -73,6 +73,12 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
             return k_cell_1[0].label.name == 'while(_)_'
         return False
 
+    def is_loop(self, c1: CTerm) -> bool:
+        k_cell_1 = c1.cell('K_CELL')
+        if type(k_cell_1) is KSequence and type(k_cell_1[0]) is KApply:
+            return k_cell_1[0].label.name == 'while(_)_'
+        return False
+
 
 EMPTY_STATES: Final[list[tuple[str, str]]] = []
 EXECUTE_TEST_DATA: Final = (

pyk/src/tests/integration/proof/test_refute_node.py

@@ -62,6 +62,9 @@ def abstract_node(self, c: CTerm) -> CTerm:
     def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         return False
 
+    def is_loop(self, c1: CTerm) -> bool:
+        return False
+
 
 REFUTE_NODE_TEST_DATA: Iterable[tuple[str, Iterable[KInner], ProofStatus]] = (
     ('refute-node-fail', (leInt(KVariable('N'), intToken(0)),), ProofStatus.FAILED),

pyk/src/tests/integration/proof/test_simple.py

@@ -35,6 +35,9 @@ def abstract_node(self, c: CTerm) -> CTerm:
     def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         return False
 
+    def is_loop(self, c1: CTerm) -> bool:
+        return False
+
 
 class TestSimpleProof(KCFGExploreTest, KProveTest):
     KOMPILE_MAIN_FILE = K_FILES / 'simple-proofs.k'