Improvements to printing using new infrastructure (#593)

These are some improvements to printing that we can implement now that
we have merged changes upstream
runtimeverification/k#4808.

- Improves the printing of spans in the TUI viewer to actually print the
file name and line that it's referring to.
- Passes the entire `DisplayOpts` to the `KMIRAPRNodePrinter`, because
why not?
- Omits printing the `<currentBody>` cell by default in TUI and shower,
but enables turning it back on with `--no-omit-current-body` option to
both.
- Saves off the `SMIRInfo` in the `proof_dir` when we have it available
in `prove-rs`, so that it can be used for printing sourcemap information
in the show/view commands (like current function name and span).

---------

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

Author: 3 people

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.170"
+version = "0.3.171"
 description = ""
 requires-python = "~=3.10"
 dependencies = [

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.170'
+VERSION: Final = '0.3.171'

kmir/src/kmir/__main__.py

@@ -114,25 +114,22 @@ def _kmir_prove_raw(opts: ProveRawOpts) -> None:
 def _kmir_view(opts: ViewOpts) -> None:
     kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR)
     proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
-    smir_info = None
-    if opts.smir_info is not None:
-        smir_info = SMIRInfo.from_file(opts.smir_info)
     printer = PrettyPrinter(kmir.definition)
-    cterm_show = CTermShow(printer.print)
-    node_printer = KMIRAPRNodePrinter(cterm_show, proof, smir_info=smir_info, full_printer=False)
-    viewer = APRProofViewer(proof, kmir, node_printer=node_printer)
+    omit_labels = ('<currentBody>',) if opts.omit_current_body else ()
+    cterm_show = CTermShow(printer.print, omit_labels=omit_labels)
+    opts.full_printer = False
+    node_printer = KMIRAPRNodePrinter(cterm_show, proof, opts)
+    viewer = APRProofViewer(proof, kmir, node_printer=node_printer, cterm_show=cterm_show)
     viewer.run()
 
 
 def _kmir_show(opts: ShowOpts) -> None:
     kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR)
     proof = APRProof.read_proof_data(opts.proof_dir, opts.id)
-    smir_info = None
-    if opts.smir_info is not None:
-        smir_info = SMIRInfo.from_file(opts.smir_info)
     printer = PrettyPrinter(kmir.definition)
-    cterm_show = CTermShow(printer.print)
-    node_printer = KMIRAPRNodePrinter(cterm_show, proof, smir_info=smir_info, full_printer=opts.full_printer)
+    omit_labels = ('<currentBody>',) if opts.omit_current_body else ()
+    cterm_show = CTermShow(printer.print, omit_labels=omit_labels)
+    node_printer = KMIRAPRNodePrinter(cterm_show, proof, opts)
     shower = APRProofShow(kmir.definition, node_printer=node_printer)
     lines = shower.show(proof)
     print('\n'.join(lines))
@@ -232,6 +229,13 @@ def _arg_parser() -> ArgumentParser:
         default=None,
         help='Path to SMIR JSON file to improve debug messaging.',
     )
+    display_args.add_argument(
+        '--no-omit-current-body',
+        dest='omit_current_body',
+        default=True,
+        action='store_false',
+        help='Display the <currentBody> cell completely.',
+    )
 
     command_parser.add_parser(
         'show', help='Show a saved proof', parents=[kcli_args.logging_args, proof_args, display_args]
@@ -291,13 +295,25 @@ def _parse_args(ns: Namespace) -> KMirOpts:
             )
         case 'view':
             proof_dir = Path(ns.proof_dir).resolve()
-            return ViewOpts(proof_dir, ns.id, full_printer=ns.full_printer, smir_info=ns.smir_info)
+            return ViewOpts(
+                proof_dir,
+                ns.id,
+                full_printer=ns.full_printer,
+                smir_info=ns.smir_info,
+                omit_current_body=ns.omit_current_body,
+            )
         case 'prune':
             proof_dir = Path(ns.proof_dir).resolve()
             return PruneOpts(proof_dir, ns.id, ns.node_id)
         case 'show':
             proof_dir = Path(ns.proof_dir).resolve()
-            return ShowOpts(proof_dir, ns.id, full_printer=ns.full_printer, smir_info=ns.smir_info)
+            return ShowOpts(
+                proof_dir,
+                ns.id,
+                full_printer=ns.full_printer,
+                smir_info=ns.smir_info,
+                omit_current_body=ns.omit_current_body,
+            )
         case 'prove-rs':
             return ProveRSOpts(
                 rs_file=Path(ns.rs_file).resolve(),

kmir/src/kmir/kmir.py

@@ -35,7 +35,7 @@
     from pyk.kore.syntax import Pattern
     from pyk.utils import BugReport
 
-    from .options import ProveRSOpts
+    from .options import DisplayOpts, ProveRSOpts
 
 _LOGGER: Final = logging.getLogger(__name__)
 
@@ -166,6 +166,8 @@ def prove_rs(self, opts: ProveRSOpts) -> APRProof:
             apr_proof = self.apr_proof_from_kast(
                 label, kmir_kast, SMIRInfo(smir_json), start_symbol=opts.start_symbol, proof_dir=opts.proof_dir
             )
+            if apr_proof.proof_dir is not None and (apr_proof.proof_dir / apr_proof.id).is_dir():
+                (apr_proof.proof_dir / apr_proof.id / 'smir.json').write_text(json.dumps(smir_json))
         if apr_proof.passed:
             return apr_proof
         with self.kcfg_explore(label) as kcfg_explore:
@@ -195,14 +197,20 @@ def __init__(self, cterm_show: CTermShow, full_printer: bool = False) -> None:
 class KMIRAPRNodePrinter(KMIRNodePrinter, APRProofNodePrinter):
     smir_info: SMIRInfo | None
 
-    def __init__(
-        self, cterm_show: CTermShow, proof: APRProof, smir_info: SMIRInfo | None = None, full_printer: bool = False
-    ) -> None:
-        KMIRNodePrinter.__init__(self, cterm_show, full_printer=full_printer)
-        APRProofNodePrinter.__init__(self, proof, cterm_show, full_printer=full_printer)
-        self.smir_info = smir_info
+    def __init__(self, cterm_show: CTermShow, proof: APRProof, opts: DisplayOpts) -> None:
+        KMIRNodePrinter.__init__(self, cterm_show, full_printer=opts.full_printer)
+        APRProofNodePrinter.__init__(self, proof, cterm_show, full_printer=opts.full_printer)
+        self.smir_info = None
+        if opts.smir_info:
+            self.smir_info = SMIRInfo.from_file(opts.smir_info)
+        elif (
+            proof.proof_dir is not None
+            and (proof.proof_dir / proof.id).is_dir()
+            and (proof.proof_dir / proof.id / 'smir.json').is_file()
+        ):
+            self.smir_info = SMIRInfo.from_file(proof.proof_dir / proof.id / 'smir.json')
 
-    def _span(self, node: KCFG.Node) -> int | None:
+    def _span(self, node: KCFG.Node) -> str | None:
         curr_span: int | None = None
         span_worklist: list[KInner] = [node.cterm.cell('K_CELL')]
         while span_worklist:
@@ -218,7 +226,12 @@ def _span(self, node: KCFG.Node) -> int | None:
                 span_worklist = list(next_item.args) + span_worklist
             if type(next_item) is KSequence:
                 span_worklist = list(next_item.items) + span_worklist
-        return curr_span
+        if self.smir_info is not None and curr_span is not None and curr_span in self.smir_info.spans:
+            path, start_row, _start_column, _end_row, _end_column = self.smir_info.spans[curr_span]
+            return f'{str(path)[-30:]}:{start_row}'
+        if curr_span is not None:
+            return f'{curr_span}'
+        return None
 
     def _function_name(self, node: KCFG.Node) -> str | None:
         curr_func_ty_kast = node.cterm.cell('CURRENTFUNC_CELL')

kmir/src/kmir/options.py

@@ -132,18 +132,21 @@ def __init__(
 class DisplayOpts(ProofOpts):
     full_printer: bool
     smir_info: Path | None
+    omit_current_body: bool
 
     def __init__(
         self,
         proof_dir: Path | str,
         id: str,
         full_printer: bool = True,
         smir_info: Path | None = None,
+        omit_current_body: bool = True,
     ) -> None:
         self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
         self.id = id
         self.full_printer = full_printer
         self.smir_info = smir_info
+        self.omit_current_body = omit_current_body
 
 
 @dataclass

kmir/src/kmir/smir.py

@@ -84,6 +84,10 @@ def function_tys(self) -> dict[str, int]:
             res[name] = fun_syms[sym]
         return res
 
+    @cached_property
+    def spans(self) -> dict[int, tuple[Path, int, int, int, int]]:
+        return {id: (p, sr, sc, er, ec) for id, [p, sr, sc, er, ec] in self._smir['spans']}
+
     @staticmethod
     def _is_func(item: dict[str, dict]) -> bool:
         return 'MonoItemFn' in item['mono_item_kind']

kmir/src/tests/integration/test_integration.py

@@ -15,7 +15,7 @@
 from kmir.__main__ import _kmir_gen_spec, _kmir_prove_raw
 from kmir.build import HASKELL_DEF_DIR, LLVM_DEF_DIR
 from kmir.kmir import KMIR, KMIRAPRNodePrinter
-from kmir.options import GenSpecOpts, ProveRawOpts, ProveRSOpts
+from kmir.options import GenSpecOpts, ProveRawOpts, ProveRSOpts, ShowOpts
 from kmir.parse.parser import Parser
 from kmir.testing.fixtures import assert_or_update_show_output
 
@@ -479,9 +479,10 @@ def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> No
         else:
             assert apr_proof.failed
 
-        shower = APRProofShow(
-            kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, full_printer=False)
+        display_opts = ShowOpts(
+            rs_file.parent, apr_proof.id, full_printer=False, smir_info=None, omit_current_body=False
         )
+        shower = APRProofShow(kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, display_opts))
         show_res = '\n'.join(shower.show(apr_proof))
         assert_or_update_show_output(
             show_res, PROVING_DIR / f'show/{rs_file.stem}.expected', update=update_expected_output
@@ -511,9 +512,10 @@ def test_prove_pinocchio(kmir: KMIR, update_expected_output: bool) -> None:
     for start_symbol in start_symbols:
         prove_rs_opts.start_symbol = start_symbol
         apr_proof = kmir.prove_rs(prove_rs_opts)
-        shower = APRProofShow(
-            kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, full_printer=True)
+        display_opts = ShowOpts(
+            pinocchio_token_program.parent, apr_proof.id, full_printer=True, smir_info=None, omit_current_body=False
         )
+        shower = APRProofShow(kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, display_opts))
         show_res = '\n'.join(shower.show(apr_proof))
         assert_or_update_show_output(
             show_res,

kmir/uv.lock

@@ -1 +1 @@
-0.3.170
+0.3.171