From 34fe7e88b72e8cd6855f0f0e71f1abbe045213b9 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Tue, 5 May 2026 15:23:31 -0500 Subject: [PATCH 1/6] Added option to run with .rs in kmir run The interface is similar to prove. --save-smir also added. --- kmir/src/kmir/__main__.py | 31 +++++++++++++++++++++---------- kmir/src/kmir/options.py | 12 +++++++++--- 2 files changed, 30 insertions(+), 13 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 11e9b493f..6523e7e85 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -59,17 +59,22 @@ def _flush_lines(lines: Iterable[str]) -> None: def _kmir_run(opts: RunOpts) -> None: - if opts.file: - smir_info = SMIRInfo.from_file(Path(opts.file)) + if opts.rs_file: + if opts.smir: + smir_info = SMIRInfo.from_file(opts.rs_file) + else: + from .cargo import cargo_get_smir_json + + smir_info = SMIRInfo(cargo_get_smir_json(opts.rs_file, save_smir=opts.save_smir)) + elif opts.bin: + cargo = CargoProject(Path.cwd()) + _LOGGER.warning(f'Requested to run {opts.bin} but multi-exec projects currently not supported') + smir_info = cargo.smir_for_project(clean=False) else: cargo = CargoProject(Path.cwd()) - # multi-exec projects currently not supported - if opts.bin: - _LOGGER.warning(f'Requested to run {opts.bin} but multi-exec projects currently not supported') - # target = opts.bin if opts.bin else cargo.default_target smir_info = cargo.smir_for_project(clean=False) - def run(target_dir: Path): + def run(target_dir: Path) -> None: kmir = KMIR.from_kompiled_kore( smir_info, target_dir=target_dir, @@ -332,10 +337,14 @@ def _arg_parser() -> ArgumentParser: run_parser = command_parser.add_parser('run', help='run stable MIR programs', parents=[kcli_args.logging_args]) run_target_selection = run_parser.add_mutually_exclusive_group() run_target_selection.add_argument( - '--bin', metavar='TARGET', help='Cargo binary target name to run (mutually exclusive with --file)' + 'rs_file', nargs='?', metavar='FILE', help='Rust or SMIR JSON file to run (use --smir for SMIR JSON)' ) run_target_selection.add_argument( - '--file', metavar='SMIR', help='SMIR JSON file to execute (mutually exclusive with --bin)' + '--bin', metavar='TARGET', help='Cargo binary target name to run (mutually exclusive with FILE)' + ) + run_parser.add_argument('--smir', action='store_true', help='Treat the input file as a SMIR JSON.') + run_parser.add_argument( + '--save-smir', action='store_true', help='Do not delete the intermediate generated SMIR JSON file.' ) run_parser.add_argument('--target-dir', type=Path, metavar='TARGET_DIR', help='SMIR kompilation target directory') run_parser.add_argument('--depth', type=int, metavar='DEPTH', help='Maximum number of execution steps') @@ -657,8 +666,10 @@ def _parse_args(ns: Namespace) -> KMirOpts: match ns.command: case 'run': return RunOpts( + rs_file=ns.rs_file, + smir=ns.smir, + save_smir=ns.save_smir, bin=ns.bin, - file=ns.file, target_dir=ns.target_dir, depth=ns.depth, start_symbol=ns.start_symbol, diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index ae5cd6844..4eb0abd95 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -21,8 +21,10 @@ class KMirOpts: ... class RunOpts(KMirOpts): start_symbol: str depth: int + rs_file: Path | None + smir: bool + save_smir: bool bin: str | None - file: str | None target_dir: Path | None symbolic: bool haskell_target: str | None @@ -34,8 +36,10 @@ def __init__( start_symbol: str, depth: int, *, + rs_file: str | Path | None = None, + smir: bool = False, + save_smir: bool = False, bin: str | None = None, - file: str | None = None, target_dir: str | Path | None = None, symbolic: bool = False, haskell_target: str | None = None, @@ -44,8 +48,10 @@ def __init__( ): self.start_symbol = start_symbol self.depth = depth + self.rs_file = Path(rs_file).resolve() if rs_file is not None else None + self.smir = smir + self.save_smir = save_smir self.bin = bin - self.file = file self.target_dir = Path(target_dir).resolve() if target_dir is not None else None self.symbolic = symbolic self.haskell_target = haskell_target From cfb16c86998a3866b8fe6ac39fc1d9ff196a2ed5 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Tue, 5 May 2026 15:29:45 -0500 Subject: [PATCH 2/6] Error message when input is not provided. --- kmir/src/kmir/__main__.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 6523e7e85..c1c7072ce 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -59,6 +59,11 @@ def _flush_lines(lines: Iterable[str]) -> None: def _kmir_run(opts: RunOpts) -> None: + if not opts.rs_file and not opts.bin: + raise SystemExit('kmir run: error: either FILE or --bin is required') + if opts.smir and not opts.rs_file: + raise SystemExit('kmir run: error: --smir requires a FILE argument') + if opts.rs_file: if opts.smir: smir_info = SMIRInfo.from_file(opts.rs_file) @@ -66,12 +71,9 @@ def _kmir_run(opts: RunOpts) -> None: from .cargo import cargo_get_smir_json smir_info = SMIRInfo(cargo_get_smir_json(opts.rs_file, save_smir=opts.save_smir)) - elif opts.bin: - cargo = CargoProject(Path.cwd()) - _LOGGER.warning(f'Requested to run {opts.bin} but multi-exec projects currently not supported') - smir_info = cargo.smir_for_project(clean=False) else: cargo = CargoProject(Path.cwd()) + _LOGGER.warning(f'Requested to run {opts.bin} but multi-exec projects currently not supported') smir_info = cargo.smir_for_project(clean=False) def run(target_dir: Path) -> None: From 0132f79fbc3e67a439d2dd07841a8d17661b418e Mon Sep 17 00:00:00 2001 From: mariaKt Date: Tue, 5 May 2026 16:35:20 -0500 Subject: [PATCH 3/6] Used single positional argument for input, --smir and --bin are flags. --- kmir/src/kmir/__main__.py | 39 ++++++++++++++------------------------- kmir/src/kmir/options.py | 10 +++++----- 2 files changed, 19 insertions(+), 30 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index c1c7072ce..d4855f340 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -59,22 +59,15 @@ def _flush_lines(lines: Iterable[str]) -> None: def _kmir_run(opts: RunOpts) -> None: - if not opts.rs_file and not opts.bin: - raise SystemExit('kmir run: error: either FILE or --bin is required') - if opts.smir and not opts.rs_file: - raise SystemExit('kmir run: error: --smir requires a FILE argument') - - if opts.rs_file: - if opts.smir: - smir_info = SMIRInfo.from_file(opts.rs_file) - else: - from .cargo import cargo_get_smir_json - - smir_info = SMIRInfo(cargo_get_smir_json(opts.rs_file, save_smir=opts.save_smir)) - else: - cargo = CargoProject(Path.cwd()) - _LOGGER.warning(f'Requested to run {opts.bin} but multi-exec projects currently not supported') + if opts.smir: + smir_info = SMIRInfo.from_file(opts.rs_file) + elif opts.bin: + cargo = CargoProject(opts.rs_file) smir_info = cargo.smir_for_project(clean=False) + else: + from .cargo import cargo_get_smir_json + + smir_info = SMIRInfo(cargo_get_smir_json(opts.rs_file, save_smir=opts.save_smir)) def run(target_dir: Path) -> None: kmir = KMIR.from_kompiled_kore( @@ -337,14 +330,10 @@ def _arg_parser() -> ArgumentParser: kcli_args = KCLIArgs() run_parser = command_parser.add_parser('run', help='run stable MIR programs', parents=[kcli_args.logging_args]) - run_target_selection = run_parser.add_mutually_exclusive_group() - run_target_selection.add_argument( - 'rs_file', nargs='?', metavar='FILE', help='Rust or SMIR JSON file to run (use --smir for SMIR JSON)' - ) - run_target_selection.add_argument( - '--bin', metavar='TARGET', help='Cargo binary target name to run (mutually exclusive with FILE)' - ) - run_parser.add_argument('--smir', action='store_true', help='Treat the input file as a SMIR JSON.') + run_parser.add_argument('rs_file', metavar='FILE', help='Rust file, SMIR JSON (with --smir), or cargo target (with --bin)') + run_input_mode = run_parser.add_mutually_exclusive_group() + run_input_mode.add_argument('--smir', action='store_true', help='Treat the input as a SMIR JSON file.') + run_input_mode.add_argument('--bin', action='store_true', help='Treat the input as a cargo binary target name.') run_parser.add_argument( '--save-smir', action='store_true', help='Do not delete the intermediate generated SMIR JSON file.' ) @@ -669,12 +658,12 @@ def _parse_args(ns: Namespace) -> KMirOpts: case 'run': return RunOpts( rs_file=ns.rs_file, + start_symbol=ns.start_symbol, + depth=ns.depth, smir=ns.smir, save_smir=ns.save_smir, bin=ns.bin, target_dir=ns.target_dir, - depth=ns.depth, - start_symbol=ns.start_symbol, symbolic=ns.symbolic, ) case 'info': diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index 4eb0abd95..ca029ca09 100644 --- a/kmir/src/kmir/options.py +++ b/kmir/src/kmir/options.py @@ -21,10 +21,10 @@ class KMirOpts: ... class RunOpts(KMirOpts): start_symbol: str depth: int - rs_file: Path | None + rs_file: Path smir: bool save_smir: bool - bin: str | None + bin: bool target_dir: Path | None symbolic: bool haskell_target: str | None @@ -33,22 +33,22 @@ class RunOpts(KMirOpts): def __init__( self, + rs_file: str | Path, start_symbol: str, depth: int, *, - rs_file: str | Path | None = None, smir: bool = False, save_smir: bool = False, - bin: str | None = None, + bin: bool = False, target_dir: str | Path | None = None, symbolic: bool = False, haskell_target: str | None = None, llvm_lib_target: str | None = None, llvm_target: str | None = None, ): + self.rs_file = Path(rs_file).resolve() self.start_symbol = start_symbol self.depth = depth - self.rs_file = Path(rs_file).resolve() if rs_file is not None else None self.smir = smir self.save_smir = save_smir self.bin = bin From b5a858493bcac3aa191a24d9301a5280f2a8c4d1 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Tue, 5 May 2026 17:04:57 -0500 Subject: [PATCH 4/6] Updated documentation. --- README.md | 2 +- kmir/src/tests/integration/data/exec-smir/README.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 2d8b17566..e235851bf 100644 --- a/README.md +++ b/README.md @@ -69,7 +69,7 @@ Every subcommand supports `--help` for the full option list. | Command | Purpose | | --- | --- | -| `kmir run` | Execute a Rust program from SMIR JSON | +| `kmir run` | Execute a Rust program (from `.rs`, SMIR JSON with `--smir`, or cargo target with `--bin`) | | `kmir prove` | Prove properties of a Rust source file (recommended entry point) | | `kmir show` | Inspect a proof graph — nodes, deltas, rules, statistics | | `kmir view` | Interactive proof viewer | diff --git a/kmir/src/tests/integration/data/exec-smir/README.md b/kmir/src/tests/integration/data/exec-smir/README.md index 2ad2cdc02..f2167485c 100644 --- a/kmir/src/tests/integration/data/exec-smir/README.md +++ b/kmir/src/tests/integration/data/exec-smir/README.md @@ -9,7 +9,7 @@ The tests below this directory are intended to be run with `kmir run`, comparing * Generate stable-mir JSON `NAME.smir.json` for the test program (using `deps/stable-mir-pretty`) * run the program once to generate the expected output state ``` - /mir-semantics $ poetry -C kmir run -- kmir run path/to/NAME.smir.json > //.run.state + /mir-semantics $ uv --project kmir/ run kmir run path/to/NAME.smir.json --smir > //.run.state ``` * check that the output is as expected * add test to `EXEC_DATA` array in `kmir/src/tests/integration/test_integration.py` From 533ecc2720148828115b91689f7ec07f5c2712be Mon Sep 17 00:00:00 2001 From: mariaKt Date: Tue, 5 May 2026 17:42:32 -0500 Subject: [PATCH 5/6] Code quality fixes --- kmir/src/kmir/__main__.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index d4855f340..290b50ed8 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -330,7 +330,9 @@ def _arg_parser() -> ArgumentParser: kcli_args = KCLIArgs() run_parser = command_parser.add_parser('run', help='run stable MIR programs', parents=[kcli_args.logging_args]) - run_parser.add_argument('rs_file', metavar='FILE', help='Rust file, SMIR JSON (with --smir), or cargo target (with --bin)') + run_parser.add_argument( + 'rs_file', metavar='FILE', help='Rust file, SMIR JSON (with --smir), or cargo target (with --bin)' + ) run_input_mode = run_parser.add_mutually_exclusive_group() run_input_mode.add_argument('--smir', action='store_true', help='Treat the input as a SMIR JSON file.') run_input_mode.add_argument('--bin', action='store_true', help='Treat the input as a cargo binary target name.') From 6a9f8f2ab52981753244889bd3cf85cd17cd9581 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Tue, 5 May 2026 20:50:32 -0500 Subject: [PATCH 6/6] Rename ui tests script that uses prove, add script that uses run. --- Makefile | 2 +- .../tests/external/test_stable_mir_ui_exec.py | 85 +++++++++++++++++++ ...ui_pass.py => test_stable_mir_ui_prove.py} | 0 3 files changed, 86 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/external/test_stable_mir_ui_exec.py rename kmir/src/tests/external/{test_stable_mir_ui_pass.py => test_stable_mir_ui_prove.py} (100%) diff --git a/Makefile b/Makefile index 374536ff6..489bfedb8 100644 --- a/Makefile +++ b/Makefile @@ -63,7 +63,7 @@ test-verify-rust-std: stable-mir-json build .PHONY: test-stable-mir-ui test-stable-mir-ui: stable-mir-json build @test -n "$(RUST_DIR_ROOT)" || (echo "RUST_DIR_ROOT is required. Example: RUST_DIR_ROOT=/path/to/rust make test-stable-mir-ui"; exit 2) - $(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/external/test_stable_mir_ui_pass.py --maxfail=1 --verbose $(TEST_ARGS) + $(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/external/test_stable_mir_ui_prove.py --maxfail=1 --verbose $(TEST_ARGS) # Checks and formatting diff --git a/kmir/src/tests/external/test_stable_mir_ui_exec.py b/kmir/src/tests/external/test_stable_mir_ui_exec.py new file mode 100644 index 000000000..55cb61011 --- /dev/null +++ b/kmir/src/tests/external/test_stable_mir_ui_exec.py @@ -0,0 +1,85 @@ +"""Run stable-mir-ui tests using kmir run (LLVM backend). + +For each test in passing.tsv, compiles the .rs file to SMIR JSON, +runs it with the LLVM backend, and checks that execution reaches #EndProgram. +""" + +from __future__ import annotations + +import os +import tempfile +from pathlib import Path + +import pytest + +from kmir.cargo import cargo_get_smir_json +from kmir.kmir import KMIR +from kmir.smir import SMIRInfo + +THIS_DIR = Path(__file__).resolve().parent +REPO_ROOT = THIS_DIR.parents[3] +PASSING_TSV = REPO_ROOT / 'deps' / 'stable-mir-json' / 'tests' / 'ui' / 'passing.tsv' +SKIP_FILE = THIS_DIR / 'data' / 'stable-mir-ui' / 'skip.txt' +PASSING_TESTS: tuple[str, ...] = tuple( + line.split('\t', maxsplit=1)[0] for line in PASSING_TSV.read_text().splitlines() if line.strip() +) +SKIP_ENTRIES: frozenset[str] = ( + frozenset(line for line in SKIP_FILE.read_text().splitlines() if line.strip()) + if SKIP_FILE.is_file() + else frozenset() +) + + +@pytest.fixture(scope='session') +def rust_dir_root() -> Path: + rust_dir_root_raw = os.environ.get('RUST_DIR_ROOT') + if not rust_dir_root_raw: + pytest.fail( + 'RUST_DIR_ROOT is required. Example: RUST_DIR_ROOT=/path/to/rust ./run-ui-tests.sh', + pytrace=False, + ) + + rust_dir_root = Path(rust_dir_root_raw).expanduser().resolve() + if not rust_dir_root.is_dir(): + pytest.fail(f'RUST_DIR_ROOT is not a directory: {rust_dir_root}', pytrace=False) + + return rust_dir_root + + +@pytest.mark.timeout(300) +@pytest.mark.parametrize('test_rel_path', PASSING_TESTS, ids=PASSING_TESTS) +def test_stable_mir_ui_exec(test_rel_path: str, rust_dir_root: Path, update_skip_mode: bool, tmp_path: Path) -> None: + if (test_rel_path in SKIP_ENTRIES) != update_skip_mode: + pytest.skip() + + rs_file = rust_dir_root / test_rel_path + + try: + smir_data = cargo_get_smir_json(rs_file, save_smir=False) + smir_info = SMIRInfo(smir_data) + except Exception: + if update_skip_mode: + pytest.xfail('Compilation error') + raise + + try: + with tempfile.TemporaryDirectory() as target_dir: + kmir = KMIR.from_kompiled_kore(smir_info, target_dir=Path(target_dir), symbolic=False) + result = kmir.run_smir(smir_info) + result_pretty = kmir.kore_to_pretty(result) + except Exception: + if update_skip_mode: + pytest.xfail('Execution error') + raise + + reached_end = '#EndProgram ~> .K' in result_pretty + + if update_skip_mode: + if not reached_end: + pytest.xfail('Did not reach #EndProgram') + return + + if not reached_end: + output_file = tmp_path / 'show.txt' + output_file.write_text(result_pretty) + raise AssertionError(f'Execution did not reach #EndProgram. See: {output_file}') diff --git a/kmir/src/tests/external/test_stable_mir_ui_pass.py b/kmir/src/tests/external/test_stable_mir_ui_prove.py similarity index 100% rename from kmir/src/tests/external/test_stable_mir_ui_pass.py rename to kmir/src/tests/external/test_stable_mir_ui_prove.py