diff --git a/README.md b/README.md index bba94ad23..e5253f484 100644 --- a/README.md +++ b/README.md @@ -122,6 +122,9 @@ 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" +# Show additional deltas after the main output, and also print rules for those edges +uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2" --node-deltas-pro "3:4" + # Display full node information (default is compact) uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer @@ -143,9 +146,9 @@ uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose ``` -**`kmir show-rules`** - Show rules applied between nodes +**Rules within `kmir show`** - Show rules applied between nodes ```bash -uv --project kmir run kmir show-rules proof_id source_node target_node --proof-dir ./proof_dir +uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --rules "SOURCE:TARGET[,SOURCE:TARGET...]" ``` ### Recommended Workflow @@ -178,7 +181,7 @@ uv --project kmir run kmir show-rules proof_id source_node target_node --proof-d 4. **Analyze Rules**: ```bash - uv --project kmir run kmir show-rules proof_id 1 3 --proof-dir ./proof_dir + uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --rules "1:3" ``` ### Advanced Show Usage Examples @@ -219,6 +222,8 @@ Most commands support: **`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") +- `--node-deltas-pro DELTAS`: Additional node deltas (same format as `--node-deltas`). Equivalent to "print the corresponding deltas again, and automatically print the rules for these edges". +- `--rules EDGES`: Comma separated list of edges in format "source:target". Prints rules for each edge in Markdown link format `[label](file:///abs/path#LstartLine)` when available - `--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) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 1b742b356..6cbf23a92 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -27,11 +27,11 @@ PruneOpts, RunOpts, ShowOpts, - ShowRulesOpts, ViewOpts, ) from .parse.parser import parse_json from .smir import SMIRInfo, Ty +from .utils import render_rules if TYPE_CHECKING: from argparse import Namespace @@ -154,32 +154,23 @@ def _kmir_show(opts: ShowOpts) -> None: node_printer = KMIRAPRNodePrinter(cterm_show, proof, opts) shower = APRProofShow(kmir.definition, node_printer=node_printer) shower.kcfg_show.pretty_printer = printer + effective_node_deltas = tuple(sorted({*(opts.node_deltas or ()), *(opts.node_deltas_pro or ())})) + effective_rule_edges = tuple(sorted({*(opts.rules or ()), *(opts.node_deltas_pro or ())})) + _LOGGER.info( - f'Showing {proof.id} with\n nodes: {opts.nodes},\n node_deltas: {opts.node_deltas},\n omit_cells: {tuple(all_omit_cells)}' + f'Showing {proof.id} with\n nodes: {opts.nodes},\n node_deltas: {effective_node_deltas},\n omit_cells: {tuple(all_omit_cells)}' ) lines = shower.show( proof, nodes=opts.nodes or (), - node_deltas=opts.node_deltas or (), + node_deltas=effective_node_deltas, omit_cells=tuple(all_omit_cells), ) - print('\n'.join(lines)) - + if effective_rule_edges: + lines.append('# Rules: ') + lines.extend(render_rules(proof, effective_rule_edges)) -def _kmir_show_rules(opts: ShowRulesOpts) -> None: - """Show rules applied on the edge from source to target node.""" - proof = APRProof.read_proof_data(opts.proof_dir, opts.id) - edge = proof.kcfg.edge(opts.source, opts.target) - if edge is None: - print(f'Error: No edge found from node {opts.source} to node {opts.target}') - return - rules = edge.rules - print(f'Rules applied on edge {opts.source} -> {opts.target}:') - print(f'Total rules: {len(rules)}') - print('-' * 80) - for rule in rules: - print(rule) - print('-' * 80) + print('\n'.join(lines)) def _kmir_prune(opts: PruneOpts) -> None: @@ -221,8 +212,6 @@ def kmir(args: Sequence[str]) -> None: _kmir_view(opts) case ShowOpts(): _kmir_show(opts) - case ShowRulesOpts(): - _kmir_show_rules(opts) case PruneOpts(): _kmir_prune(opts) case ProveRSOpts(): @@ -318,6 +307,9 @@ def _arg_parser() -> ArgumentParser: show_parser.add_argument( '--node-deltas', metavar='DELTAS', help='Comma separated list of node deltas in format "source:target"' ) + show_parser.add_argument( + '--node-deltas-pro', metavar='DELTAS', help='Extra node deltas (printed after main output)' + ) show_parser.add_argument( '--omit-cells', metavar='CELLS', help='Comma separated list of cell names to omit from output' ) @@ -336,11 +328,7 @@ def _arg_parser() -> ArgumentParser: 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] - ) - show_rules_parser.add_argument('source', type=int, metavar='SOURCE', help='Source node ID') - show_rules_parser.add_argument('target', type=int, metavar='TARGET', help='Target node ID') + show_parser.add_argument('--rules', metavar='EDGES', help='Comma separated list of edges in format "source:target"') command_parser.add_parser( 'view', help='View proof information', parents=[kcli_args.logging_args, proof_args, display_args] @@ -411,17 +399,12 @@ def _parse_args(ns: Namespace) -> KMirOpts: omit_current_body=ns.omit_current_body, nodes=ns.nodes, node_deltas=ns.node_deltas, + node_deltas_pro=ns.node_deltas_pro, + rules=ns.rules, omit_cells=ns.omit_cells, omit_static_info=ns.omit_static_info, use_default_printer=ns.use_default_printer, ) - case 'show-rules': - return ShowRulesOpts( - proof_dir=Path(ns.proof_dir), - id=ns.id, - source=ns.source, - target=ns.target, - ) case 'view': proof_dir = Path(ns.proof_dir) return ViewOpts( diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index b2acc6459..f9e65808f 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -153,6 +153,8 @@ def __init__( class ShowOpts(DisplayOpts): nodes: tuple[int, ...] | None node_deltas: tuple[tuple[int, int], ...] | None + node_deltas_pro: tuple[tuple[int, int], ...] | None + rules: tuple[tuple[int, int], ...] | None omit_cells: tuple[str, ...] | None omit_static_info: bool use_default_printer: bool @@ -166,6 +168,8 @@ def __init__( omit_current_body: bool = True, nodes: str | None = None, node_deltas: str | None = None, + node_deltas_pro: str | None = None, + rules: str | None = None, omit_cells: str | None = None, omit_static_info: bool = True, use_default_printer: bool = False, @@ -174,15 +178,20 @@ def __init__( 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(','): + + def _parse_pairs(text: str | None) -> tuple[tuple[int, int], ...] | None: + if text is None: + return None + pairs: list[tuple[int, int]] = [] + for delta in text.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 + if len(parts) == 2 and parts[0].strip() and parts[1].strip(): + pairs.append((int(parts[0].strip()), int(parts[1].strip()))) + return tuple(pairs) + + self.node_deltas = _parse_pairs(node_deltas) + self.node_deltas_pro = _parse_pairs(node_deltas_pro) + self.rules = _parse_pairs(rules) static_info_cells = ('', '', '', '') @@ -198,24 +207,6 @@ def __init__( class ViewOpts(DisplayOpts): ... -@dataclass -class ShowRulesOpts(ProofOpts): - source: int - target: int - - def __init__( - self, - proof_dir: Path | str, - id: str, - source: int, - target: int, - ) -> None: - self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None - self.id = id - self.source = source - self.target = target - - @dataclass class PruneOpts(ProofOpts): node_id: int diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py new file mode 100644 index 000000000..c5222bd17 --- /dev/null +++ b/kmir/src/kmir/utils.py @@ -0,0 +1,104 @@ +from __future__ import annotations + +import re +from pathlib import Path +from typing import TYPE_CHECKING, Sequence + +if TYPE_CHECKING: + from pyk.proof.reachability import APRProof + + +def _rule_to_markdown_link(rule: object) -> str: + """Render a single rule as a Markdown file link if possible. + + The function tries, in order: + - Parse the first line of str(rule) for pattern: :/abs/path:(startLine, startCol, endLine, endCol) + - Use rule attributes 'source' and 'location' when available + + Fallback to the first line of str(rule) if no path can be determined. + """ + text_first = str(rule).splitlines()[0] + + # 1) Parse textual representation first (most robust across backends) + m_text = re.match(r'^[^:]+:(/[^:]+):\((\d+)\s*,\s*\d+\s*,\s*\d+\s*,\s*\d+\)\s*$', text_first) + if m_text: + file_path = m_text.group(1) + start_line = int(m_text.group(2)) + uri = Path(file_path).resolve().as_uri() + label_text = f'{Path(file_path).name}:{start_line}' + return f'[{label_text}]({uri}#L{start_line})' + + # 2) Try attributes on the rule object (when present) + try: + att = getattr(rule, 'att', None) + source_file: str | None = None + if att is not None: + get = getattr(att, 'get', None) + if callable(get): + source_file = get('source') + loc = get('location') + else: + try: + source_file = att['source'] # type: ignore[index] + except Exception: + source_file = None + try: + loc = att['location'] # type: ignore[index] + except Exception: + loc = None + + if isinstance(loc, str): + # Format 1: startLine:startCol-endLine:endCol + m = re.match(r'^(\d+):(\d+)-(\d+):(\d+)$', loc) + if m: + start_line = int(m.group(1)) + else: + # Format 2: (startLine, startCol, endLine, endCol) + m2 = re.match(r'^\(\s*(\d+)\s*,\s*\d+\s*,\s*\d+\s*,\s*\d+\s*\)$', loc) + if m2: + start_line = int(m2.group(1)) + + if source_file is not None: + uri = Path(source_file).resolve().as_uri() + line_anchor = f'#L{start_line}' if start_line is not None else '' + label_text = ( + f'{Path(source_file).name}:{start_line}' if start_line is not None else Path(source_file).name + ) + return f'[{label_text}]({uri}{line_anchor})' + except Exception: + pass + + # 3) Fallback: raw first line + return text_first + + +def render_rules(proof: APRProof, edges: Sequence[tuple[int, int]]) -> list[str]: + """Render rules for a collection of edges as markdown text lines. + + - proof: APRProof containing the kcfg with edges + - edges: iterable of (src, dst) + """ + # Deduplicate while preserving a stable ordering + seen: set[tuple[int, int]] = set() + ordered_unique_edges: list[tuple[int, int]] = [] + for e in edges: + if e not in seen: + seen.add(e) + ordered_unique_edges.append(e) + + lines: list[str] = [] + for src, dst in ordered_unique_edges: + edge = proof.kcfg.edge(src, dst) + if edge is None: + lines.append(f'Rules applied on edge {src} -> {dst}:') + lines.append('No edge found') + continue + applied = edge.rules + lines.append(f'Rules applied on edge {src} -> {dst}:') + lines.append(f'Total rules: {len(applied)}') + lines.append('-' * 80) + for rule in applied: + lines.append(_rule_to_markdown_link(rule)) + lines.append('-' * 80) + + return lines