Support for .rs files in kmir run

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
 

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 |

kmir/src/kmir/__main__.py

@@ -59,17 +59,17 @@ def _flush_lines(lines: Iterable[str]) -> None:
 
 
 def _kmir_run(opts: RunOpts) -> None:
-    if opts.file:
-        smir_info = SMIRInfo.from_file(Path(opts.file))
-    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
+    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):
+    def run(target_dir: Path) -> None:
         kmir = KMIR.from_kompiled_kore(
             smir_info,
             target_dir=target_dir,
@@ -330,12 +330,14 @@ 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(
-        '--bin', metavar='TARGET', help='Cargo binary target name to run (mutually exclusive with --file)'
+    run_parser.add_argument(
+        'rs_file', metavar='FILE', help='Rust file, SMIR JSON (with --smir), or cargo target (with --bin)'
     )
-    run_target_selection.add_argument(
-        '--file', metavar='SMIR', help='SMIR JSON file to execute (mutually exclusive 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.'
     )
     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,11 +659,13 @@ def _parse_args(ns: Namespace) -> KMirOpts:
     match ns.command:
         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,
-                file=ns.file,
                 target_dir=ns.target_dir,
-                depth=ns.depth,
-                start_symbol=ns.start_symbol,
                 symbolic=ns.symbolic,
             )
         case 'info':

kmir/src/kmir/options.py

@@ -21,8 +21,10 @@ class KMirOpts: ...
 class RunOpts(KMirOpts):
     start_symbol: str
     depth: int
-    bin: str | None
-    file: str | None
+    rs_file: Path
+    smir: bool
+    save_smir: bool
+    bin: bool
     target_dir: Path | None
     symbolic: bool
     haskell_target: str | None
@@ -31,21 +33,25 @@ class RunOpts(KMirOpts):
 
     def __init__(
         self,
+        rs_file: str | Path,
         start_symbol: str,
         depth: int,
         *,
-        bin: str | None = None,
-        file: str | None = None,
+        smir: bool = False,
+        save_smir: bool = False,
+        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.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

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}')

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 > <path>/<to>/<NAME>.run.state
+  /mir-semantics $ uv --project kmir/ run kmir run path/to/NAME.smir.json --smir > <path>/<to>/<NAME>.run.state
   ```
 * check that the output is as expected
 * add test to `EXEC_DATA` array in `kmir/src/tests/integration/test_integration.py`