diff --git a/README.md b/README.md index 5e66b9fa8..bba94ad23 100644 --- a/README.md +++ b/README.md @@ -96,11 +96,46 @@ uv --project kmir run kmir link file1.smir.json file2.smir.json file3.smir.json uv --project kmir run kmir link file1.smir.json file2.smir.json ``` +**`kmir info`** - Inspect SMIR JSON metadata (currently: types) +```bash +# Show information about specific type IDs in a SMIR JSON +uv --project kmir run kmir info path/to/program.smir.json --types "1,2,3" + +# Notes +# - The --types option accepts a comma-separated list of numeric Stable MIR type IDs. +# - Output format: one line per requested type, e.g.: +# Type Ty(1): Int(....) +# Type Ty(2): StructT(name=..., adt_def=..., fields=[...]) +# - If --types is omitted, the command currently produces no output. +``` + ### Analysis Commands -**`kmir show`** - Display proof information +**`kmir show`** - Display proof information with advanced filtering options ```bash +# Basic usage uv --project kmir run kmir show proof_id --proof-dir ./proof_dir + +# Show specific nodes only +uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3" + +# Show node deltas (transitions between specific nodes) +uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2,3:4" + +# Display full node information (default is compact) +uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer + +# Show static information cells (functions, types, etc.) +uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-static-info + +# Show current body cell content +uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-current-body + +# Omit specific cells from output +uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --omit-cells "cell1,cell2" + +# Combine multiple options for detailed analysis +uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info --nodes "1,2" --verbose ``` **`kmir view`** - Detailed view of proof results @@ -128,7 +163,16 @@ uv --project kmir run kmir show-rules proof_id source_node target_node --proof-d 3. **View Results**: ```bash + # Quick overview (compact format, static info hidden) uv --project kmir run kmir show proof_id --proof-dir ./proof_dir + + # Detailed analysis with full information + uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info + + # Focus on specific nodes + uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3" + + # Interactive view uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose ``` @@ -137,6 +181,32 @@ uv --project kmir run kmir show-rules proof_id source_node target_node --proof-d uv --project kmir run kmir show-rules proof_id 1 3 --proof-dir ./proof_dir ``` +### Advanced Show Usage Examples + +**Debugging workflow:** +```bash +# 1. Start with a quick overview +uv --project kmir run kmir show my_proof --proof-dir ./proofs + +# 2. Focus on problematic nodes (e.g., nodes 5, 6, 7) +uv --project kmir run kmir show my_proof --proof-dir ./proofs --nodes "5,6,7" + +# 3. Examine transitions between specific nodes +uv --project kmir run kmir show my_proof --proof-dir ./proofs --node-deltas "5:6,6:7" + +# 4. Get full details for deep debugging +uv --project kmir run kmir show my_proof --proof-dir ./proofs --nodes "6" --full-printer --no-omit-static-info --no-omit-current-body +``` + +**Performance analysis:** +```bash +# Hide verbose cells but show execution flow +uv --project kmir run kmir show my_proof --proof-dir ./proofs --omit-cells "locals,heap" --verbose + +# Focus on function calls and type information +uv --project kmir run kmir show my_proof --proof-dir ./proofs --no-omit-static-info --omit-cells "currentBody" +``` + ### Command Options Most commands support: @@ -146,6 +216,15 @@ Most commands support: - `--max-depth DEPTH`: Maximum execution depth - `--max-iterations ITERATIONS`: Maximum iterations +**`kmir show` specific options:** +- `--nodes NODES`: Comma separated list of node IDs to show (e.g., "1,2,3") +- `--node-deltas DELTAS`: Comma separated list of node deltas in format "source:target" (e.g., "1:2,3:4") +- `--omit-cells CELLS`: Comma separated list of cell names to omit from output +- `--full-printer`: Display the full node in output (default is compact) +- `--no-omit-static-info`: Display static information cells (functions, start-symbol, types, adt-to-ty) +- `--no-omit-current-body`: Display the `` cell completely +- `--smir-info SMIR_INFO`: Path to SMIR JSON file to improve debug messaging + For complete options, use `--help` with each command. ### Supporters diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index ad212d576..1b742b356 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -20,6 +20,7 @@ from .linker import link from .options import ( GenSpecOpts, + InfoOpts, LinkOpts, ProveRawOpts, ProveRSOpts, @@ -30,7 +31,7 @@ ViewOpts, ) from .parse.parser import parse_json -from .smir import SMIRInfo +from .smir import SMIRInfo, Ty if TYPE_CHECKING: from argparse import Namespace @@ -130,14 +131,38 @@ def _kmir_view(opts: ViewOpts) -> None: def _kmir_show(opts: ShowOpts) -> None: + from pyk.kast.pretty import PrettyPrinter + + from .kprint import KMIRPrettyPrinter + kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR) proof = APRProof.read_proof_data(opts.proof_dir, opts.id) - printer = PrettyPrinter(kmir.definition) - omit_labels = ('',) if opts.omit_current_body else () - cterm_show = CTermShow(printer.print, omit_labels=omit_labels) + + # Use custom KMIR printer by default, switch to standard printer if requested + if opts.use_default_printer: + printer = PrettyPrinter(kmir.definition) + _LOGGER.info('Using standard PrettyPrinter') + else: + printer = KMIRPrettyPrinter(kmir.definition) + _LOGGER.info('Using custom KMIRPrettyPrinter') + + all_omit_cells = list(opts.omit_cells or ()) + if opts.omit_current_body: + all_omit_cells.append('') + + cterm_show = CTermShow(printer.print, omit_labels=tuple(all_omit_cells)) node_printer = KMIRAPRNodePrinter(cterm_show, proof, opts) shower = APRProofShow(kmir.definition, node_printer=node_printer) - lines = shower.show(proof) + shower.kcfg_show.pretty_printer = printer + _LOGGER.info( + f'Showing {proof.id} with\n nodes: {opts.nodes},\n node_deltas: {opts.node_deltas},\n omit_cells: {tuple(all_omit_cells)}' + ) + lines = shower.show( + proof, + nodes=opts.nodes or (), + node_deltas=opts.node_deltas or (), + omit_cells=tuple(all_omit_cells), + ) print('\n'.join(lines)) @@ -164,6 +189,16 @@ def _kmir_prune(opts: PruneOpts) -> None: proof.write_proof_data() +def _kmir_info(opts: InfoOpts) -> None: + smir_info = SMIRInfo.from_file(opts.smir_file) + + if opts.types: + print(f'\nTypes requested: {opts.types}') + chosen_types = [Ty(type_id) for type_id in opts.types] + for type_id in chosen_types: + print(f'Type {type_id}: {smir_info.unref_type(type_id)}') + + def _kmir_link(opts: LinkOpts) -> None: result = link([SMIRInfo.from_file(f) for f in opts.smir_files]) result.dump(opts.output_file) @@ -178,6 +213,8 @@ def kmir(args: Sequence[str]) -> None: _kmir_run(opts) case GenSpecOpts(): _kmir_gen_spec(opts) + case InfoOpts(): + _kmir_info(opts) case ProveRawOpts(): _kmir_prove_raw(opts) case ViewOpts(): @@ -221,6 +258,12 @@ def _arg_parser() -> ArgumentParser: '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from' ) + info_parser = command_parser.add_parser( + 'info', help='Show information about a SMIR JSON file', parents=[kcli_args.logging_args] + ) + info_parser.add_argument('smir_file', metavar='FILE', help='SMIR JSON file to analyze') + info_parser.add_argument('--types', metavar='TYPES', help='Comma separated list of type IDs to show details for') + prove_args = ArgumentParser(add_help=False) prove_args.add_argument('--proof-dir', metavar='DIR', help='Proof directory') prove_args.add_argument('--bug-report', metavar='PATH', help='path to optional bug report') @@ -247,11 +290,11 @@ def _arg_parser() -> ArgumentParser: display_args = ArgumentParser(add_help=False) display_args.add_argument( - '--no-full-printer', + '--full-printer', dest='full_printer', - action='store_false', - default=True, - help='Do not display the full node in output.', + action='store_true', + default=False, + help='Display the full node in output.', ) display_args.add_argument( '--smir-info', @@ -268,9 +311,30 @@ def _arg_parser() -> ArgumentParser: help='Display the cell completely.', ) - command_parser.add_parser( + show_parser = command_parser.add_parser( 'show', help='Show proof information', parents=[kcli_args.logging_args, proof_args, display_args] ) + show_parser.add_argument('--nodes', metavar='NODES', help='Comma separated list of node IDs to show') + show_parser.add_argument( + '--node-deltas', metavar='DELTAS', help='Comma separated list of node deltas in format "source:target"' + ) + show_parser.add_argument( + '--omit-cells', metavar='CELLS', help='Comma separated list of cell names to omit from output' + ) + show_parser.add_argument( + '--no-omit-static-info', + dest='omit_static_info', + action='store_false', + default=True, + help='Display static information cells (functions, start-symbol, types, adt-to-ty)', + ) + show_parser.add_argument( + '--use-default-printer', + dest='use_default_printer', + action='store_true', + default=False, + help='Use standard PrettyPrinter instead of custom KMIR printer', + ) show_rules_parser = command_parser.add_parser( 'show-rules', help='Show rules applied on a specific edge', parents=[kcli_args.logging_args, proof_args] @@ -324,6 +388,8 @@ def _parse_args(ns: Namespace) -> KMirOpts: ) case 'gen-spec': return GenSpecOpts(input_file=Path(ns.input_file), output_file=ns.output_file, start_symbol=ns.start_symbol) + case 'info': + return InfoOpts(smir_file=Path(ns.smir_file), types=ns.types) case 'prove': proof_dir = Path(ns.proof_dir) return ProveRawOpts( @@ -343,6 +409,11 @@ def _parse_args(ns: Namespace) -> KMirOpts: full_printer=ns.full_printer, smir_info=Path(ns.smir_info) if ns.smir_info else None, omit_current_body=ns.omit_current_body, + nodes=ns.nodes, + node_deltas=ns.node_deltas, + omit_cells=ns.omit_cells, + omit_static_info=ns.omit_static_info, + use_default_printer=ns.use_default_printer, ) case 'show-rules': return ShowRulesOpts( diff --git a/kmir/src/kmir/kprint.py b/kmir/src/kmir/kprint.py new file mode 100644 index 000000000..21887dd59 --- /dev/null +++ b/kmir/src/kmir/kprint.py @@ -0,0 +1,28 @@ +from __future__ import annotations + +import logging +from typing import TYPE_CHECKING + +from pyk.kast.pretty import PrettyPrinter, indent + +_LOGGER: logging.Logger = logging.getLogger(__name__) + +if TYPE_CHECKING: + from pyk.kast.outer import KDefinition + + +class KMIRPrettyPrinter(PrettyPrinter): + """ + Custom Pretty Printer for improved ListItem display formatting. + Formats ListItem elements with line breaks for better readability. + """ + + def __init__(self, definition: KDefinition) -> None: + """ + Initialize KMIR Pretty Printer + + Args: + definition: K definition + """ + super().__init__(definition) + self.symbol_table['ListItem'] = lambda *args: 'ListItem (' + (indent(', '.join(args))).strip() + ')\n' diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index bb34a02ae..b2acc6459 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -138,7 +138,7 @@ def __init__( self, proof_dir: Path | str, id: str, - full_printer: bool = True, + full_printer: bool = False, smir_info: Path | None = None, omit_current_body: bool = True, ) -> None: @@ -150,7 +150,48 @@ def __init__( @dataclass -class ShowOpts(DisplayOpts): ... +class ShowOpts(DisplayOpts): + nodes: tuple[int, ...] | None + node_deltas: tuple[tuple[int, int], ...] | None + omit_cells: tuple[str, ...] | None + omit_static_info: bool + use_default_printer: bool + + def __init__( + self, + proof_dir: Path | str, + id: str, + full_printer: bool = False, + smir_info: Path | None = None, + omit_current_body: bool = True, + nodes: str | None = None, + node_deltas: str | None = None, + omit_cells: str | None = None, + omit_static_info: bool = True, + use_default_printer: bool = False, + ) -> None: + super().__init__(proof_dir, id, full_printer, smir_info, omit_current_body) + self.omit_static_info = omit_static_info + self.use_default_printer = use_default_printer + self.nodes = tuple(int(n.strip()) for n in nodes.split(',')) if nodes is not None else None + if node_deltas is not None: + deltas = [] + for delta in node_deltas.split(','): + parts = delta.strip().split(':') + if len(parts) == 2: + deltas.append((int(parts[0].strip()), int(parts[1].strip()))) + self.node_deltas = tuple(deltas) + else: + self.node_deltas = None + + static_info_cells = ('', '', '', '') + + user_omit_cells = tuple(cell.strip() for cell in omit_cells.split(',')) if omit_cells is not None else () + + if omit_static_info: + self.omit_cells = static_info_cells + user_omit_cells + else: + self.omit_cells = user_omit_cells if user_omit_cells else None @dataclass @@ -180,6 +221,16 @@ class PruneOpts(ProofOpts): node_id: int +@dataclass +class InfoOpts(KMirOpts): + smir_file: Path + types: tuple[int, ...] | None + + def __init__(self, smir_file: Path, types: str | None = None) -> None: + self.smir_file = smir_file + self.types = tuple(int(t.strip()) for t in types.split(',')) if types is not None else None + + @dataclass class LinkOpts(KMirOpts): smir_files: list[Path] diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 0c23e0c98..f4ca22fcc 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -35,6 +35,24 @@ def dump(self, smir_json_file: Path) -> None: def types(self) -> dict[Ty, TypeMetadata]: return {Ty(id): metadata_from_json(type) for id, type in self._smir['types']} + def unref_type(self, ty: Ty) -> TypeMetadata | None: + """Recursively resolve type until reaching a non-reference type.""" + if ty not in self.types: + _LOGGER.warning(f'Type {ty} not found in types') + return None + type_info = self.types[ty] + while isinstance(type_info, RefT): + if Ty(type_info.pointee_type) not in self.types: + _LOGGER.info(f'Pointee type {Ty(type_info.pointee_type)} not found in types for reference type {ty}') + return type_info + type_info = self.types[Ty(type_info.pointee_type)] + return type_info + + @cached_property + def unref_types(self) -> dict[Ty, TypeMetadata | None]: + """Returns a dictionary of all types and their unreferenced versions.""" + return {ty: self.unref_type(ty) for ty in self.types.keys()} + @cached_property def adt_defs(self) -> dict[AdtDef, Ty]: res = {} diff --git a/kmir/src/tests/integration/data/prove-rs/show/arith.smir.cli-info.expected b/kmir/src/tests/integration/data/prove-rs/show/arith.smir.cli-info.expected new file mode 100644 index 000000000..37b6fa5cd --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/arith.smir.cli-info.expected @@ -0,0 +1,5 @@ + +Types requested: (1, 5, 6) +Type 1: TupleT(components=[]) +Type 5: RefT(pointee_type=33) +Type 6: Int(info=) \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected new file mode 100644 index 000000000..fb58b9478 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected @@ -0,0 +1,14 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: src/rust/library/std/src/rt.rs:194 +│ +│ (6 steps) +├─ 3 (terminal) +│ #EndProgram ~> .K +│ function: main +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + #EndProgram ~> .K \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected new file mode 100644 index 000000000..fb58b9478 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected @@ -0,0 +1,14 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: src/rust/library/std/src/rt.rs:194 +│ +│ (6 steps) +├─ 3 (terminal) +│ #EndProgram ~> .K +│ function: main +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + #EndProgram ~> .K \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-prune.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-prune.expected new file mode 100644 index 000000000..9c16c71fb --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-prune.expected @@ -0,0 +1 @@ +Pruned nodes: [] \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/show/link.arith.smir+unary.smir.counts.expected b/kmir/src/tests/integration/data/prove-rs/show/link.arith.smir+unary.smir.counts.expected new file mode 100644 index 000000000..eeed67f91 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/link.arith.smir+unary.smir.counts.expected @@ -0,0 +1,5 @@ +name: arith,unary +types: 40 +functions: 19 +items: 20 +spans: 130 \ No newline at end of file diff --git a/kmir/src/tests/integration/test_cli.py b/kmir/src/tests/integration/test_cli.py new file mode 100644 index 000000000..36f77c001 --- /dev/null +++ b/kmir/src/tests/integration/test_cli.py @@ -0,0 +1,125 @@ +from __future__ import annotations + +import json +from pathlib import Path +from typing import TYPE_CHECKING + +from kmir.__main__ import _kmir_info, _kmir_link, _kmir_prune, _kmir_show +from kmir.options import InfoOpts, LinkOpts, ProveRSOpts, PruneOpts, ShowOpts +from kmir.smir import SMIRInfo +from kmir.testing.fixtures import assert_or_update_show_output + +if TYPE_CHECKING: + import pytest + from pyk.proof import APRProof + + from kmir.kmir import KMIR + +PROVE_RS_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True) + + +def _prove_and_store( + kmir: KMIR, rs_or_json: Path, tmp_path: Path, start_symbol: str = 'main', is_smir: bool = False +) -> APRProof: + opts = ProveRSOpts(rs_or_json, proof_dir=tmp_path, smir=is_smir, start_symbol=start_symbol) + apr_proof = kmir.prove_rs(opts) + apr_proof.write_proof_data() + return apr_proof + + +def test_cli_show_printers_snapshot( + kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str], update_expected_output: bool +) -> None: + rs_file = PROVE_RS_DIR / 'assert-true.rs' + start_symbol = 'main' + apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False) + + # Custom KMIRPrettyPrinter + show_opts_custom = ShowOpts( + proof_dir=tmp_path, + id=apr_proof.id, + full_printer=False, + smir_info=None, + omit_current_body=False, + use_default_printer=False, + ) + _kmir_show(show_opts_custom) + out_custom = capsys.readouterr().out.rstrip() + assert_or_update_show_output( + out_custom, + PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-custom-printer.expected', + update=update_expected_output, + ) + + # Standard PrettyPrinter + show_opts_default = ShowOpts( + proof_dir=tmp_path, + id=apr_proof.id, + full_printer=False, + smir_info=None, + omit_current_body=False, + use_default_printer=True, + ) + _kmir_show(show_opts_default) + out_default = capsys.readouterr().out.rstrip() + assert_or_update_show_output( + out_default, + PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-default-printer.expected', + update=update_expected_output, + ) + + +def test_cli_info_snapshot(capsys: pytest.CaptureFixture[str], update_expected_output: bool) -> None: + smir_json = PROVE_RS_DIR / 'arith.smir.json' + smir_info = SMIRInfo.from_file(smir_json) + # choose first few type ids deterministically + chosen_tys = sorted(smir_info.types.keys())[:3] + types_arg = ','.join(str(t) for t in chosen_tys) + + info_opts = InfoOpts(smir_file=smir_json, types=types_arg) + _kmir_info(info_opts) + out = capsys.readouterr().out.rstrip() + assert_or_update_show_output( + out, PROVE_RS_DIR / f'show/{smir_json.stem}.cli-info.expected', update=update_expected_output + ) + + +def test_cli_link_counts_snapshot(tmp_path: Path, update_expected_output: bool) -> None: + smir1 = PROVE_RS_DIR / 'arith.smir.json' + smir2 = (Path(__file__).parent / 'data' / 'exec-smir' / 'arithmetic' / 'unary.smir.json').resolve(strict=True) + output_file = tmp_path / 'linked.smir.json' + + link_opts = LinkOpts(smir_files=[str(smir1), str(smir2)], output_file=str(output_file)) + _kmir_link(link_opts) + + linked = json.loads(output_file.read_text()) + counts_text = '\n'.join( + [ + f"name: {linked['name']}", + f"types: {len(linked['types'])}", + f"functions: {len(linked['functions'])}", + f"items: {len(linked['items'])}", + f"spans: {len(linked['spans'])}", + ] + ) + + assert_or_update_show_output( + counts_text, + PROVE_RS_DIR / f'show/link.{smir1.stem}+{smir2.stem}.counts.expected', + update=update_expected_output, + ) + + +def test_cli_prune_snapshot( + kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str], update_expected_output: bool +) -> None: + rs_file = PROVE_RS_DIR / 'assert-true.rs' + start_symbol = 'main' + apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False) + + prune_opts = PruneOpts(proof_dir=tmp_path, id=apr_proof.id, node_id=apr_proof.target) + _kmir_prune(prune_opts) + out = capsys.readouterr().out.rstrip() + assert_or_update_show_output( + out, PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-prune.expected', update=update_expected_output + )