Update kmir run to behave more like cargo run

README.md

@@ -36,7 +36,7 @@ Use `--help` with each command for more details.
 
 `parse` to parse a Stable MIR JSON file (`*.smir.json`) file to a K AST
 
-`kmir run` to load an SMIR JSON generated by the `stable-mir-json` tool.
+`kmir run` to run a binary target in your cargo project (or a specific smir json provided with --file). The SMIR JSON will need to have been already built with `stable-mir-json`, or you will need the `RUSTC` environment variable set to your installation of `stable-mir-json`.
 
 `kmir gen-spec` to take a SMIR JSON and create a K specification module that ensures termination of the program.
 
@@ -48,4 +48,4 @@ Use `--help` with each command for more details.
 
 KMIR / mir-semantics is supported by funding from the following sources:
 - [Polkadot Open Gov](https://polkadot.subsquare.io/referenda/749)
-- Solana
+- Solana

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.117"
+version = "0.3.118"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.117'
+VERSION: Final = '0.3.118'

kmir/src/kmir/__main__.py

@@ -16,6 +16,7 @@
 from kmir.build import HASKELL_DEF_DIR, LLVM_LIB_DIR, haskell_semantics, llvm_semantics
 from kmir.kmir import KMIR, KMIRAPRNodePrinter
 from kmir.parse.parser import parse_json
+from kmir.rust import CargoProject
 
 if TYPE_CHECKING:
     from collections.abc import Sequence
@@ -27,7 +28,8 @@ class KMirOpts: ...
 
 @dataclass
 class RunOpts(KMirOpts):
-    input_file: Path
+    bin: str | None
+    file: str | None
     depth: int
     start_symbol: str
     haskell_backend: bool
@@ -80,7 +82,15 @@ class ProveViewOpts(KMirOpts):
 def _kmir_run(opts: RunOpts) -> None:
     tools = haskell_semantics() if opts.haskell_backend else llvm_semantics()
 
-    parse_result = parse_json(tools.definition, opts.input_file, 'Pgm')
+    smir_file: Path
+    if opts.file:
+        smir_file = Path(opts.file).resolve()
+    else:
+        cargo = CargoProject(Path.cwd())
+        target = opts.bin if opts.bin else cargo.default_target
+        smir_file = cargo.smir_for(target)
+
+    parse_result = parse_json(tools.definition, smir_file, 'Pgm')
     if parse_result is None:
         print('Parse error!', file=sys.stderr)
         sys.exit(1)
@@ -170,7 +180,9 @@ def _arg_parser() -> ArgumentParser:
     command_parser = parser.add_subparsers(dest='command', required=True)
 
     run_parser = command_parser.add_parser('run', help='run stable MIR programs')
-    run_parser.add_argument('input_file', metavar='FILE', help='MIR program to run')
+    run_target_selection = run_parser.add_mutually_exclusive_group()
+    run_target_selection.add_argument('--bin', metavar='TARGET', help='Target to run')
+    run_target_selection.add_argument('--file', metavar='SMIR', help='SMIR json file to execute')
     run_parser.add_argument('--depth', type=int, metavar='DEPTH', help='Depth to execute')
     run_parser.add_argument(
         '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from'
@@ -213,7 +225,8 @@ def _parse_args(args: Sequence[str]) -> KMirOpts:
     match ns.command:
         case 'run':
             return RunOpts(
-                input_file=Path(ns.input_file).resolve(),
+                bin=ns.bin,
+                file=ns.file,
                 depth=ns.depth,
                 start_symbol=ns.start_symbol,
                 haskell_backend=ns.haskell_backend,

kmir/src/kmir/rust/__init__.py

@@ -0,0 +1 @@
+from .cargo import CargoProject

kmir/src/kmir/rust/cargo.py

@@ -0,0 +1,82 @@
+from __future__ import annotations
+
+import json
+import subprocess
+from functools import cached_property
+from pathlib import Path
+
+
+class CargoProject:
+    working_directory: Path
+
+    def __init__(self, working_directory: Path) -> None:
+        self.working_directory = working_directory
+
+    @cached_property
+    def metadata(self) -> dict:
+        """Metadata about the cargo project"""
+
+        command = ['cargo', 'metadata', '--format-version', '1']
+        command_result = subprocess.run(command, capture_output=True, text=True, cwd=self.working_directory)
+        metadata = json.loads(command_result.stdout)
+        return metadata
+
+    @cached_property
+    def manifest(self) -> dict:
+        """Information about the Cargo.toml file"""
+
+        command = ['cargo', 'read-manifest']
+        command_result = subprocess.run(command, capture_output=True, text=True, cwd=self.working_directory)
+        manifest = json.loads(command_result.stdout)
+        return manifest
+
+    @property
+    def build_messages(self) -> list[dict]:
+        """Output of messages from `cargo build`"""
+
+        command = ['cargo', 'build', '--message-format=json']
+        command_result = subprocess.run(command, capture_output=True, text=True, cwd=self.working_directory)
+        split_command_result = command_result.stdout.splitlines()
+        messages = [json.loads(message) for message in split_command_result]
+        return messages
+
+    def smir_for(self, target: str) -> Path:
+        """Gets the latest smir json in the target directory for the given target. Raises a RuntimeError if none exist."""
+
+        is_artifact = lambda message: message.get('reason') == 'compiler-artifact'
+        is_my_target = lambda artifact: artifact.get('target', {}).get('name') == target
+        artifact = next(message for message in self.build_messages if is_artifact(message) and is_my_target(message))
+        executable_name = Path(artifact['executable'])
+        deps_dir = executable_name.parent / 'deps'
+
+        # Get the smir file(s) and sort them by modified time
+        smir_files = deps_dir.glob(f'{target}*.smir.json')
+        sorted_smir_files = sorted(smir_files, key=lambda f: f.stat().st_mtime, reverse=True)
+
+        if len(sorted_smir_files) == 0:
+            raise RuntimeError(
+                f'Unable to find smir json for target {target!r}. Have you built it using stable-mir-json?'
+            )
+
+        # Return the most recently modified smir file
+        return sorted_smir_files[0]
+
+    @cached_property
+    def default_target(self) -> str:
+        """Returns the name of the default binary target. If it can't find a default, raises a RuntimeError"""
+
+        default_run = self.manifest.get('default_run')
+        if isinstance(default_run, str):
+            return default_run
+
+        is_bin = lambda target: any(kind == 'bin' for kind in target.get('kind'))
+        targets = self.manifest.get('targets')
+        assert isinstance(targets, list)
+        bin_targets = [target.get('name') for target in targets if is_bin(target)]
+
+        if len(bin_targets) != 1:
+            raise RuntimeError(
+                f"Can't determine which binary to run. Use --bin, or the 'default-run' manifest key. Found {bin_targets}"
+            )
+
+        return bin_targets[0]

package/version

@@ -1 +1 @@
-0.3.117
+0.3.118