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