Skip to content

Commit

Permalink
Add is_loop predicate to KCFGSemantics and derived classes
Browse files Browse the repository at this point in the history
  • Loading branch information
nwatson22 committed May 8, 2024
1 parent 313aaba commit e8cff33
Show file tree
Hide file tree
Showing 7 changed files with 36 additions and 5 deletions.
6 changes: 6 additions & 0 deletions pyk/src/pyk/kcfg/semantics.py
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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
11 changes: 6 additions & 5 deletions pyk/src/pyk/proof/reachability.py
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
6 changes: 6 additions & 0 deletions pyk/src/tests/integration/ktool/test_imp.py
Original file line number Diff line number Diff line change
Expand Up @@ -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]] = (
(
Expand Down
6 changes: 6 additions & 0 deletions pyk/src/tests/integration/proof/test_goto.py
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
6 changes: 6 additions & 0 deletions pyk/src/tests/integration/proof/test_imp.py
Original file line number Diff line number Diff line change
Expand Up @@ -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 = (
Expand Down
3 changes: 3 additions & 0 deletions pyk/src/tests/integration/proof/test_refute_node.py
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down
3 changes: 3 additions & 0 deletions pyk/src/tests/integration/proof/test_simple.py
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down

0 comments on commit e8cff33

Please sign in to comment.