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/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/kmir/__main__.py b/kmir/src/kmir/__main__.py index 11e9b493f..290b50ed8 100644 --- a/kmir/src/kmir/__main__.py +++ b/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': diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index ae5cd6844..ca029ca09 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 - 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 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 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`