From c4c90ca94bffb8764959650cfd63c57ea7e185f4 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 8 Aug 2025 14:37:52 +0800 Subject: [PATCH 01/12] feat: add custom KMIRPrettyPrinter for improved ListItem formatting - Create KMIRPrettyPrinter class inheriting from PrettyPrinter - Add custom ListItem formatting with proper indentation for multiline content - Implement symbol table customization for ListItem in __init__ - Use indent() function for consistent 2-space indentation - Make custom printer the default with --use-default-printer option to switch back - Add proper logging support for debugging ListItem formatting --- kmir/src/kmir/kprint.py | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 kmir/src/kmir/kprint.py diff --git a/kmir/src/kmir/kprint.py b/kmir/src/kmir/kprint.py new file mode 100644 index 000000000..e2826c659 --- /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.kore.syntax import Definition + + +class KMIRPrettyPrinter(PrettyPrinter): + """ + Custom Pretty Printer for improved ListItem display formatting. + Formats ListItem elements with line breaks for better readability. + """ + + def __init__(self, definition: Definition) -> None: + """ + Initialize KMIR Pretty Printer + + Args: + definition: K definition + """ + super().__init__(definition) + self.symbol_table['ListItem'] = lambda *args: 'ListItem (' + (indent(', '.join(args))).strip() + ')\n' From 800d7d7372a5e87afb5c97a8454aba02351f324d Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 8 Aug 2025 14:37:59 +0800 Subject: [PATCH 02/12] feat: add utility functions for kmir operations - Add utility functions for common kmir operations - Improve code organization and reusability --- kmir/src/kmir/utils.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 kmir/src/kmir/utils.py diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py new file mode 100644 index 000000000..112c4e4c6 --- /dev/null +++ b/kmir/src/kmir/utils.py @@ -0,0 +1,16 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +if TYPE_CHECKING: + from pyk.kast import KInner + from pyk.ktool.kprint import KPrint + + +def kast_print(kast: KInner, *, kprint: KPrint) -> str: + # TODO: copied from riscv-semantics, which should be upstreamed to pyk + from pyk.konvert import kast_to_kore + from pyk.kore.tools import kore_print + + kore = kast_to_kore(kprint.definition, kast) + return kore_print(kore, definition_dir=kprint.definition_dir) From 10052a3ec9321fda554495394f17f0a21db07405 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 8 Aug 2025 14:38:28 +0800 Subject: [PATCH 03/12] docs: update README with comprehensive kmir show command documentation - Add detailed usage examples for all new show command options - Document --nodes, --node-deltas, --omit-cells parameters - Add examples for --full-printer, --no-omit-static-info options - Include debugging workflow examples and performance analysis - Add advanced usage patterns and recommended workflows - Update command options section with all new parameters - Provide practical examples for different use cases --- README.md | 68 ++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 67 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 5e66b9fa8..1f07e06d5 100644 --- a/README.md +++ b/README.md @@ -98,9 +98,31 @@ uv --project kmir run kmir link file1.smir.json file2.smir.json ### 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 +150,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 +168,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 +203,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 From 12de141146238a9f650e35aa6c78068f7782690e Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 8 Aug 2025 14:39:05 +0800 Subject: [PATCH 04/12] refactor: remove unused utils.py file - Remove utils.py as it contains unused utility functions - Clean up codebase by removing dead code - No functionality is affected as the file was not imported anywhere --- kmir/src/kmir/utils.py | 16 ---------------- 1 file changed, 16 deletions(-) delete mode 100644 kmir/src/kmir/utils.py diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py deleted file mode 100644 index 112c4e4c6..000000000 --- a/kmir/src/kmir/utils.py +++ /dev/null @@ -1,16 +0,0 @@ -from __future__ import annotations - -from typing import TYPE_CHECKING - -if TYPE_CHECKING: - from pyk.kast import KInner - from pyk.ktool.kprint import KPrint - - -def kast_print(kast: KInner, *, kprint: KPrint) -> str: - # TODO: copied from riscv-semantics, which should be upstreamed to pyk - from pyk.konvert import kast_to_kore - from pyk.kore.tools import kore_print - - kore = kast_to_kore(kprint.definition, kast) - return kore_print(kore, definition_dir=kprint.definition_dir) From 0fb2cf8b9caf2c88b02569732b5c8efda4b314db Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 11 Aug 2025 10:05:50 +0800 Subject: [PATCH 05/12] Fix SMIR type resolution and add info command - Fix KeyError in unref_type when pointee_type doesn't exist in types - Add proper handling for RefType and PtrType that can be integers directly - Add new 'info' command to show type information from SMIR JSON files - Add InfoOpts class for command line options - Improve error handling and logging for missing types --- kmir/src/kmir/__main__.py | 23 ++++++++++++++++++++++- kmir/src/kmir/options.py | 10 ++++++++++ kmir/src/kmir/smir.py | 24 +++++++++++++++++++++++- 3 files changed, 55 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index ad212d576..c2e1bff62 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, RefT, Ty if TYPE_CHECKING: from argparse import Namespace @@ -164,6 +165,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 +189,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 +234,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') @@ -324,6 +343,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( diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index bb34a02ae..9950f5ead 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -180,6 +180,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..1ed2e4df2 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.warning(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 = {} @@ -297,7 +315,11 @@ class FunT(TypeMetadata): type_str: str -def metadata_from_json(typeinfo: dict) -> TypeMetadata: +def metadata_from_json(typeinfo: dict | int) -> TypeMetadata: + # Handle case where typeinfo is directly an integer (reference type) + if isinstance(typeinfo, int): + return RefT(typeinfo) + if 'PrimitiveType' in typeinfo: return _primty_from_json(typeinfo['PrimitiveType']) elif 'EnumType' in typeinfo: From 8fea5527c511bd674c7890113ef199b9b35134a0 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 11 Aug 2025 10:30:54 +0800 Subject: [PATCH 06/12] Enhance README and implement kmir info command - Add `kmir info` command to inspect SMIR JSON metadata, allowing users to query specific type IDs. - Update README with usage examples for the new `info` command, including details on the `--types` option. - Refactor imports in `__main__.py` and `kprint.py` for clarity and correctness. - Clean up whitespace in several files for improved code readability. --- README.md | 13 +++++++++++++ kmir/src/kmir/__main__.py | 8 ++++---- kmir/src/kmir/kprint.py | 4 ++-- kmir/src/kmir/smir.py | 4 ++-- 4 files changed, 21 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index 1f07e06d5..bba94ad23 100644 --- a/README.md +++ b/README.md @@ -96,6 +96,19 @@ 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 with advanced filtering options diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index c2e1bff62..08a7f7f87 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -31,7 +31,7 @@ ViewOpts, ) from .parse.parser import parse_json -from .smir import SMIRInfo, RefT, Ty +from .smir import SMIRInfo, Ty if TYPE_CHECKING: from argparse import Namespace @@ -167,12 +167,12 @@ def _kmir_prune(opts: PruneOpts) -> None: def _kmir_info(opts: InfoOpts) -> None: smir_info = SMIRInfo.from_file(opts.smir_file) - + if opts.types: - print(f"\nTypes requested: {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)}") + print(f'Type {type_id}: {smir_info.unref_type(type_id)}') def _kmir_link(opts: LinkOpts) -> None: diff --git a/kmir/src/kmir/kprint.py b/kmir/src/kmir/kprint.py index e2826c659..21887dd59 100644 --- a/kmir/src/kmir/kprint.py +++ b/kmir/src/kmir/kprint.py @@ -8,7 +8,7 @@ _LOGGER: logging.Logger = logging.getLogger(__name__) if TYPE_CHECKING: - from pyk.kore.syntax import Definition + from pyk.kast.outer import KDefinition class KMIRPrettyPrinter(PrettyPrinter): @@ -17,7 +17,7 @@ class KMIRPrettyPrinter(PrettyPrinter): Formats ListItem elements with line breaks for better readability. """ - def __init__(self, definition: Definition) -> None: + def __init__(self, definition: KDefinition) -> None: """ Initialize KMIR Pretty Printer diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 1ed2e4df2..ef5e85764 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -47,7 +47,7 @@ def unref_type(self, ty: Ty) -> TypeMetadata | None: 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.""" @@ -319,7 +319,7 @@ def metadata_from_json(typeinfo: dict | int) -> TypeMetadata: # Handle case where typeinfo is directly an integer (reference type) if isinstance(typeinfo, int): return RefT(typeinfo) - + if 'PrimitiveType' in typeinfo: return _primty_from_json(typeinfo['PrimitiveType']) elif 'EnumType' in typeinfo: From c9dd742f80f63bcbffb1bbcafa3ee9aa6de6c803 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 11 Aug 2025 10:34:09 +0800 Subject: [PATCH 07/12] make format & make check --- kmir/src/kmir/smir.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index ef5e85764..7008337ff 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -38,12 +38,12 @@ def types(self) -> dict[Ty, TypeMetadata]: 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") + _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.warning(f"Pointee type {Ty(type_info.pointee_type)} not found in types for reference type {ty}") + _LOGGER.warning(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 From 7de6d6fb4a4fc027ca4b34a800d47ad62c4b54a8 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 11 Aug 2025 10:34:54 +0800 Subject: [PATCH 08/12] fix --- kmir/src/kmir/smir.py | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 7008337ff..543801c4c 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -315,11 +315,7 @@ class FunT(TypeMetadata): type_str: str -def metadata_from_json(typeinfo: dict | int) -> TypeMetadata: - # Handle case where typeinfo is directly an integer (reference type) - if isinstance(typeinfo, int): - return RefT(typeinfo) - +def metadata_from_json(typeinfo: dict) -> TypeMetadata: if 'PrimitiveType' in typeinfo: return _primty_from_json(typeinfo['PrimitiveType']) elif 'EnumType' in typeinfo: From 69087bf9f668499bebe9996499e2c6e11d0e5ed0 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 8 Aug 2025 14:37:46 +0800 Subject: [PATCH 09/12] feat: enhance kmir show command with advanced filtering and formatting options - Add nodes, node_deltas, and omit_cells parameters to ShowOpts - Implement default static info cells omission (functions, start-symbol, types, adt-to-ty) - Add --no-omit-static-info option to display static information - Add --use-default-printer option to switch between custom and standard printers - Change default behavior: --full-printer now defaults to False - Consolidate omit_labels and omit_cells into unified omit_cells parameter - Update _kmir_show function to handle new parameters correctly --- kmir/src/kmir/__main__.py | 68 +++++++++++++++++++++++++++++++++------ kmir/src/kmir/options.py | 45 ++++++++++++++++++++++++-- 2 files changed, 102 insertions(+), 11 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 08a7f7f87..1b742b356 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -131,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)) @@ -266,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', @@ -287,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] @@ -364,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/options.py b/kmir/src/kmir/options.py index 9950f5ead..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 From 65028de171d10e423197e00d1f880fab689e88a6 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 11 Aug 2025 14:20:05 +0800 Subject: [PATCH 10/12] warning 2 info --- kmir/src/kmir/smir.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 543801c4c..f4ca22fcc 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -43,7 +43,7 @@ def unref_type(self, ty: Ty) -> TypeMetadata | None: type_info = self.types[ty] while isinstance(type_info, RefT): if Ty(type_info.pointee_type) not in self.types: - _LOGGER.warning(f'Pointee type {Ty(type_info.pointee_type)} not found in types for reference type {ty}') + _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 From a841eb4b776770868307bfa74fbc117e36edee8d Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 11 Aug 2025 15:28:52 +0800 Subject: [PATCH 11/12] chore: update stable-mir-json subproject to dirty state --- .../show/arith.smir.cli-info.expected | 5 + ...sert-true.main.cli-custom-printer.expected | 14 +++ ...ert-true.main.cli-default-printer.expected | 14 +++ .../show/assert-true.main.cli-prune.expected | 1 + ...link.arith.smir+unary.smir.counts.expected | 5 + kmir/src/tests/integration/test_cli.py | 118 ++++++++++++++++++ 6 files changed, 157 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/arith.smir.cli-info.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-prune.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/link.arith.smir+unary.smir.counts.expected create mode 100644 kmir/src/tests/integration/test_cli.py 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..74d64e954 --- /dev/null +++ b/kmir/src/tests/integration/test_cli.py @@ -0,0 +1,118 @@ +from __future__ import annotations + +import json +from pathlib import Path + +import pytest + +from kmir.__main__ import _kmir_info, _kmir_link, _kmir_prune, _kmir_show +from kmir.kmir import KMIR +from kmir.options import InfoOpts, LinkOpts, ProveRSOpts, PruneOpts, ShowOpts +from kmir.smir import SMIRInfo +from kmir.testing.fixtures import assert_or_update_show_output + + +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): + 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(list(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 + ) + + From 5061128758979b49436e58d3ef9b3ee43c90e237 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 11 Aug 2025 15:46:43 +0800 Subject: [PATCH 12/12] make format & check --- kmir/src/tests/integration/test_cli.py | 27 ++++++++++++++++---------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/kmir/src/tests/integration/test_cli.py b/kmir/src/tests/integration/test_cli.py index 74d64e954..36f77c001 100644 --- a/kmir/src/tests/integration/test_cli.py +++ b/kmir/src/tests/integration/test_cli.py @@ -2,20 +2,25 @@ import json from pathlib import Path - -import pytest +from typing import TYPE_CHECKING from kmir.__main__ import _kmir_info, _kmir_link, _kmir_prune, _kmir_show -from kmir.kmir import KMIR 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): +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() @@ -41,7 +46,9 @@ def test_cli_show_printers_snapshot( _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 + out_custom, + PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-custom-printer.expected', + update=update_expected_output, ) # Standard PrettyPrinter @@ -56,7 +63,9 @@ def test_cli_show_printers_snapshot( _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 + out_default, + PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-default-printer.expected', + update=update_expected_output, ) @@ -64,7 +73,7 @@ def test_cli_info_snapshot(capsys: pytest.CaptureFixture[str], update_expected_o smir_json = PROVE_RS_DIR / 'arith.smir.json' smir_info = SMIRInfo.from_file(smir_json) # choose first few type ids deterministically - chosen_tys = sorted(list(smir_info.types.keys()))[:3] + 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) @@ -96,7 +105,7 @@ def test_cli_link_counts_snapshot(tmp_path: Path, update_expected_output: bool) assert_or_update_show_output( counts_text, - PROVE_RS_DIR / f"show/link.{smir1.stem}+{smir2.stem}.counts.expected", + PROVE_RS_DIR / f'show/link.{smir1.stem}+{smir2.stem}.counts.expected', update=update_expected_output, ) @@ -114,5 +123,3 @@ def test_cli_prune_snapshot( assert_or_update_show_output( out, PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-prune.expected', update=update_expected_output ) - -