From e8cff33e40b10081a78e0c7f63f5174e3623b61e Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 8 May 2024 17:51:28 -0500 Subject: [PATCH] Add is_loop predicate to KCFGSemantics and derived classes --- pyk/src/pyk/kcfg/semantics.py | 6 ++++++ pyk/src/pyk/proof/reachability.py | 11 ++++++----- pyk/src/tests/integration/ktool/test_imp.py | 6 ++++++ pyk/src/tests/integration/proof/test_goto.py | 6 ++++++ pyk/src/tests/integration/proof/test_imp.py | 6 ++++++ pyk/src/tests/integration/proof/test_refute_node.py | 3 +++ pyk/src/tests/integration/proof/test_simple.py | 3 +++ 7 files changed, 36 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/kcfg/semantics.py b/pyk/src/pyk/kcfg/semantics.py index 97ed43b4568..3be59ab4ea7 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/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 diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 87067794955..f86324127c0 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/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: diff --git a/pyk/src/tests/integration/ktool/test_imp.py b/pyk/src/tests/integration/ktool/test_imp.py index a3828f7a69d..4f039096d4f 100644 --- a/pyk/src/tests/integration/ktool/test_imp.py +++ b/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]] = ( ( diff --git a/pyk/src/tests/integration/proof/test_goto.py b/pyk/src/tests/integration/proof/test_goto.py index a643c93231c..66a4cf21b9f 100644 --- a/pyk/src/tests/integration/proof/test_goto.py +++ b/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] diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index d2f40148626..bf89d36db5d 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/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 = ( diff --git a/pyk/src/tests/integration/proof/test_refute_node.py b/pyk/src/tests/integration/proof/test_refute_node.py index c2c3801b0f7..132344eaf49 100644 --- a/pyk/src/tests/integration/proof/test_refute_node.py +++ b/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), diff --git a/pyk/src/tests/integration/proof/test_simple.py b/pyk/src/tests/integration/proof/test_simple.py index 273f807fd8f..510a786ce08 100644 --- a/pyk/src/tests/integration/proof/test_simple.py +++ b/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'