diff --git a/pyk/src/pyk/kcfg/semantics.py b/pyk/src/pyk/kcfg/semantics.py index 629f259b79..d705324fc6 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/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 diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 98b96f5a33..33356783cb 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/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: diff --git a/pyk/src/tests/integration/ktool/test_imp.py b/pyk/src/tests/integration/ktool/test_imp.py index 0593db69eb..f71c737a9d 100644 --- a/pyk/src/tests/integration/ktool/test_imp.py +++ b/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 diff --git a/pyk/src/tests/integration/proof/test_custom_step.py b/pyk/src/tests/integration/proof/test_custom_step.py index c8d1f1ad90..e5995de49f 100644 --- a/pyk/src/tests/integration/proof/test_custom_step.py +++ b/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: diff --git a/pyk/src/tests/integration/proof/test_goto.py b/pyk/src/tests/integration/proof/test_goto.py index 25e7ce55c4..ce1cf03c41 100644 --- a/pyk/src/tests/integration/proof/test_goto.py +++ b/pyk/src/tests/integration/proof/test_goto.py @@ -23,7 +23,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,11 +30,14 @@ 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] diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 2b63e3b069..a5231d43bd 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/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 = ( diff --git a/pyk/src/tests/integration/proof/test_refute_node.py b/pyk/src/tests/integration/proof/test_refute_node.py index c5d10f5634..e43e6f673e 100644 --- a/pyk/src/tests/integration/proof/test_refute_node.py +++ b/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), diff --git a/pyk/src/tests/integration/proof/test_simple.py b/pyk/src/tests/integration/proof/test_simple.py index 96a72e7153..2c307e6a6f 100644 --- a/pyk/src/tests/integration/proof/test_simple.py +++ b/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'