Reusing backend information to construct KCFGs more efficiently

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(next_states[0].state):
+                (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

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()
@@ -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,17 +1349,20 @@ class Step(KCFGExtendResult):
     logs: tuple[LogEntry, ...]
     rule_labels: list[str]
     cut: bool = field(default=False)
+    info: str = field(default='')
 
 
 @final
 @dataclass(frozen=True)
 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

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

pyk/src/pyk/proof/reachability.py

@@ -44,7 +44,19 @@ class APRProofResult:
 
 @dataclass
 class APRProofExtendResult(APRProofResult):
-    extend_result: KCFGExtendResult
+    """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)
 
 
 @dataclass
@@ -66,8 +78,10 @@ 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
     prior_loops_cache: FrozenDict[int, tuple[int, ...]] = field(compare=False)
     circularity: bool
     nonzero_depth: bool
@@ -99,6 +113,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 +151,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 +186,18 @@ 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,
+                    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),
@@ -189,7 +212,26 @@ 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 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
+                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(
+                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):
@@ -669,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
@@ -682,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,
@@ -694,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
@@ -748,6 +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]:
+        # 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,15 +801,15 @@ 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)
 
         terminal_result: 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 +830,48 @@ 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,
-        )
+        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
+        # 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,
+            )
+
+        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
+        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}')
+                to_cache = True
+            # Otherwise, discard the second result
+            else:
+                extend_results = [extend_results[0]]
+
         return [
             APRProofExtendResult(
-                node_id=step.node.id, extend_result=extend_result, prior_loops_cache_update=prior_loops
+                node_id=step.node.id,
+                extend_results=extend_results,
+                prior_loops_cache_update=prior_loops,
+                to_cache=to_cache,
+                use_cache=use_cache,
             )
         ]