APRProof specific proof state visualization (runtimeverification/pyk#489)

Fixes: #413 

This PR introduces proof-specific viewers, and does a few refactors to
make that possible:

- Helpers are added to `KCFG` for turning into modules, including:
- `KCFG.Split.covers` which returns each individual split as a reverse
cover.
- `KCFG.NDBranch.edges`, which returns each non-deterministic step as an
edge.
- `KCFG.Edge.to_rule`, which converts an edge into a K rule (or claim).
- Small refactorings to `KCFGShow` structure:
- `KCFGShow.dot` returns a `Digraph` directly (for further manipulation)
instead of a list of `str`.
- `KCFGShow.to_module` which returns a `KFlatModule` is factored out and
used directly in `KCFGShow.show`.
- Helper methods embedded in other methods in `KCFGShow` are factored
out directly to staticmethods of `KCFGShow` so they can be reused
easily.
- We just treat `stuck` as a node attribute now, printed at the
beginning of a node, instead of printing it a second time following a
node too.
- The way that `KCFGShow` calculates node attributes is adjusted and
factor out.
- A new class `NodePrinter` is factored out, which by default just uses
the attributes the `KCFG` knows about for printing out nodes.
- That class is extended by `APRProofNodePrinter` and
`APRBMCProofNodePrinter`, which add the additional information about the
nodes `pending,terminal,bounded` state. If a node is `terminal` or
`bounded`, then the `stuck` attribute is no longer printed for less
confusion.
- `KCFGShow` now takes an optional `*NodePrinter` as an argument (or
builds on itself), so instantiating that class is how you can customize
how nodes are displayed in text.
- The tests are adapted to use the more specific `*NodePrinter` classes,
and the output checked that the more specific node information is indeed
being included.
- Adds helper predicates `APRProof.is_{pending,terminal}` and
`APRProof.is_bounded`, which should behave better in case there are
qualified node ids passed in.

---------

Co-authored-by: devops <[email protected]>

Author: ehildenb

pyk/package/version

@@ -1 +1 @@
-0.1.334
+0.1.335

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.334"
+version = "0.1.335"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

pyk/src/pyk/kcfg/kcfg.py

@@ -7,7 +7,8 @@
 from threading import RLock
 from typing import TYPE_CHECKING, List, Union, cast, final
 
-from ..cterm import CSubst, CTerm
+from ..cterm import CSubst, CTerm, build_claim, build_rule
+from ..kast.inner import KApply
 from ..kast.manip import (
     bool_to_ml_pred,
     extract_lhs,
@@ -24,7 +25,7 @@
     from typing import Any
 
     from ..kast.inner import KInner
-    from ..kast.outer import KClaim, KDefinition
+    from ..kast.outer import KClaim, KDefinition, KRuleLike
 
 
 NodeIdLike = int | str
@@ -79,6 +80,22 @@ def to_dict(self) -> dict[str, Any]:
                 'depth': self.depth,
             }
 
+        def to_rule(self, label: str, claim: bool = False, priority: int | None = None) -> KRuleLike:
+            def is_ceil_condition(kast: KInner) -> bool:
+                return type(kast) is KApply and kast.label.name == '#Ceil'
+
+            sentence_id = f'{label}-{self.source.id}-TO-{self.target.id}'
+            init_constraints = [c for c in self.source.cterm.constraints if not is_ceil_condition(c)]
+            init_cterm = CTerm(self.source.cterm.config, init_constraints)
+            target_constraints = [c for c in self.target.cterm.constraints if not is_ceil_condition(c)]
+            target_cterm = CTerm(self.target.cterm.config, target_constraints)
+            rule: KRuleLike
+            if claim:
+                rule, _ = build_claim(sentence_id, init_cterm, target_cterm)
+            else:
+                rule, _ = build_rule(sentence_id, init_cterm, target_cterm, priority=priority)
+            return rule
+
     @final
     @dataclass(frozen=True)
     class Cover(EdgeLike):
@@ -139,6 +156,10 @@ def to_dict(self) -> dict[str, Any]:
         def with_single_target(self, target: KCFG.Node) -> KCFG.Split:
             return KCFG.Split(self.source, ((target, self.splits[target.id]),))
 
+        @property
+        def covers(self) -> tuple[KCFG.Cover, ...]:
+            return tuple(KCFG.Cover(target, self.source, csubst) for target, csubst in self._targets)
+
     @final
     @dataclass(frozen=True)
     class NDBranch(MultiEdge):
@@ -162,6 +183,10 @@ def to_dict(self) -> dict[str, Any]:
         def with_single_target(self, target: KCFG.Node) -> KCFG.NDBranch:
             return KCFG.NDBranch(self.source, (target,))
 
+        @property
+        def edges(self) -> tuple[KCFG.Edge, ...]:
+            return tuple(KCFG.Edge(self.source, target, 1) for target in self.targets)
+
     _node_id: int
     _nodes: dict[int, Node]
     _edges: dict[int, dict[int, Edge]]

pyk/src/pyk/kcfg/show.py

@@ -5,7 +5,6 @@
 
 from graphviz import Digraph
 
-from ..cterm import CTerm, build_claim, build_rule
 from ..kast.inner import KApply, KRewrite, top_down
 from ..kast.manip import (
     flatten_label,
@@ -22,29 +21,40 @@
 from .kcfg import KCFG
 
 if TYPE_CHECKING:
-    from collections.abc import Callable, Iterable
+    from collections.abc import Iterable
     from pathlib import Path
     from typing import Final
 
     from ..kast import KInner
-    from ..kast.outer import KRuleLike
+    from ..kast.outer import KDefinition
     from ..ktool.kprint import KPrint
     from .kcfg import NodeIdLike
 
 _LOGGER: Final = logging.getLogger(__name__)
 
 
-class KCFGShow:
+class NodePrinter:
     kprint: KPrint
+    full_printer: bool
+    minimize: bool
 
-    def __init__(
-        self,
-        kprint: KPrint,
-    ):
+    def __init__(self, kprint: KPrint, full_printer: bool = False, minimize: bool = False):
         self.kprint = kprint
+        self.full_printer = full_printer
+        self.minimize = minimize
+
+    def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
+        attrs = self.node_attrs(kcfg, node)
+        attr_str = ' (' + ', '.join(attrs) + ')' if attrs else ''
+        node_strs = [f'{node.id}{attr_str}']
+        if self.full_printer:
+            kast = node.cterm.kast
+            if self.minimize:
+                kast = minimize_term(kast)
+            node_strs.extend(' ' + line for line in self.kprint.pretty_print(kast).split('\n'))
+        return node_strs
 
-    @staticmethod
-    def node_attrs(kcfg: KCFG, node: KCFG.Node) -> list[str]:
+    def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
         attrs = []
         if kcfg.is_init(node.id):
             attrs.append('init')
@@ -60,25 +70,43 @@ def node_attrs(kcfg: KCFG, node: KCFG.Node) -> list[str]:
             attrs.append('leaf')
         if kcfg.is_split(node.id):
             attrs.append('split')
+        attrs.extend(['@' + alias for alias in sorted(kcfg.aliases(node.id))])
         return attrs
 
+
+class KCFGShow:
+    kprint: KPrint
+    node_printer: NodePrinter
+
+    def __init__(self, kprint: KPrint, node_printer: NodePrinter | None = None):
+        self.kprint = kprint
+        self.node_printer = node_printer if node_printer is not None else NodePrinter(kprint)
+
+    def node_short_info(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
+        return self.node_printer.print_node(kcfg, node)
+
     @staticmethod
-    def node_short_info(
-        kcfg: KCFG, node: KCFG.Node, node_printer: Callable[[CTerm], Iterable[str]] | None = None
-    ) -> list[str]:
-        attrs = KCFGShow.node_attrs(kcfg, node) + ['@' + alias for alias in sorted(kcfg.aliases(node.id))]
-        attr_string = ' (' + ', '.join(attrs) + ')' if attrs else ''
-        node_header = str(node.id) + attr_string
-        node_strs = [node_header]
-        if node_printer:
-            node_strs.extend(f' {nl}' for nl in node_printer(node.cterm))
-        return node_strs
+    def hide_cells(term: KInner, omit_cells: Iterable[str]) -> KInner:
+        def _hide_cells(_k: KInner) -> KInner:
+            if type(_k) == KApply and _k.label.name in omit_cells:
+                return DOTS
+            return _k
+
+        if omit_cells:
+            return top_down(_hide_cells, term)
+        return term
+
+    @staticmethod
+    def simplify_config(defn: KDefinition, config: KInner, omit_cells: Iterable[str]) -> KInner:
+        config = inline_cell_maps(config)
+        config = sort_ac_collections(defn, config)
+        config = KCFGShow.hide_cells(config, omit_cells)
+        return config
 
     def pretty_segments(
         self,
         kcfg: KCFG,
         minimize: bool = True,
-        node_printer: Callable[[CTerm], Iterable[str]] | None = None,
     ) -> Iterable[tuple[str, Iterable[str]]]:
         """Return a pretty version of the KCFG in segments.
 
@@ -90,17 +118,8 @@ def pretty_segments(
         processed_nodes: list[KCFG.Node] = []
         ret_lines: list[tuple[str, list[str]]] = []
 
-        def _bold(text: str) -> str:
-            return '\033[1m' + text + '\033[0m'
-
-        def _green(text: str) -> str:
-            return '\033[32m' + text + '\033[0m'
-
         def _print_node(node: KCFG.Node) -> list[str]:
-            short_info = KCFGShow.node_short_info(kcfg, node, node_printer=node_printer)
-            if kcfg.is_frontier(node.id):
-                short_info[0] = _bold(short_info[0])
-            return short_info
+            return self.node_short_info(kcfg, node)
 
         def _print_edge(edge: KCFG.Edge) -> list[str]:
             if edge.depth == 1:
@@ -170,8 +189,6 @@ def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: list[KCFG
                     suffix = ['(looped back)', '']
                 elif processed and not kcfg.is_target(curr_node.id):
                     suffix = ['(continues as previously)', '']
-                elif kcfg.is_stuck(curr_node.id):
-                    suffix = ['(stuck)', '']
                 else:
                     suffix = ['']
             ret_node_lines.append(indent + elbow + ' ' + curr_node_strs[0])
@@ -286,17 +303,8 @@ def pretty(
         self,
         kcfg: KCFG,
         minimize: bool = True,
-        node_printer: Callable[[CTerm], Iterable[str]] | None = None,
     ) -> Iterable[str]:
-        return (
-            line
-            for _, seg_lines in self.pretty_segments(
-                kcfg,
-                minimize=minimize,
-                node_printer=node_printer,
-            )
-            for line in seg_lines
-        )
+        return (line for _, seg_lines in self.pretty_segments(kcfg, minimize=minimize) for line in seg_lines)
 
     def show(
         self,
@@ -307,37 +315,17 @@ def show(
         to_module: bool = False,
         minimize: bool = True,
         sort_collections: bool = False,
-        node_printer: Callable[[CTerm], Iterable[str]] | None = None,
         omit_cells: Iterable[str] = (),
     ) -> list[str]:
         res_lines: list[str] = []
-        res_lines += self.pretty(cfg, minimize=minimize, node_printer=node_printer)
-
-        def hide_cells(term: KInner) -> KInner:
-            def _hide_cells(_k: KInner) -> KInner:
-                if type(_k) == KApply and _k.label.name in omit_cells:
-                    return DOTS
-                return _k
-
-            if omit_cells:
-                return top_down(_hide_cells, term)
-            return term
-
-        def simplify_config(config: KInner) -> KInner:
-            config = inline_cell_maps(config)
-            config = sort_ac_collections(self.kprint.definition, config)
-            config = hide_cells(config)
-            return config
-
-        def is_ceil_condition(kast: KInner) -> bool:
-            return type(kast) is KApply and kast.label.name == '#Ceil'
+        res_lines += self.pretty(cfg, minimize=minimize)
 
         nodes_printed = False
 
         for node_id in nodes:
             nodes_printed = True
             kast = cfg.node(node_id).cterm.kast
-            kast = hide_cells(kast)
+            kast = KCFGShow.hide_cells(kast, omit_cells)
             if minimize:
                 kast = minimize_term(kast)
             res_lines.append('')
@@ -349,8 +337,8 @@ def is_ceil_condition(kast: KInner) -> bool:
 
         for node_id_1, node_id_2 in node_deltas:
             nodes_printed = True
-            config_1 = simplify_config(cfg.node(node_id_1).cterm.config)
-            config_2 = simplify_config(cfg.node(node_id_2).cterm.config)
+            config_1 = KCFGShow.simplify_config(self.kprint.definition, cfg.node(node_id_1).cterm.config, omit_cells)
+            config_2 = KCFGShow.simplify_config(self.kprint.definition, cfg.node(node_id_2).cterm.config, omit_cells)
             config_delta = push_down_rewrites(KRewrite(config_1, config_2))
             if minimize:
                 config_delta = minimize_term(config_delta)
@@ -367,35 +355,39 @@ def is_ceil_condition(kast: KInner) -> bool:
         res_lines.append('')
 
         if to_module:
-
-            def to_rule(edge: KCFG.Edge, *, claim: bool = False) -> KRuleLike:
-                sentence_id = f'BASIC-BLOCK-{edge.source.id}-TO-{edge.target.id}'
-                init_constraints = [c for c in edge.source.cterm.constraints if not is_ceil_condition(c)]
-                init_cterm = CTerm(simplify_config(edge.source.cterm.config), init_constraints)
-                target_constraints = [c for c in edge.target.cterm.constraints if not is_ceil_condition(c)]
-                target_cterm = CTerm(simplify_config(edge.target.cterm.config), target_constraints)
-                rule: KRuleLike
-                if claim:
-                    rule, _ = build_claim(sentence_id, init_cterm, target_cterm)
-                else:
-                    rule, _ = build_rule(sentence_id, init_cterm, target_cterm, priority=35)
-                return rule
-
-            rules = [to_rule(e) for e in cfg.edges()]
-            nd_steps = [
-                to_rule(KCFG.Edge(ndbranch.source, target, 1))
-                for ndbranch in cfg.ndbranches()
-                for target in ndbranch.targets
-            ]
-            claims = [to_rule(KCFG.Edge(nd, cfg.get_unique_target(), -1), claim=True) for nd in cfg.frontier]
-            cfg_module_name = cfgid.upper().replace('.', '-').replace('_', '-')
-            new_module = KFlatModule(f'SUMMARY-{cfg_module_name}', rules + nd_steps + claims)
-            res_lines.append(self.kprint.pretty_print(new_module, sort_collections=sort_collections))
-            res_lines.append('')
+            module = self.to_module(cfgid, cfg, omit_cells=omit_cells)
+            res_lines.append(self.kprint.pretty_print(module, sort_collections=sort_collections))
 
         return res_lines
 
-    def dot(self, kcfg: KCFG, node_printer: Callable[[CTerm], Iterable[str]] | None = None) -> str:
+    def to_module(
+        self,
+        cfgid: str,
+        cfg: KCFG,
+        module_name: str | None = None,
+        imports: Iterable[str] = (),
+        omit_cells: Iterable[str] = (),
+    ) -> KFlatModule:
+        rules = [e.to_rule('BASIC-BLOCK') for e in cfg.edges()]
+        rules = [
+            r.let(body=KCFGShow.simplify_config(self.kprint.definition, r.body, omit_cells=omit_cells)) for r in rules
+        ]
+        nd_steps = [edge.to_rule('ND-STEP') for ndbranch in cfg.ndbranches() for edge in ndbranch.edges]
+        nd_steps = [
+            r.let(body=KCFGShow.simplify_config(self.kprint.definition, r.body, omit_cells=omit_cells))
+            for r in nd_steps
+        ]
+        claims = [KCFG.Edge(nd, cfg.get_unique_target(), -1).to_rule('UNPROVEN', claim=True) for nd in cfg.frontier]
+        claims = [
+            c.let(body=KCFGShow.simplify_config(self.kprint.definition, c.body, omit_cells=omit_cells)) for c in claims
+        ]
+
+        cfg_module_name = (
+            module_name if module_name is not None else f'SUMMARY-{cfgid.upper().replace(".", "-").replace("_", "-")}'
+        )
+        return KFlatModule(cfg_module_name, rules + nd_steps + claims)
+
+    def dot(self, kcfg: KCFG) -> Digraph:
         def _short_label(label: str) -> str:
             return '\n'.join(
                 [
@@ -407,8 +399,8 @@ def _short_label(label: str) -> str:
         graph = Digraph()
 
         for node in kcfg.nodes:
-            label = '\n'.join(KCFGShow.node_short_info(kcfg, node, node_printer=node_printer))
-            class_attrs = ' '.join(KCFGShow.node_attrs(kcfg, node))
+            label = '\n'.join(self.node_short_info(kcfg, node))
+            class_attrs = ' '.join(self.node_printer.node_attrs(kcfg, node))
             attrs = {'class': class_attrs} if class_attrs else {}
             graph.node(name=node.id, label=label, **attrs)
 
@@ -445,24 +437,17 @@ def _short_label(label: str) -> str:
                 attrs = {'class': 'target', 'style': 'solid'}
                 graph.edge(tail_name=node.id, head_name=target_id, label='  false', **attrs)
 
-        return graph.source
+        return graph
 
-    def dump(
-        self,
-        cfgid: str,
-        cfg: KCFG,
-        dump_dir: Path,
-        dot: bool = False,
-        node_printer: Callable[[CTerm], Iterable[str]] | None = None,
-    ) -> None:
+    def dump(self, cfgid: str, cfg: KCFG, dump_dir: Path, dot: bool = False) -> None:
         ensure_dir_path(dump_dir)
 
         cfg_file = dump_dir / f'{cfgid}.json'
         cfg_file.write_text(cfg.to_json())
         _LOGGER.info(f'Wrote CFG file {cfgid}: {cfg_file}')
 
         if dot:
-            cfg_dot = self.dot(cfg, node_printer=node_printer)
+            cfg_dot = self.dot(cfg)
             dot_file = dump_dir / f'{cfgid}.dot'
             dot_file.write_text(cfg_dot)
             _LOGGER.info(f'Wrote DOT file {cfgid}: {dot_file}')