From c8738d6694434c6adcbce898629deacc47fc14b5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Mon, 19 Aug 2024 15:57:47 +0200 Subject: [PATCH] Reusing backend information to construct KCFGs more efficiently (#4590) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR leverages information provided by the backend as part of an `execute` request to construct more than one KCFG element: specifically, vacuous nodes, stuck nodes, edges resulting from cut-nodes, branches, and non-deterministic branches. In addition, it moves the associated printing to the KCFG class, allowing for more informative prints: for example, we can now print the target nodes of edges and branches, the absence of which (personally) was making debugging of large proofs slightly more difficult. The PR also removes the `always_check_subsumption` flag, which was not used and was made obsolete by the subsumption logic in `step_proof`. --------- Co-authored-by: Tamás Tóth --- pyk/src/pyk/kcfg/explore.py | 59 ++++------ pyk/src/pyk/kcfg/kcfg.py | 24 +++- pyk/src/pyk/kcfg/semantics.py | 16 +++ pyk/src/pyk/proof/reachability.py | 107 +++++++++++++++--- 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, 174 insertions(+), 59 deletions(-) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 69a02c07b0f..c401a06cdda 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -218,19 +218,15 @@ def extend_cterm( cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), module_name: str | None = None, - ) -> 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}') + ) -> list[KCFGExtendResult]: 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 +236,27 @@ 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()) + elif depth == 0: + extend_results.append(Stuck()) # Cut rule - if 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, - ) - + elif len(next_states) == 1: + 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 - 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( @@ -277,15 +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}') - return 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] - return 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..16825a71d95 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'Extending current KCFG with the following: {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() @@ -1333,6 +1348,7 @@ class Step(KCFGExtendResult): logs: tuple[LogEntry, ...] rule_labels: list[str] cut: bool = field(default=False) + info: str = field(default='') @final @@ -1340,10 +1356,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..fc98409e607 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/pyk/src/pyk/kcfg/semantics.py @@ -12,15 +12,28 @@ class KCFGSemantics(ABC): @abstractmethod def is_terminal(self, c: CTerm) -> bool: ... + """Check whether or not a given ``CTerm`` is terminal.""" + @abstractmethod def abstract_node(self, c: CTerm) -> CTerm: ... + """Implement an abstraction mechanism.""" + @abstractmethod def same_loop(self, c1: CTerm, c2: CTerm) -> bool: ... + """Check whether or not the two given ``CTerm``s represent the same loop head.""" + + @abstractmethod + def can_make_custom_step(self, c: CTerm) -> bool: ... + + """Check whether or not the semantics can make a custom step from a given ``CTerm``.""" + @abstractmethod def custom_step(self, c: CTerm) -> KCFGExtendResult | None: ... + """Implement a custom semantic step.""" + class DefaultSemantics(KCFGSemantics): def is_terminal(self, c: CTerm) -> bool: @@ -32,5 +45,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 58c9bb24df0..5879711b465 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -44,7 +44,23 @@ class APRProofResult: @dataclass class APRProofExtendResult(APRProofResult): - extend_result: KCFGExtendResult + """Proof extension to be applied.""" + + extension_to_apply: KCFGExtendResult + + +@dataclass +class APRProofExtendAndCacheResult(APRProofExtendResult): + """Proof extension to be cached.""" + + extension_to_cache: KCFGExtendResult + + +@dataclass +class APRProofUseCacheResult(APRProofResult): + """Proof extension to be applied using the extension cache.""" + + cached_node_id: NodeIdLike @dataclass @@ -66,6 +82,7 @@ class APRProofStep: target: KCFG.Node proof_id: str bmc_depth: int | None + use_cache: NodeIdLike | None module_name: str shortest_path_to_node: tuple[KCFG.Node, ...] prior_loops_cache: FrozenDict[int, tuple[int, ...]] = field(compare=False) @@ -99,6 +116,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, @@ -136,6 +154,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) @@ -170,11 +189,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 != [] else None + ) + steps.append( APRProofStep( bmc_depth=self.bmc_depth, module_name=module_name, node=node, + 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), @@ -188,8 +213,24 @@ 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) + # 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 + self._next_steps[result.node_id] = result.extension_to_cache + self.kcfg.extend( + extend_result=result.extension_to_apply, + 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): @@ -669,7 +710,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 @@ -682,7 +722,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, @@ -694,7 +733,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 @@ -748,6 +786,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]: + # 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: @@ -761,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)] - # Terminal checks for current node and target node + # 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) @@ -769,7 +808,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) @@ -790,20 +829,52 @@ 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 - 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 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.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( + 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, + ) + + # 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 current node is at non-zero depth + if step.nonzero_depth: + _LOGGER.info(f'Caching next step for edge starting from {step.node.id}') + 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_result=extend_result, prior_loops_cache_update=prior_loops + node_id=step.node.id, + extension_to_apply=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