Adding is-loop functionality (#4650)

This PR adds a recogniser function for loops to the KCFG semantics. This
allows us to avoid unnecessary KCFG traversal computation in the cases
when the node examined is not a loop head. This computation turned out
to be quite expensive in real-world proofs with a high branching factor.

pyk/src/pyk/kcfg/semantics.py

@@ -19,6 +19,11 @@ def abstract_node(self, c: CTerm) -> CTerm: ...
 
     """Implement an abstraction mechanism."""
 
+    @abstractmethod
+    def is_loop(self, c: CTerm) -> bool: ...
+
+    """Check whether or not the given ``CTerm`` represents a loop head."""
+
     @abstractmethod
     def same_loop(self, c1: CTerm, c2: CTerm) -> bool: ...
 
@@ -47,6 +52,9 @@ def is_terminal(self, c: CTerm) -> bool:
     def abstract_node(self, c: CTerm) -> CTerm:
         return c
 
+    def is_loop(self, c: CTerm) -> bool:
+        return False
+
     def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         return False
 

pyk/src/pyk/proof/reachability.py

@@ -786,7 +786,7 @@ def _check_subsume(self, node: KCFG.Node, target_node: KCFG.Node, proof_id: str)
     def step_proof(self, step: APRProofStep) -> list[APRProofResult]:
         # Check if the current node should be bounded
         prior_loops: tuple[int, ...] = ()
-        if step.bmc_depth is not None:
+        if step.bmc_depth is not None and 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:

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

@@ -52,10 +52,19 @@ def is_terminal(self, c: CTerm) -> bool:
     def abstract_node(self, c: CTerm) -> CTerm:
         return c
 
+    def is_loop(self, c: CTerm) -> bool:
+        k_cell = c.cell('K_CELL')
+        return (
+            type(k_cell) is KSequence
+            and type(k_cell[0]) is KApply
+            and len(k_cell) > 0
+            and k_cell[0].label.name == 'while(_)_'
+        )
+
     def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         k_cell_1 = c1.cell('K_CELL')
         k_cell_2 = c2.cell('K_CELL')
-        if k_cell_1 == k_cell_2 and type(k_cell_1) is KSequence and type(k_cell_1[0]) is KApply:
+        if k_cell_1 == k_cell_2 and type(k_cell_1) is KSequence and len(k_cell_1) > 0 and type(k_cell_1[0]) is KApply:
             return k_cell_1[0].label.name == 'while(_)_'
         return False
 

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

@@ -58,18 +58,6 @@ def is_terminal(self, c: CTerm) -> bool:
             return True
         return False
 
-    def abstract_node(self, c: CTerm) -> CTerm:
-        return c
-
-    def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
-        return False
-
-    def can_make_custom_step(self, c: CTerm) -> bool:
-        return False
-
-    def custom_step(self, c: CTerm) -> KCFGExtendResult | None:
-        return None
-
 
 class CustomStepSemanticsWithStep(CustomStepSemanticsWithoutStep):
     def can_make_custom_step(self, c: CTerm) -> bool:

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

@@ -23,19 +23,21 @@
     from pyk.cterm import CTerm
     from pyk.kast.outer import KDefinition
     from pyk.kcfg import KCFGExplore
-    from pyk.kcfg.kcfg import KCFGExtendResult
     from pyk.kcfg.semantics import KCFGSemantics
     from pyk.ktool.kprove import KProve
 
 _LOGGER: Final = logging.getLogger(__name__)
 
 
 class GotoSemantics(DefaultSemantics):
-    def is_terminal(self, c: CTerm) -> bool:
-        return False
-
-    def abstract_node(self, c: CTerm) -> CTerm:
-        return c
+    def is_loop(self, c: CTerm) -> bool:
+        k_cell = c.cell('K_CELL')
+        return (
+            type(k_cell) is KSequence
+            and len(k_cell) > 0
+            and type(k_cell[0]) is KApply
+            and k_cell[0].label.name == 'jumpi'
+        )
 
     def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         k_cell = c1.cell('K_CELL')
@@ -45,12 +47,6 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
             return k_cell[0].label.name == 'jumpi'
         return False
 
-    def can_make_custom_step(self, c: CTerm) -> bool:
-        return False
-
-    def custom_step(self, c: CTerm) -> KCFGExtendResult | None:
-        return None
-
 
 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

@@ -33,7 +33,6 @@
     from pyk.kast.inner import KInner
     from pyk.kast.outer import KDefinition
     from pyk.kcfg import KCFGExplore
-    from pyk.kcfg.kcfg import KCFGExtendResult
     from pyk.kcfg.semantics import KCFGSemantics
     from pyk.ktool.kprint import KPrint, SymbolTable
     from pyk.ktool.kprove import KProve
@@ -65,22 +64,22 @@ def is_terminal(self, c: CTerm) -> bool:
             return True
         return False
 
-    def abstract_node(self, c: CTerm) -> CTerm:
-        return c
+    def is_loop(self, c: CTerm) -> bool:
+        k_cell = c.cell('K_CELL')
+        return (
+            type(k_cell) is KSequence
+            and len(k_cell) > 0
+            and type(k_cell[0]) is KApply
+            and k_cell[0].label.name == 'while(_)_'
+        )
 
     def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         k_cell_1 = c1.cell('K_CELL')
         k_cell_2 = c2.cell('K_CELL')
-        if k_cell_1 == k_cell_2 and type(k_cell_1) is KSequence and type(k_cell_1[0]) is KApply:
+        if k_cell_1 == k_cell_2 and type(k_cell_1) is KSequence and len(k_cell_1) > 0 and type(k_cell_1[0]) is KApply:
             return k_cell_1[0].label.name == 'while(_)_'
         return False
 
-    def can_make_custom_step(self, c: CTerm) -> bool:
-        return False
-
-    def custom_step(self, c: CTerm) -> KCFGExtendResult | None:
-        return None
-
 
 EMPTY_STATES: Final[list[tuple[str, str]]] = []
 EXECUTE_TEST_DATA: Final = (

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

@@ -30,7 +30,6 @@
     from pyk.kast.inner import KInner
     from pyk.kast.outer import KDefinition
     from pyk.kcfg import KCFGExplore
-    from pyk.kcfg.kcfg import KCFGExtendResult
     from pyk.kcfg.semantics import KCFGSemantics
     from pyk.ktool.kprove import KProve
 
@@ -59,18 +58,6 @@ def is_terminal(self, c: CTerm) -> bool:
             return True
         return False
 
-    def abstract_node(self, c: CTerm) -> CTerm:
-        return c
-
-    def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
-        return False
-
-    def can_make_custom_step(self, c: CTerm) -> bool:
-        return False
-
-    def custom_step(self, c: CTerm) -> KCFGExtendResult | None:
-        return None
-
 
 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

@@ -17,7 +17,6 @@
     from pyk.cterm import CTerm
     from pyk.kast.outer import KDefinition
     from pyk.kcfg import KCFGExplore
-    from pyk.kcfg.kcfg import KCFGExtendResult
     from pyk.kcfg.semantics import KCFGSemantics
     from pyk.ktool.kprove import KProve
 
@@ -31,18 +30,6 @@ def is_terminal(self, c: CTerm) -> bool:
             return True
         return False
 
-    def abstract_node(self, c: CTerm) -> CTerm:
-        return c
-
-    def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
-        return False
-
-    def can_make_custom_step(self, c: CTerm) -> bool:
-        return False
-
-    def custom_step(self, c: CTerm) -> KCFGExtendResult | None:
-        return None
-
 
 class TestSimpleProof(KCFGExploreTest, KProveTest):
     KOMPILE_MAIN_FILE = K_FILES / 'simple-proofs.k'