From c5327570272ae21884eef04e7d13b6a31fda252a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 2 May 2025 03:21:52 +0000 Subject: [PATCH 1/9] kmir/{smir,kmir}: add actual file lookup for span of execution --- kmir/src/kmir/kmir.py | 9 +++++++-- kmir/src/kmir/smir.py | 4 ++++ 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index c5727fa33..484b8ad7b 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -202,7 +202,7 @@ def __init__( APRProofNodePrinter.__init__(self, proof, cterm_show, full_printer=full_printer) self.smir_info = smir_info - 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 +218,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'span: {curr_span}' + return None def _function_name(self, node: KCFG.Node) -> str | None: curr_func_ty_kast = node.cterm.cell('CURRENTFUNC_CELL') diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 29837c78b..56f809b18 100644 --- a/kmir/src/kmir/smir.py +++ b/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'] From e564c8e804ee7c56f78c0c65be3f8b12138cb57e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 4 May 2025 18:05:52 +0000 Subject: [PATCH 2/9] kmir/{kmir,__main__}: refactor to pass entire DisplayOptions to show functionality --- kmir/src/kmir/__main__.py | 10 ++-------- kmir/src/kmir/kmir.py | 12 +++++------- kmir/src/tests/integration/test_integration.py | 12 +++++------- 3 files changed, 12 insertions(+), 22 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index ccf260664..12ec923d4 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -114,12 +114,9 @@ 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) + node_printer = KMIRAPRNodePrinter(cterm_show, proof, opts) viewer = APRProofViewer(proof, kmir, node_printer=node_printer) viewer.run() @@ -127,12 +124,9 @@ def _kmir_view(opts: ViewOpts) -> None: 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) + node_printer = KMIRAPRNodePrinter(cterm_show, proof, opts) shower = APRProofShow(kmir.definition, node_printer=node_printer) lines = shower.show(proof) print('\n'.join(lines)) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 484b8ad7b..8bb999d82 100644 --- a/kmir/src/kmir/kmir.py +++ b/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__) @@ -195,12 +195,10 @@ 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 = SMIRInfo.from_file(opts.smir_info) if opts.smir_info else None def _span(self, node: KCFG.Node) -> str | None: curr_span: int | None = None diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 68875be49..1df4ec637 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/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,8 @@ 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) + 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 +510,8 @@ 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=False, smir_info=None) + 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, From a4f22a42377dc60a7c67d9b98e1eeb248e1f3c9d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 13 May 2025 18:54:41 +0000 Subject: [PATCH 3/9] kmir/kmir.py: correct span printing --- kmir/src/kmir/kmir.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 8bb999d82..e44b201b0 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -220,7 +220,7 @@ def _span(self, node: KCFG.Node) -> str | None: 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'span: {curr_span}' + return f'{curr_span}' return None def _function_name(self, node: KCFG.Node) -> str | None: From 953a9c4b16666b682028466b0b0d48a0b041c915 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 14 May 2025 20:55:24 +0000 Subject: [PATCH 4/9] kmir/{kmir,__main__}: use upstreamed option to omit cells --- kmir/src/kmir/__main__.py | 29 ++++++++++++++++--- kmir/src/kmir/options.py | 3 ++ .../src/tests/integration/test_integration.py | 8 +++-- 3 files changed, 34 insertions(+), 6 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 12ec923d4..37f70e12b 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -115,7 +115,8 @@ def _kmir_view(opts: ViewOpts) -> None: kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR) proof = APRProof.read_proof_data(opts.proof_dir, opts.id) printer = PrettyPrinter(kmir.definition) - cterm_show = CTermShow(printer.print) + omit_labels = ('',) if opts.omit_current_body else () + cterm_show = CTermShow(printer.print, omit_labels=omit_labels) node_printer = KMIRAPRNodePrinter(cterm_show, proof, opts) viewer = APRProofViewer(proof, kmir, node_printer=node_printer) viewer.run() @@ -125,7 +126,8 @@ def _kmir_show(opts: ShowOpts) -> None: kmir = KMIR(HASKELL_DEF_DIR, LLVM_LIB_DIR) proof = APRProof.read_proof_data(opts.proof_dir, opts.id) printer = PrettyPrinter(kmir.definition) - cterm_show = CTermShow(printer.print) + omit_labels = ('',) 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) @@ -226,6 +228,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 cell completely.', + ) command_parser.add_parser( 'show', help='Show a saved proof', parents=[kcli_args.logging_args, proof_args, display_args] @@ -285,13 +294,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(), diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index 343d740b6..c0b7db9d8 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -132,6 +132,7 @@ def __init__( class DisplayOpts(ProofOpts): full_printer: bool smir_info: Path | None + omit_current_body: bool def __init__( self, @@ -139,11 +140,13 @@ def __init__( 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 diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 1df4ec637..b3c48457d 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -479,7 +479,9 @@ def test_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> No else: assert apr_proof.failed - display_opts = ShowOpts(rs_file.parent, apr_proof.id, full_printer=False, smir_info=None) + 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( @@ -510,7 +512,9 @@ 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) - display_opts = ShowOpts(pinocchio_token_program.parent, apr_proof.id, full_printer=False, smir_info=None) + display_opts = ShowOpts( + pinocchio_token_program.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( From 904e5f14c1595bd2a285dd921b33d266cd915fa6 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 21 May 2025 01:19:05 +0000 Subject: [PATCH 5/9] Set Version: 0.3.171 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index e51950c3b..665b3bcb6 100644 --- a/kmir/pyproject.toml +++ b/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 = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 92cd7d43f..6546cce99 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.170' +VERSION: Final = '0.3.171' diff --git a/kmir/uv.lock b/kmir/uv.lock index 9968011ce..fab94096d 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -491,7 +491,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.170" +version = "0.3.171" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index a71140a88..dd7b514b6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.170 +0.3.171 From 60a68aed4a4ac45a7ea12275eb9c9c6da79b0f10 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 21 May 2025 02:07:11 +0000 Subject: [PATCH 6/9] kmir/{kmir,__main__}: enable saving and using SMIRInfo for prove-rs --- kmir/src/kmir/__main__.py | 2 ++ kmir/src/kmir/kmir.py | 12 +++++++++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 37f70e12b..62a5515c2 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -114,6 +114,8 @@ 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) + if not opts.smir_info and proof.proof_dir is not None and (proof.proof_dir / proof.id / 'smir.json').is_file(): + opts.smir_info = proof.proof_dir / proof.id / 'smir.json' printer = PrettyPrinter(kmir.definition) omit_labels = ('',) if opts.omit_current_body else () cterm_show = CTermShow(printer.print, omit_labels=omit_labels) diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index e44b201b0..78165b1b6 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -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: @@ -198,7 +200,15 @@ class KMIRAPRNodePrinter(KMIRNodePrinter, APRProofNodePrinter): 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 = SMIRInfo.from_file(opts.smir_info) if opts.smir_info else None + 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) -> str | None: curr_span: int | None = None From 41a0941855eef165cb1a3117b314ee64f26290c8 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 21 May 2025 02:15:06 +0000 Subject: [PATCH 7/9] kmir/__main__: make sure that full node printer has options passed --- kmir/src/kmir/__main__.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 62a5515c2..d6193a892 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -119,8 +119,9 @@ def _kmir_view(opts: ViewOpts) -> None: printer = PrettyPrinter(kmir.definition) omit_labels = ('',) 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) + viewer = APRProofViewer(proof, kmir, node_printer=node_printer, cterm_show=cterm_show) viewer.run() From 598ee74c661c7ccd39a307e5241c9fb905728180 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 21 May 2025 02:40:31 +0000 Subject: [PATCH 8/9] kmir/tests/test_integration: correct how we are printing output --- kmir/src/tests/integration/test_integration.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index b3c48457d..7e615736a 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -513,7 +513,7 @@ def test_prove_pinocchio(kmir: KMIR, update_expected_output: bool) -> None: prove_rs_opts.start_symbol = start_symbol apr_proof = kmir.prove_rs(prove_rs_opts) display_opts = ShowOpts( - pinocchio_token_program.parent, apr_proof.id, full_printer=False, smir_info=None, omit_current_body=False + 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)) From d345d962da05e5ee2e99a20edafcb045fe396590 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 21 May 2025 14:18:26 +1000 Subject: [PATCH 9/9] Remove search for `smir.json` from `_kmir_view` --- kmir/src/kmir/__main__.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index d6193a892..4defb2842 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -114,8 +114,6 @@ 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) - if not opts.smir_info and proof.proof_dir is not None and (proof.proof_dir / proof.id / 'smir.json').is_file(): - opts.smir_info = proof.proof_dir / proof.id / 'smir.json' printer = PrettyPrinter(kmir.definition) omit_labels = ('',) if opts.omit_current_body else () cterm_show = CTermShow(printer.print, omit_labels=omit_labels)