From 5630763157e2fe0375618f6cdd9e834b94783f77 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 15 Aug 2024 13:10:22 +0200 Subject: [PATCH 01/29] different approach --- pyk/src/pyk/kcfg/explore.py | 45 ++++++++++--------- pyk/src/pyk/proof/reachability.py | 40 +++++++++++------ .../tests/unit/test-data/pyk_toml_test.toml | 2 +- 3 files changed, 52 insertions(+), 35 deletions(-) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 69a02c07b0f..c7c3f2da8c2 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -218,19 +218,20 @@ def extend_cterm( cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), module_name: str | None = None, - ) -> KCFGExtendResult: + ) -> list[KCFGExtendResult]: + def log(message: str, *, warning: bool = False) -> None: _LOGGER.log(logging.WARNING if warning else logging.INFO, f'Extend result for {self.id}: {message}') custom_step_result = self.kcfg_semantics.custom_step(_cterm) if custom_step_result is not None: log(f'custom step node: {node_id}') - return custom_step_result + return [custom_step_result] abstract_cterm = self.kcfg_semantics.abstract_node(_cterm) if _cterm != abstract_cterm: log(f'abstraction node: {node_id}') - return Abstract(abstract_cterm) + return [Abstract(abstract_cterm)] cterm, next_states, depth, vacuous, next_node_logs = self.cterm_symbolic.execute( _cterm, @@ -240,33 +241,35 @@ def log(message: str, *, warning: bool = False) -> None: module_name=module_name, ) + extend_results: list[KCFGExtendResult] = [] + # Basic block if depth > 0: log(f'basic block at depth {depth}: {node_id}') - return Step(cterm, depth, next_node_logs, self._extract_rule_labels(next_node_logs)) + extend_results.append(Step(cterm, depth, next_node_logs, self._extract_rule_labels(next_node_logs))) # Stuck or vacuous if not next_states: if vacuous: log(f'vacuous node: {node_id}', warning=True) - return Vacuous() - log(f'stuck node: {node_id}') - return Stuck() - + extend_results.append(Vacuous()) + else: + log(f'stuck node: {node_id}') + extend_results.append(Stuck()) # Cut rule - if len(next_states) == 1: + elif len(next_states) == 1: log(f'cut-rule basic block at depth {depth}: {node_id}') - return Step( - next_states[0].state, - 1, - next_node_logs, - self._extract_rule_labels(next_node_logs), - cut=True, + extend_results.append( + Step( + next_states[0].state, + 1, + next_node_logs, + self._extract_rule_labels(next_node_logs), + cut=True, + ) ) - # Branch - assert len(next_states) > 1 - if all(branch_constraint for _, branch_constraint in next_states): + elif all(branch_constraint for _, branch_constraint in next_states): branch_preds = [flatten_label('#And', not_none(rule_predicate)) for _, rule_predicate in next_states] common_preds = list( unique( @@ -283,9 +286,11 @@ def log(message: str, *, warning: bool = False) -> None: ) constraint_strs = [self.pretty_print(ml_pred_to_bool(bc)) for bc in branches] log(f'{len(branches)} branches: {node_id} -> {constraint_strs}') - return Branch(branches) + extend_results.append(Branch(branches)) else: # NDBranch log(f'{len(next_states)} non-deterministic branches: {node_id}') next_cterms = [cterm for cterm, _ in next_states] - return NDBranch(next_cterms, next_node_logs, self._extract_rule_labels(next_node_logs)) + extend_results.append(NDBranch(next_cterms, next_node_logs, self._extract_rule_labels(next_node_logs))) + + return extend_results diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 58c9bb24df0..2fa71be8298 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -188,14 +188,14 @@ def get_steps(self) -> list[APRProofStep]: def commit(self, result: APRProofResult) -> None: self.prior_loops_cache[result.node_id] = result.prior_loops_cache_update - if isinstance(result, APRProofExtendResult): - self.kcfg.extend(result.extend_result, self.kcfg.node(result.node_id), logs=self.logs) - elif isinstance(result, APRProofSubsumeResult): - self.kcfg.create_cover(result.node_id, self.target, csubst=result.csubst) + if isinstance(result, APRProofBoundedResult): + self.add_bounded(result.node_id) elif isinstance(result, APRProofTerminalResult): self.add_terminal(result.node_id) - elif isinstance(result, APRProofBoundedResult): - self.add_bounded(result.node_id) + elif isinstance(result, APRProofSubsumeResult): + self.kcfg.create_cover(result.node_id, self.target, csubst=result.csubst) + elif isinstance(result, APRProofExtendResult): + self.kcfg.extend(result.extend_result, self.kcfg.node(result.node_id), logs=self.logs) else: raise ValueError(f'Incorrect result type, expected APRProofResult: {result}') @@ -674,6 +674,7 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]): direct_subproof_rules: bool assume_defined: bool kcfg_explore: KCFGExplore + next_steps: dict[NodeIdLike, KCFGExtendResult] def __init__( self, @@ -698,6 +699,7 @@ def __init__( self.fast_check_subsumption = fast_check_subsumption self.direct_subproof_rules = direct_subproof_rules self.assume_defined = assume_defined + self.next_steps = {} def close(self) -> None: self.kcfg_explore.cterm_symbolic._kore_client.close() @@ -793,14 +795,24 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: if step.circularity and not step.nonzero_depth and (execute_depth is None or execute_depth > 1): execute_depth = 1 - extend_result = self.kcfg_explore.extend_cterm( - step.node.cterm, - execute_depth=execute_depth, - cut_point_rules=cut_rules, - terminal_rules=self.terminal_rules, - module_name=step.module_name, - node_id=step.node.id, - ) + if step.node.id in self.next_steps: + extend_results = [self.next_steps.pop(step.node.id)] + else: + extend_results = self.kcfg_explore.extend_cterm( + step.node.cterm, + execute_depth=execute_depth, + cut_point_rules=cut_rules, + terminal_rules=self.terminal_rules, + module_name=step.module_name, + node_id=step.node.id, + ) + + assert len(extend_results) == 1 or len(extend_results) == 2 + extend_result = extend_results[0] + if len(extend_results) == 2: + assert step.node.id not in self.next_steps + self.next_steps[step.node.id] = extend_results[1] + return [ APRProofExtendResult( node_id=step.node.id, extend_result=extend_result, prior_loops_cache_update=prior_loops diff --git a/pyk/src/tests/unit/test-data/pyk_toml_test.toml b/pyk/src/tests/unit/test-data/pyk_toml_test.toml index 9919e16f378..74b5870db45 100644 --- a/pyk/src/tests/unit/test-data/pyk_toml_test.toml +++ b/pyk/src/tests/unit/test-data/pyk_toml_test.toml @@ -1,6 +1,6 @@ [coverage] output = "default-file" -definition = "/tmp" +definition = "/var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T" [print] input = "kast-json" From 6ff9f374cf31980c58b95f40950cb5726f6154ee Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 15 Aug 2024 13:16:09 +0200 Subject: [PATCH 02/29] no changes to .toml --- pyk/src/tests/unit/test-data/pyk_toml_test.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/tests/unit/test-data/pyk_toml_test.toml b/pyk/src/tests/unit/test-data/pyk_toml_test.toml index 74b5870db45..9919e16f378 100644 --- a/pyk/src/tests/unit/test-data/pyk_toml_test.toml +++ b/pyk/src/tests/unit/test-data/pyk_toml_test.toml @@ -1,6 +1,6 @@ [coverage] output = "default-file" -definition = "/var/folders/ks/1p8zyp5j7xz_v1krhl4l17tm0000gn/T" +definition = "/tmp" [print] input = "kast-json" From cb9e98c80eeaf0b4cbdb7e505c108831f430dcd5 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 15 Aug 2024 13:19:59 +0200 Subject: [PATCH 03/29] reverting changes --- pyk/src/pyk/proof/reachability.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 2fa71be8298..93edb17ca19 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -188,14 +188,14 @@ def get_steps(self) -> list[APRProofStep]: def commit(self, result: APRProofResult) -> None: self.prior_loops_cache[result.node_id] = result.prior_loops_cache_update - if isinstance(result, APRProofBoundedResult): - self.add_bounded(result.node_id) - elif isinstance(result, APRProofTerminalResult): - self.add_terminal(result.node_id) + if isinstance(result, APRProofExtendResult): + self.kcfg.extend(result.extend_result, self.kcfg.node(result.node_id), logs=self.logs) elif isinstance(result, APRProofSubsumeResult): self.kcfg.create_cover(result.node_id, self.target, csubst=result.csubst) - elif isinstance(result, APRProofExtendResult): - self.kcfg.extend(result.extend_result, self.kcfg.node(result.node_id), logs=self.logs) + elif isinstance(result, APRProofTerminalResult): + self.add_terminal(result.node_id) + elif isinstance(result, APRProofBoundedResult): + self.add_bounded(result.node_id) else: raise ValueError(f'Incorrect result type, expected APRProofResult: {result}') From 00d519e9cbbebec0629d6c1de3d18081cbd62c68 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 15 Aug 2024 15:10:24 +0200 Subject: [PATCH 04/29] adding predecessor to APRProofStep --- pyk/src/pyk/proof/reachability.py | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 93edb17ca19..c45f218d5b4 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -68,6 +68,7 @@ class APRProofStep: bmc_depth: int | None module_name: str shortest_path_to_node: tuple[KCFG.Node, ...] + predecessor_node_id: NodeIdLike | None prior_loops_cache: FrozenDict[int, tuple[int, ...]] = field(compare=False) circularity: bool nonzero_depth: bool @@ -170,11 +171,17 @@ def get_steps(self) -> list[APRProofStep]: nonzero_depth = self.nonzero_depth(node) module_name = self.circularities_module_name if nonzero_depth else self.dependencies_module_name + predecessor_edges = self.kcfg.edges(target_id=node.id) + predecessor_node_id: NodeIdLike | None = ( + single(predecessor_edges).source.id if predecessor_edges is not None else None + ) + steps.append( APRProofStep( bmc_depth=self.bmc_depth, module_name=module_name, node=node, + predecessor_node_id=predecessor_node_id, proof_id=self.id, target=self.kcfg.node(self.target), shortest_path_to_node=tuple(shortest_path), @@ -795,8 +802,8 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: if step.circularity and not step.nonzero_depth and (execute_depth is None or execute_depth > 1): execute_depth = 1 - if step.node.id in self.next_steps: - extend_results = [self.next_steps.pop(step.node.id)] + if step.predecessor_node_id in self.next_steps: + extend_results = [self.next_steps.pop(step.predecessor_node_id)] else: extend_results = self.kcfg_explore.extend_cterm( step.node.cterm, From f2158a8d1a73c76dcf94fea08d7f39a3fb5490e2 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 15 Aug 2024 15:18:44 +0200 Subject: [PATCH 05/29] correction --- pyk/src/pyk/proof/reachability.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index c45f218d5b4..e5656b203db 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -173,7 +173,7 @@ def get_steps(self) -> list[APRProofStep]: predecessor_edges = self.kcfg.edges(target_id=node.id) predecessor_node_id: NodeIdLike | None = ( - single(predecessor_edges).source.id if predecessor_edges is not None else None + single(predecessor_edges).source.id if predecessor_edges != [] else None ) steps.append( From 733d0892b57b051cd635415f5230fd5251886a14 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 15 Aug 2024 19:02:41 +0200 Subject: [PATCH 06/29] overhaul --- pyk/src/pyk/kcfg/explore.py | 40 ++++++------------- pyk/src/pyk/kcfg/kcfg.py | 27 +++++++++++-- pyk/src/pyk/kcfg/semantics.py | 6 +++ pyk/src/pyk/proof/reachability.py | 11 +++-- pyk/src/tests/integration/ktool/test_imp.py | 3 ++ .../integration/proof/test_custom_step.py | 12 ++++-- pyk/src/tests/integration/proof/test_goto.py | 3 ++ pyk/src/tests/integration/proof/test_imp.py | 3 ++ .../integration/proof/test_refute_node.py | 3 ++ .../tests/integration/proof/test_simple.py | 3 ++ 10 files changed, 73 insertions(+), 38 deletions(-) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index c7c3f2da8c2..c9427c066da 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -220,17 +220,12 @@ def extend_cterm( module_name: str | None = None, ) -> list[KCFGExtendResult]: - def log(message: str, *, warning: bool = False) -> None: - _LOGGER.log(logging.WARNING if warning else logging.INFO, f'Extend result for {self.id}: {message}') - custom_step_result = self.kcfg_semantics.custom_step(_cterm) if custom_step_result is not None: - log(f'custom step node: {node_id}') return [custom_step_result] abstract_cterm = self.kcfg_semantics.abstract_node(_cterm) if _cterm != abstract_cterm: - log(f'abstraction node: {node_id}') return [Abstract(abstract_cterm)] cterm, next_states, depth, vacuous, next_node_logs = self.cterm_symbolic.execute( @@ -245,29 +240,21 @@ def log(message: str, *, warning: bool = False) -> None: # Basic block if depth > 0: - log(f'basic block at depth {depth}: {node_id}') - extend_results.append(Step(cterm, depth, next_node_logs, self._extract_rule_labels(next_node_logs))) + extend_results.append((Step(cterm, depth, next_node_logs, self._extract_rule_labels(next_node_logs)))) # Stuck or vacuous if not next_states: if vacuous: - log(f'vacuous node: {node_id}', warning=True) extend_results.append(Vacuous()) - else: - log(f'stuck node: {node_id}') + elif depth == 0: extend_results.append(Stuck()) # Cut rule elif len(next_states) == 1: - log(f'cut-rule basic block at depth {depth}: {node_id}') - extend_results.append( - Step( - next_states[0].state, - 1, - next_node_logs, - self._extract_rule_labels(next_node_logs), - cut=True, + if not self.kcfg_semantics.can_make_custom_step(cterm): + (next_node_logs, rules) = ( + ((), []) if extend_results else (next_node_logs, self._extract_rule_labels(next_node_logs)) ) - ) + extend_results.append(Step(next_states[0].state, 1, next_node_logs, rules, cut=True, info='cut-rule')) # Branch elif all(branch_constraint for _, branch_constraint in next_states): branch_preds = [flatten_label('#And', not_none(rule_predicate)) for _, rule_predicate in next_states] @@ -280,17 +267,14 @@ def log(message: str, *, warning: bool = False) -> None: ) ) branches = [mlAnd(pred for pred in branch_pred if pred not in common_preds) for branch_pred in branch_preds] - if common_preds: - log( - f'Common predicates found in branches: {[self.pretty_print(ml_pred_to_bool(cp)) for cp in common_preds]}' - ) - constraint_strs = [self.pretty_print(ml_pred_to_bool(bc)) for bc in branches] - log(f'{len(branches)} branches: {node_id} -> {constraint_strs}') - extend_results.append(Branch(branches)) + info = f'{[self.pretty_print(ml_pred_to_bool(bc)) for bc in branches]}' + extend_results.append(Branch(branches, info=info)) else: # NDBranch - log(f'{len(next_states)} non-deterministic branches: {node_id}') next_cterms = [cterm for cterm, _ in next_states] - extend_results.append(NDBranch(next_cterms, next_node_logs, self._extract_rule_labels(next_node_logs))) + (next_node_logs, rules) = ( + ((), []) if extend_results else (next_node_logs, self._extract_rule_labels(next_node_logs)) + ) + extend_results.append(NDBranch(next_cterms, next_node_logs, rules)) return extend_results diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 835aea290c5..07b5e0062db 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -509,30 +509,45 @@ def extend( node: KCFG.Node, logs: dict[int, tuple[LogEntry, ...]], ) -> None: + + def log(message: str, *, warning: bool = False) -> None: + result_info = extend_result.info if type(extend_result) is Step or type(extend_result) is Branch else '' + result_info_message = f': {result_info}' if result_info else '' + _LOGGER.log( + logging.WARNING if warning else logging.INFO, + f'Extend result for {node.id}: {message}{result_info_message}', + ) + match extend_result: case Vacuous(): self.add_vacuous(node.id) + log(f'vacuous node: {node.id}', warning=True) case Stuck(): self.add_stuck(node.id) + log(f'stuck node: {node.id}') case Abstract(cterm): new_node = self.create_node(cterm) self.create_cover(node.id, new_node.id) + log(f'abstraction node: {node.id}') case Step(cterm, depth, next_node_logs, rule_labels, _): next_node = self.create_node(cterm) logs[next_node.id] = next_node_logs self.create_edge(node.id, next_node.id, depth, rules=rule_labels) + log(f'basic block at depth {depth}: {node.id} --> {next_node.id}') - case Branch(constraints, _): - self.split_on_constraints(node.id, constraints) + case Branch(branches, _): + branch_node_ids = self.split_on_constraints(node.id, branches) + log(f'{len(branches)} branches: {node.id} --> {branch_node_ids}') case NDBranch(cterms, next_node_logs, rule_labels): next_ids = [self.create_node(cterm).id for cterm in cterms] for i in next_ids: logs[i] = next_node_logs self.create_ndbranch(node.id, next_ids, rules=rule_labels) + log(f'{len(cterms)} non-deterministic branches: {node.id} --> {next_ids}') case _: raise AssertionError() @@ -1306,7 +1321,8 @@ def read_node_data(cfg_dir: Path, node_id: int) -> KCFG.Node: return KCFG.Node.from_dict(store.read_node_data(node_id)) -class KCFGExtendResult(ABC): ... +class KCFGExtendResult(ABC): + info: str = field(default='') @final @@ -1333,6 +1349,7 @@ class Step(KCFGExtendResult): logs: tuple[LogEntry, ...] rule_labels: list[str] cut: bool = field(default=False) + info: str = field(default='') @final @@ -1340,10 +1357,12 @@ class Step(KCFGExtendResult): class Branch(KCFGExtendResult): constraints: tuple[KInner, ...] heuristic: bool + info: str = field(default='') - def __init__(self, constraints: Iterable[KInner], *, heuristic: bool = False): + def __init__(self, constraints: Iterable[KInner], *, heuristic: bool = False, info: str = ''): object.__setattr__(self, 'constraints', tuple(constraints)) object.__setattr__(self, 'heuristic', heuristic) + object.__setattr__(self, 'info', info) @final diff --git a/pyk/src/pyk/kcfg/semantics.py b/pyk/src/pyk/kcfg/semantics.py index 05134f82e00..1c611818de2 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/pyk/src/pyk/kcfg/semantics.py @@ -18,6 +18,9 @@ def abstract_node(self, c: CTerm) -> CTerm: ... @abstractmethod def same_loop(self, c1: CTerm, c2: CTerm) -> bool: ... + @abstractmethod + def can_make_custom_step(self, c: CTerm) -> bool: ... + @abstractmethod def custom_step(self, c: CTerm) -> KCFGExtendResult | None: ... @@ -32,5 +35,8 @@ def abstract_node(self, c: CTerm) -> CTerm: 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 diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index e5656b203db..1366e278035 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -196,7 +196,11 @@ def get_steps(self) -> list[APRProofStep]: def commit(self, result: APRProofResult) -> None: self.prior_loops_cache[result.node_id] = result.prior_loops_cache_update if isinstance(result, APRProofExtendResult): - self.kcfg.extend(result.extend_result, self.kcfg.node(result.node_id), logs=self.logs) + self.kcfg.extend( + result.extend_result, + node=self.kcfg.node(result.node_id), + logs=self.logs, + ) elif isinstance(result, APRProofSubsumeResult): self.kcfg.create_cover(result.node_id, self.target, csubst=result.csubst) elif isinstance(result, APRProofTerminalResult): @@ -815,14 +819,15 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: ) assert len(extend_results) == 1 or len(extend_results) == 2 - extend_result = extend_results[0] if len(extend_results) == 2: assert step.node.id not in self.next_steps self.next_steps[step.node.id] = extend_results[1] return [ APRProofExtendResult( - node_id=step.node.id, extend_result=extend_result, prior_loops_cache_update=prior_loops + node_id=step.node.id, + extend_result=extend_results[0], + prior_loops_cache_update=prior_loops, ) ] diff --git a/pyk/src/tests/integration/ktool/test_imp.py b/pyk/src/tests/integration/ktool/test_imp.py index 66b45faa559..bf61b808677 100644 --- a/pyk/src/tests/integration/ktool/test_imp.py +++ b/pyk/src/tests/integration/ktool/test_imp.py @@ -58,6 +58,9 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: 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 diff --git a/pyk/src/tests/integration/proof/test_custom_step.py b/pyk/src/tests/integration/proof/test_custom_step.py index b1aa1e357f8..ed73b4b7b86 100644 --- a/pyk/src/tests/integration/proof/test_custom_step.py +++ b/pyk/src/tests/integration/proof/test_custom_step.py @@ -63,18 +63,24 @@ def abstract_node(self, c: CTerm) -> CTerm: 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 custom_step(self, c: CTerm) -> KCFGExtendResult | None: + def can_make_custom_step(self, c: CTerm) -> bool: k_cell = c.cell('K_CELL') - if ( + return ( type(k_cell) is KSequence and type(k_cell[0]) is KApply and k_cell[0].label.name == 'c_CUSTOM-STEP-SYNTAX_Step' - ): + ) + + def custom_step(self, c: CTerm) -> KCFGExtendResult | None: + if self.can_make_custom_step(c): new_cterm = CTerm.from_kast(set_cell(c.kast, 'K_CELL', KSequence(KApply('d_CUSTOM-STEP-SYNTAX_Step')))) return Step(new_cterm, 1, (), ['CUSTOM-STEP.c.d'], cut=True) return None diff --git a/pyk/src/tests/integration/proof/test_goto.py b/pyk/src/tests/integration/proof/test_goto.py index 06666c352f0..3a8b74aaff9 100644 --- a/pyk/src/tests/integration/proof/test_goto.py +++ b/pyk/src/tests/integration/proof/test_goto.py @@ -44,6 +44,9 @@ 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 diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index b087432a8ea..8acbcd60cc7 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -74,6 +74,9 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: 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 diff --git a/pyk/src/tests/integration/proof/test_refute_node.py b/pyk/src/tests/integration/proof/test_refute_node.py index c60fbab7728..69f5a28bb7e 100644 --- a/pyk/src/tests/integration/proof/test_refute_node.py +++ b/pyk/src/tests/integration/proof/test_refute_node.py @@ -63,6 +63,9 @@ def abstract_node(self, c: CTerm) -> CTerm: 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 diff --git a/pyk/src/tests/integration/proof/test_simple.py b/pyk/src/tests/integration/proof/test_simple.py index f4517c27d9f..4ce4d8e7ef6 100644 --- a/pyk/src/tests/integration/proof/test_simple.py +++ b/pyk/src/tests/integration/proof/test_simple.py @@ -36,6 +36,9 @@ def abstract_node(self, c: CTerm) -> CTerm: 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 From 869e7b2f40a6c39129c9e5d9c8ca1846dffdf50c Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 15 Aug 2024 19:08:22 +0200 Subject: [PATCH 07/29] formatting correction --- pyk/src/pyk/kcfg/explore.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index c9427c066da..c401a06cdda 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -240,7 +240,7 @@ def extend_cterm( # Basic block if depth > 0: - extend_results.append((Step(cterm, depth, next_node_logs, self._extract_rule_labels(next_node_logs)))) + extend_results.append(Step(cterm, depth, next_node_logs, self._extract_rule_labels(next_node_logs))) # Stuck or vacuous if not next_states: From b20e4c60ddc8d277581df52b7d5dd0602cf564f9 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 15 Aug 2024 23:19:53 +0200 Subject: [PATCH 08/29] better logging message --- pyk/src/pyk/kcfg/kcfg.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 07b5e0062db..5dd204e15f0 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -515,7 +515,7 @@ def log(message: str, *, warning: bool = False) -> None: result_info_message = f': {result_info}' if result_info else '' _LOGGER.log( logging.WARNING if warning else logging.INFO, - f'Extend result for {node.id}: {message}{result_info_message}', + f'Extend KCFG: {message}{result_info_message}', ) match extend_result: From a60b914497a7e05a02a42fdfb9df34cc7fef7a0f Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 15 Aug 2024 23:48:46 +0200 Subject: [PATCH 09/29] further messages --- pyk/src/pyk/kcfg/kcfg.py | 2 +- pyk/src/pyk/proof/reachability.py | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 5dd204e15f0..eafbf694431 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -515,7 +515,7 @@ def log(message: str, *, warning: bool = False) -> None: result_info_message = f': {result_info}' if result_info else '' _LOGGER.log( logging.WARNING if warning else logging.INFO, - f'Extend KCFG: {message}{result_info_message}', + f'Extending current KCFG with the following: {message}{result_info_message}', ) match extend_result: diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 1366e278035..c1583b867e2 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -807,6 +807,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: execute_depth = 1 if step.predecessor_node_id in self.next_steps: + _LOGGER.info(f'Using cached step for edge {step.predecessor_node_id} --> {step.node.id}') extend_results = [self.next_steps.pop(step.predecessor_node_id)] else: extend_results = self.kcfg_explore.extend_cterm( From 45fd80b2459237db4af2454e551b41f980502869 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 02:10:03 +0200 Subject: [PATCH 10/29] minor further messages --- pyk/src/pyk/proof/reachability.py | 1 + 1 file changed, 1 insertion(+) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index c1583b867e2..5e59a909c6f 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -822,6 +822,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: assert len(extend_results) == 1 or len(extend_results) == 2 if len(extend_results) == 2: assert step.node.id not in self.next_steps + _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') self.next_steps[step.node.id] = extend_results[1] return [ From 0018b2abbc01af48390898608b709e050f7df64d Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 08:55:56 +0200 Subject: [PATCH 11/29] moving logic to APRProof --- pyk/src/pyk/proof/reachability.py | 39 +++++++++++++++++++++++-------- 1 file changed, 29 insertions(+), 10 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 5e59a909c6f..401ee4d3ffd 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -44,7 +44,8 @@ class APRProofResult: @dataclass class APRProofExtendResult(APRProofResult): - extend_result: KCFGExtendResult + extend_results: list[KCFGExtendResult] + to_cache: bool = field(default=False) @dataclass @@ -66,6 +67,7 @@ class APRProofStep: target: KCFG.Node proof_id: str bmc_depth: int | None + cached: bool module_name: str shortest_path_to_node: tuple[KCFG.Node, ...] predecessor_node_id: NodeIdLike | None @@ -100,6 +102,7 @@ class APRProof(Proof[APRProofStep, APRProofResult], KCFGExploration): prior_loops_cache: dict[int, tuple[int, ...]] _checked_for_bounded: set[int] + _next_steps: dict[NodeIdLike, KCFGExtendResult] def __init__( self, @@ -137,6 +140,7 @@ def __init__( self.error_info = error_info self._checked_for_bounded = set() + self._next_steps = {} if self.proof_dir is not None and self.proof_subdir is not None: ensure_dir_path(self.proof_dir) @@ -182,6 +186,7 @@ def get_steps(self) -> list[APRProofStep]: module_name=module_name, node=node, predecessor_node_id=predecessor_node_id, + cached=predecessor_node_id in self._next_steps, proof_id=self.id, target=self.kcfg.node(self.target), shortest_path_to_node=tuple(shortest_path), @@ -196,8 +201,22 @@ def get_steps(self) -> list[APRProofStep]: def commit(self, result: APRProofResult) -> None: self.prior_loops_cache[result.node_id] = result.prior_loops_cache_update if isinstance(result, APRProofExtendResult): + # Result has been cached, use the cache + if len(result.extend_results) == 0: + assert result.node_id in self._next_steps + extend_result = self._next_steps.pop(result.node_id) + # Result contains two steps, first to be applied, second to be cached + elif result.to_cache: + assert result.node_id not in self._next_steps + assert result.extend_results is not None and len(result.extend_results) == 2 + self._next_steps[result.node_id] = result.extend_results[1] + extend_result = result.extend_results[0] + # Result contains one step, which is to be applied + else: + assert result.extend_results is not None and len(result.extend_results) == 1 + extend_result = result.extend_results[0] self.kcfg.extend( - result.extend_result, + extend_result=extend_result, node=self.kcfg.node(result.node_id), logs=self.logs, ) @@ -685,7 +704,6 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]): direct_subproof_rules: bool assume_defined: bool kcfg_explore: KCFGExplore - next_steps: dict[NodeIdLike, KCFGExtendResult] def __init__( self, @@ -710,7 +728,6 @@ def __init__( self.fast_check_subsumption = fast_check_subsumption self.direct_subproof_rules = direct_subproof_rules self.assume_defined = assume_defined - self.next_steps = {} def close(self) -> None: self.kcfg_explore.cterm_symbolic._kore_client.close() @@ -806,9 +823,9 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: if step.circularity and not step.nonzero_depth and (execute_depth is None or execute_depth > 1): execute_depth = 1 - if step.predecessor_node_id in self.next_steps: + if step.cached: _LOGGER.info(f'Using cached step for edge {step.predecessor_node_id} --> {step.node.id}') - extend_results = [self.next_steps.pop(step.predecessor_node_id)] + extend_results = [] else: extend_results = self.kcfg_explore.extend_cterm( step.node.cterm, @@ -819,17 +836,19 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: node_id=step.node.id, ) - assert len(extend_results) == 1 or len(extend_results) == 2 + to_cache: bool = False + + assert len(extend_results) <= 2 if len(extend_results) == 2: - assert step.node.id not in self.next_steps _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') - self.next_steps[step.node.id] = extend_results[1] + to_cache = True return [ APRProofExtendResult( node_id=step.node.id, - extend_result=extend_results[0], + extend_results=extend_results, prior_loops_cache_update=prior_loops, + to_cache=to_cache, ) ] From b0bc50e79f00ecbe80977d172295f5ee263f2bc1 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 10:20:29 +0200 Subject: [PATCH 12/29] corrections --- pyk/src/pyk/proof/reachability.py | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 401ee4d3ffd..483c234c4a9 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -46,6 +46,7 @@ class APRProofResult: class APRProofExtendResult(APRProofResult): extend_results: list[KCFGExtendResult] to_cache: bool = field(default=False) + use_cache: NodeIdLike | None = field(default=None) @dataclass @@ -202,9 +203,10 @@ def commit(self, result: APRProofResult) -> None: self.prior_loops_cache[result.node_id] = result.prior_loops_cache_update if isinstance(result, APRProofExtendResult): # Result has been cached, use the cache - if len(result.extend_results) == 0: - assert result.node_id in self._next_steps - extend_result = self._next_steps.pop(result.node_id) + if result.use_cache is not None: + assert len(result.extend_results) == 0 + assert result.use_cache in self._next_steps + extend_result = self._next_steps.pop(result.use_cache) # Result contains two steps, first to be applied, second to be cached elif result.to_cache: assert result.node_id not in self._next_steps @@ -778,6 +780,9 @@ def _check_subsume(self, node: KCFG.Node, target_node: KCFG.Node, proof_id: str) return csubst def step_proof(self, step: APRProofStep) -> list[APRProofResult]: + to_cache: bool = False + use_cache: NodeIdLike | None = None + prior_loops: tuple[int, ...] = () if step.bmc_depth is not None: for node in step.shortest_path_to_node: @@ -826,6 +831,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: if step.cached: _LOGGER.info(f'Using cached step for edge {step.predecessor_node_id} --> {step.node.id}') extend_results = [] + use_cache = step.predecessor_node_id else: extend_results = self.kcfg_explore.extend_cterm( step.node.cterm, @@ -836,8 +842,6 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: node_id=step.node.id, ) - to_cache: bool = False - assert len(extend_results) <= 2 if len(extend_results) == 2: _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') @@ -849,6 +853,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: extend_results=extend_results, prior_loops_cache_update=prior_loops, to_cache=to_cache, + use_cache=use_cache, ) ] From 8d4ab1f46a735124e591f0c427296685e7812974 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 19:14:18 +0200 Subject: [PATCH 13/29] documentation and circularity precision --- pyk/src/pyk/proof/reachability.py | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 483c234c4a9..145db2a2fda 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -44,6 +44,16 @@ class APRProofResult: @dataclass class APRProofExtendResult(APRProofResult): + """Holds the description of how an APRProof should be extended. + + Fields: + extend_results: Holds the KCFG extension to be applied. + to_cache: Holds an indicator of whether or not the provided extension + should be cached instead of being applied. + use_cache: If not None, holds the identifier of the node whose cached extension + should be applied instead of the provided extension. + """ + extend_results: list[KCFGExtendResult] to_cache: bool = field(default=False) use_cache: NodeIdLike | None = field(default=None) @@ -828,7 +838,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: if step.circularity and not step.nonzero_depth and (execute_depth is None or execute_depth > 1): execute_depth = 1 - if step.cached: + if step.cached and not (step.circularity and not step.nonzero_depth): _LOGGER.info(f'Using cached step for edge {step.predecessor_node_id} --> {step.node.id}') extend_results = [] use_cache = step.predecessor_node_id From e865465e37efae50fcd425495f00ecbe312011dc Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 19:54:44 +0200 Subject: [PATCH 14/29] second attempt at understanding circularities --- pyk/src/pyk/proof/reachability.py | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 145db2a2fda..334253ceae4 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -838,7 +838,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: if step.circularity and not step.nonzero_depth and (execute_depth is None or execute_depth > 1): execute_depth = 1 - if step.cached and not (step.circularity and not step.nonzero_depth): + if step.cached: _LOGGER.info(f'Using cached step for edge {step.predecessor_node_id} --> {step.node.id}') extend_results = [] use_cache = step.predecessor_node_id @@ -854,8 +854,12 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: assert len(extend_results) <= 2 if len(extend_results) == 2: - _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') - to_cache = True + # Do not cache if we are proving a circularity and have not made a step yet + if not (step.circularity and not step.nonzero_depth): + _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') + to_cache = True + else: + extend_results = [extend_results[0]] return [ APRProofExtendResult( From 12b0fc0749cb592e8fd49e82e58ab332f453692c Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 20:34:26 +0200 Subject: [PATCH 15/29] additional precision re circular rules --- pyk/src/pyk/proof/reachability.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 334253ceae4..b734227a092 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -793,6 +793,8 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: to_cache: bool = False use_cache: NodeIdLike | None = None + print(f'{step}') + prior_loops: tuple[int, ...] = () if step.bmc_depth is not None: for node in step.shortest_path_to_node: @@ -854,8 +856,8 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: assert len(extend_results) <= 2 if len(extend_results) == 2: - # Do not cache if we are proving a circularity and have not made a step yet - if not (step.circularity and not step.nonzero_depth): + # Do not cache if we have not made a step yet, to avoid circularity issues + if not step.nonzero_depth: _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') to_cache = True else: From 5ce87e8c2dbba091f1a2dce41de7c3b4388dccbc Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 20:52:27 +0200 Subject: [PATCH 16/29] correction --- pyk/src/pyk/proof/reachability.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index b734227a092..6e5676384e7 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -793,8 +793,6 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: to_cache: bool = False use_cache: NodeIdLike | None = None - print(f'{step}') - prior_loops: tuple[int, ...] = () if step.bmc_depth is not None: for node in step.shortest_path_to_node: From 68ba0b1d7ad91c741581281cd143be9bfd098a27 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 21:33:36 +0200 Subject: [PATCH 17/29] more corrections --- pyk/src/pyk/proof/reachability.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 6e5676384e7..bcbb4bc0857 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -793,6 +793,8 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: to_cache: bool = False use_cache: NodeIdLike | None = None + print(f'{step.node.id}'-{step.circularity}-{step.nonzero_depth}) + prior_loops: tuple[int, ...] = () if step.bmc_depth is not None: for node in step.shortest_path_to_node: @@ -855,7 +857,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: assert len(extend_results) <= 2 if len(extend_results) == 2: # Do not cache if we have not made a step yet, to avoid circularity issues - if not step.nonzero_depth: + if step.nonzero_depth: _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') to_cache = True else: From 3321f486b25c18c8f7039cc65859228ba49acbcf Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 21:34:18 +0200 Subject: [PATCH 18/29] comments --- pyk/src/pyk/proof/reachability.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index bcbb4bc0857..527649194a5 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -856,10 +856,11 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: assert len(extend_results) <= 2 if len(extend_results) == 2: - # Do not cache if we have not made a step yet, to avoid circularity issues + # Cache only if the step is non-zero depth if step.nonzero_depth: _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') to_cache = True + # Otherwise, discard the second result else: extend_results = [extend_results[0]] From 9c86d7e2809d67f9b3204c5ed19c55ca59d1da4f Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 22:06:16 +0200 Subject: [PATCH 19/29] formatting --- pyk/src/pyk/proof/reachability.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 527649194a5..ff0e2e6fa20 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -793,7 +793,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: to_cache: bool = False use_cache: NodeIdLike | None = None - print(f'{step.node.id}'-{step.circularity}-{step.nonzero_depth}) + print(f'{step.node.id}' - {step.circularity} - {step.nonzero_depth}) prior_loops: tuple[int, ...] = () if step.bmc_depth is not None: From 207e325046b3e0d8609528ed4e4daa21615dc514 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 22:08:27 +0200 Subject: [PATCH 20/29] even more formatting --- pyk/src/pyk/proof/reachability.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index ff0e2e6fa20..ab51725845a 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -793,8 +793,6 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: to_cache: bool = False use_cache: NodeIdLike | None = None - print(f'{step.node.id}' - {step.circularity} - {step.nonzero_depth}) - prior_loops: tuple[int, ...] = () if step.bmc_depth is not None: for node in step.shortest_path_to_node: From c19f63d10e2e86cf4d4ca466a3f620b07f171b8c Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 22:54:11 +0200 Subject: [PATCH 21/29] removing always_check_subsumption, more comments --- pyk/src/pyk/proof/reachability.py | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index ab51725845a..d9c0436501c 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -711,7 +711,6 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]): cut_point_rules: Iterable[str] terminal_rules: Iterable[str] counterexample_info: bool - always_check_subsumption: bool fast_check_subsumption: bool direct_subproof_rules: bool assume_defined: bool @@ -724,7 +723,6 @@ def __init__( cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), counterexample_info: bool = False, - always_check_subsumption: bool = True, fast_check_subsumption: bool = False, direct_subproof_rules: bool = False, assume_defined: bool = False, @@ -736,7 +734,6 @@ def __init__( self.cut_point_rules = cut_point_rules self.terminal_rules = terminal_rules self.counterexample_info = counterexample_info - self.always_check_subsumption = always_check_subsumption self.fast_check_subsumption = fast_check_subsumption self.direct_subproof_rules = direct_subproof_rules self.assume_defined = assume_defined @@ -790,9 +787,7 @@ def _check_subsume(self, node: KCFG.Node, target_node: KCFG.Node, proof_id: str) return csubst def step_proof(self, step: APRProofStep) -> list[APRProofResult]: - to_cache: bool = False - use_cache: NodeIdLike | None = None - + # Check if the current node should be bounded prior_loops: tuple[int, ...] = () if step.bmc_depth is not None: for node in step.shortest_path_to_node: @@ -806,7 +801,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: _LOGGER.warning(f'Bounded node {step.proof_id}: {step.node.id} at bmc depth {step.bmc_depth}') return [APRProofBoundedResult(node_id=step.node.id, prior_loops_cache_update=prior_loops)] - # Terminal checks for current node and target node + # Check if the current node and target ar terminal is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(step.node.cterm) target_is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(step.target.cterm) @@ -814,7 +809,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: [APRProofTerminalResult(node_id=step.node.id, prior_loops_cache_update=prior_loops)] if is_terminal else [] ) - # Subsumption should be checked if and only if the target node + # Subsumption is checked if and only if the target node # and the current node are either both terminal or both not terminal if is_terminal == target_is_terminal: csubst = self._check_subsume(step.node, step.target, proof_id=step.proof_id) @@ -835,13 +830,15 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: # Ensure that we record progress ASAP for circularities, so the circularity rule will be included for execution as soon as possible execute_depth = self.execute_depth - if step.circularity and not step.nonzero_depth and (execute_depth is None or execute_depth > 1): + if step.circularity and not step.nonzero_depth: execute_depth = 1 + # If the step has already been cached, do not invoke the backend and only send a signal back to the proof to use the cache if step.cached: _LOGGER.info(f'Using cached step for edge {step.predecessor_node_id} --> {step.node.id}') extend_results = [] use_cache = step.predecessor_node_id + # Invoke the backend to obtain the next KCFG extension else: extend_results = self.kcfg_explore.extend_cterm( step.node.cterm, @@ -852,9 +849,11 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: node_id=step.node.id, ) + # We can obtain two results at most assert len(extend_results) <= 2 + # We have obtained two results: first is to be applied, second to be cached potentially if len(extend_results) == 2: - # Cache only if the step is non-zero depth + # Cache only if the current node is at non-zero depth if step.nonzero_depth: _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') to_cache = True From 4d695ad82a34918a0872ef3e0d87a8ecc94a4c9c Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Fri, 16 Aug 2024 23:18:56 +0200 Subject: [PATCH 22/29] correction --- pyk/src/pyk/proof/reachability.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index d9c0436501c..6678116c80b 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -833,6 +833,8 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: if step.circularity and not step.nonzero_depth: execute_depth = 1 + use_cache: NodeIdLike | None = None + # If the step has already been cached, do not invoke the backend and only send a signal back to the proof to use the cache if step.cached: _LOGGER.info(f'Using cached step for edge {step.predecessor_node_id} --> {step.node.id}') @@ -849,6 +851,8 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: node_id=step.node.id, ) + to_cache: bool = False + # We can obtain two results at most assert len(extend_results) <= 2 # We have obtained two results: first is to be applied, second to be cached potentially From d3d3cae23e56b636958e5de1b048d670fcb6c346 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Sat, 17 Aug 2024 22:22:53 +0100 Subject: [PATCH 23/29] Final correction --- pyk/src/pyk/kcfg/explore.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index c401a06cdda..82f83668a35 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -250,7 +250,7 @@ def extend_cterm( extend_results.append(Stuck()) # Cut rule elif len(next_states) == 1: - if not self.kcfg_semantics.can_make_custom_step(cterm): + if not self.kcfg_semantics.can_make_custom_step(next_states[0]): (next_node_logs, rules) = ( ((), []) if extend_results else (next_node_logs, self._extract_rule_labels(next_node_logs)) ) From 4d5490838e2598c0ca2b5d8bff30d027514d1fa3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Sat, 17 Aug 2024 22:36:54 +0100 Subject: [PATCH 24/29] Update pyk/src/pyk/kcfg/explore.py --- pyk/src/pyk/kcfg/explore.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 82f83668a35..f53f422966d 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -250,7 +250,7 @@ def extend_cterm( extend_results.append(Stuck()) # Cut rule elif len(next_states) == 1: - if not self.kcfg_semantics.can_make_custom_step(next_states[0]): + if not self.kcfg_semantics.can_make_custom_step(next_states[0].state): (next_node_logs, rules) = ( ((), []) if extend_results else (next_node_logs, self._extract_rule_labels(next_node_logs)) ) From a66170064aa32a000d968221f26d9ca4e8ba2134 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Sat, 17 Aug 2024 23:11:01 +0100 Subject: [PATCH 25/29] Update pyk/src/pyk/kcfg/explore.py --- pyk/src/pyk/kcfg/explore.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index f53f422966d..c401a06cdda 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -250,7 +250,7 @@ def extend_cterm( extend_results.append(Stuck()) # Cut rule elif len(next_states) == 1: - if not self.kcfg_semantics.can_make_custom_step(next_states[0].state): + if not self.kcfg_semantics.can_make_custom_step(cterm): (next_node_logs, rules) = ( ((), []) if extend_results else (next_node_logs, self._extract_rule_labels(next_node_logs)) ) From 852fba4bae03870e99938b7f013a1f55b198107c Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Mon, 19 Aug 2024 11:36:32 +0200 Subject: [PATCH 26/29] minor corrections --- pyk/src/pyk/kcfg/kcfg.py | 3 +-- pyk/src/pyk/kcfg/semantics.py | 10 ++++++++++ pyk/src/pyk/proof/reachability.py | 2 +- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index eafbf694431..16825a71d95 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -1321,8 +1321,7 @@ def read_node_data(cfg_dir: Path, node_id: int) -> KCFG.Node: return KCFG.Node.from_dict(store.read_node_data(node_id)) -class KCFGExtendResult(ABC): - info: str = field(default='') +class KCFGExtendResult(ABC): ... @final diff --git a/pyk/src/pyk/kcfg/semantics.py b/pyk/src/pyk/kcfg/semantics.py index 1c611818de2..d48b986a981 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/pyk/src/pyk/kcfg/semantics.py @@ -12,18 +12,28 @@ class KCFGSemantics(ABC): @abstractmethod def is_terminal(self, c: CTerm) -> bool: ... + """Checks whether or not a given CTerm is terminal.""" + @abstractmethod def abstract_node(self, c: CTerm) -> CTerm: ... + """Implements an abstraction mechanism.""" + @abstractmethod def same_loop(self, c1: CTerm, c2: CTerm) -> bool: ... + """Checks whether or not the two given CTerms represent the same loop head.""" + @abstractmethod def can_make_custom_step(self, c: CTerm) -> bool: ... + """Checks whether or not the semantics can make a custom step from a given CTerm.""" + @abstractmethod def custom_step(self, c: CTerm) -> KCFGExtendResult | None: ... + """Implements a custom semantic step.""" + class DefaultSemantics(KCFGSemantics): def is_terminal(self, c: CTerm) -> bool: diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 6678116c80b..385fe4c36ad 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -46,7 +46,7 @@ class APRProofResult: class APRProofExtendResult(APRProofResult): """Holds the description of how an APRProof should be extended. - Fields: + Attributes: extend_results: Holds the KCFG extension to be applied. to_cache: Holds an indicator of whether or not the provided extension should be cached instead of being applied. From 76e9f1eb49556d507181dbc50b0a130c180de4fc Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Mon, 19 Aug 2024 12:45:36 +0200 Subject: [PATCH 27/29] refactoring proof results --- pyk/src/pyk/proof/reachability.py | 97 ++++++++++++++++--------------- 1 file changed, 50 insertions(+), 47 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 385fe4c36ad..6ca8b182db2 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -44,19 +44,23 @@ class APRProofResult: @dataclass class APRProofExtendResult(APRProofResult): - """Holds the description of how an APRProof should be extended. - - Attributes: - extend_results: Holds the KCFG extension to be applied. - to_cache: Holds an indicator of whether or not the provided extension - should be cached instead of being applied. - use_cache: If not None, holds the identifier of the node whose cached extension - should be applied instead of the provided extension. - """ + """Proof extension to be applied.""" + + extension_to_apply: KCFGExtendResult + + +@dataclass +class APRProofExtendAndCacheResult(APRProofExtendResult): + """Proof extension to be cached.""" - extend_results: list[KCFGExtendResult] - to_cache: bool = field(default=False) - use_cache: NodeIdLike | None = field(default=None) + extension_to_cache: KCFGExtendResult + + +@dataclass +class APRProofUseCacheResult(APRProofResult): + """Proof extension to be applied using the extension cache.""" + + cached_node_id: NodeIdLike @dataclass @@ -78,10 +82,9 @@ class APRProofStep: target: KCFG.Node proof_id: str bmc_depth: int | None - cached: bool + use_cache: NodeIdLike | None module_name: str shortest_path_to_node: tuple[KCFG.Node, ...] - predecessor_node_id: NodeIdLike | None prior_loops_cache: FrozenDict[int, tuple[int, ...]] = field(compare=False) circularity: bool nonzero_depth: bool @@ -196,8 +199,7 @@ def get_steps(self) -> list[APRProofStep]: bmc_depth=self.bmc_depth, module_name=module_name, node=node, - predecessor_node_id=predecessor_node_id, - cached=predecessor_node_id in self._next_steps, + use_cache=predecessor_node_id if predecessor_node_id in self._next_steps else None, proof_id=self.id, target=self.kcfg.node(self.target), shortest_path_to_node=tuple(shortest_path), @@ -211,24 +213,21 @@ def get_steps(self) -> list[APRProofStep]: def commit(self, result: APRProofResult) -> None: self.prior_loops_cache[result.node_id] = result.prior_loops_cache_update - if isinstance(result, APRProofExtendResult): - # Result has been cached, use the cache - if result.use_cache is not None: - assert len(result.extend_results) == 0 - assert result.use_cache in self._next_steps - extend_result = self._next_steps.pop(result.use_cache) - # Result contains two steps, first to be applied, second to be cached - elif result.to_cache: + # Result has been cached, use the cache + if isinstance(result, APRProofUseCacheResult): + assert result.cached_node_id in self._next_steps + self.kcfg.extend( + extend_result=self._next_steps.pop(result.cached_node_id), + node=self.kcfg.node(result.node_id), + logs=self.logs, + ) + elif isinstance(result, APRProofExtendResult): + # Result contains two steps, one to be applied, one to be cached + if isinstance(result, APRProofExtendAndCacheResult): assert result.node_id not in self._next_steps - assert result.extend_results is not None and len(result.extend_results) == 2 - self._next_steps[result.node_id] = result.extend_results[1] - extend_result = result.extend_results[0] - # Result contains one step, which is to be applied - else: - assert result.extend_results is not None and len(result.extend_results) == 1 - extend_result = result.extend_results[0] + self._next_steps[result.node_id] = result.extension_to_cache self.kcfg.extend( - extend_result=extend_result, + extend_result=result.extension_to_apply, node=self.kcfg.node(result.node_id), logs=self.logs, ) @@ -833,13 +832,16 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: if step.circularity and not step.nonzero_depth: execute_depth = 1 - use_cache: NodeIdLike | None = None - # If the step has already been cached, do not invoke the backend and only send a signal back to the proof to use the cache - if step.cached: - _LOGGER.info(f'Using cached step for edge {step.predecessor_node_id} --> {step.node.id}') - extend_results = [] - use_cache = step.predecessor_node_id + if step.use_cache is not None: + _LOGGER.info(f'Using cached step for edge {step.use_cache} --> {step.node.id}') + return [ + APRProofUseCacheResult( + node_id=step.node.id, + cached_node_id=step.use_cache, + prior_loops_cache_update=prior_loops, + ) + ] # Invoke the backend to obtain the next KCFG extension else: extend_results = self.kcfg_explore.extend_cterm( @@ -851,8 +853,6 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: node_id=step.node.id, ) - to_cache: bool = False - # We can obtain two results at most assert len(extend_results) <= 2 # We have obtained two results: first is to be applied, second to be cached potentially @@ -860,18 +860,21 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: # Cache only if the current node is at non-zero depth if step.nonzero_depth: _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') - to_cache = True - # Otherwise, discard the second result - else: - extend_results = [extend_results[0]] + return [ + APRProofExtendAndCacheResult( + node_id=step.node.id, + extension_to_apply=extend_results[0], + extension_to_cache=extend_results[1], + prior_loops_cache_update=prior_loops, + ) + ] + # Otherwise, discard the second result return [ APRProofExtendResult( node_id=step.node.id, - extend_results=extend_results, + extension_to_apply=extend_results[0], prior_loops_cache_update=prior_loops, - to_cache=to_cache, - use_cache=use_cache, ) ] From c3e6e8d37107d2ff42e65d6118049632142181fd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Mon, 19 Aug 2024 13:42:34 +0100 Subject: [PATCH 28/29] Update pyk/src/pyk/proof/reachability.py MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Tamás Tóth --- pyk/src/pyk/proof/reachability.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 6ca8b182db2..5879711b465 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -800,7 +800,7 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: _LOGGER.warning(f'Bounded node {step.proof_id}: {step.node.id} at bmc depth {step.bmc_depth}') return [APRProofBoundedResult(node_id=step.node.id, prior_loops_cache_update=prior_loops)] - # Check if the current node and target ar terminal + # Check if the current node and target are terminal is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(step.node.cterm) target_is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(step.target.cterm) From e60d2bec0462cfeb3edc1e5070dd57cd3ce3a34b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Mon, 19 Aug 2024 13:45:12 +0100 Subject: [PATCH 29/29] Update semantics.py Corrections --- pyk/src/pyk/kcfg/semantics.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/kcfg/semantics.py b/pyk/src/pyk/kcfg/semantics.py index d48b986a981..fc98409e607 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/pyk/src/pyk/kcfg/semantics.py @@ -12,27 +12,27 @@ class KCFGSemantics(ABC): @abstractmethod def is_terminal(self, c: CTerm) -> bool: ... - """Checks whether or not a given CTerm is terminal.""" + """Check whether or not a given ``CTerm`` is terminal.""" @abstractmethod def abstract_node(self, c: CTerm) -> CTerm: ... - """Implements an abstraction mechanism.""" + """Implement an abstraction mechanism.""" @abstractmethod def same_loop(self, c1: CTerm, c2: CTerm) -> bool: ... - """Checks whether or not the two given CTerms represent the same loop head.""" + """Check whether or not the two given ``CTerm``s represent the same loop head.""" @abstractmethod def can_make_custom_step(self, c: CTerm) -> bool: ... - """Checks whether or not the semantics can make a custom step from a given CTerm.""" + """Check whether or not the semantics can make a custom step from a given ``CTerm``.""" @abstractmethod def custom_step(self, c: CTerm) -> KCFGExtendResult | None: ... - """Implements a custom semantic step.""" + """Implement a custom semantic step.""" class DefaultSemantics(KCFGSemantics):