From a9543d2b11514e8904dd43d520d3d064efb925ca Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Wed, 9 Apr 2025 19:31:50 -0500
Subject: [PATCH 01/10] CargoPackage class for getting information about a
 cargo project.

---
 kmir/src/kmir/smir/__init__.py |  1 +
 kmir/src/kmir/smir/cargo.py    | 82 ++++++++++++++++++++++++++++++++++
 2 files changed, 83 insertions(+)
 create mode 100644 kmir/src/kmir/smir/__init__.py
 create mode 100644 kmir/src/kmir/smir/cargo.py

diff --git a/kmir/src/kmir/smir/__init__.py b/kmir/src/kmir/smir/__init__.py
new file mode 100644
index 000000000..88deb7760
--- /dev/null
+++ b/kmir/src/kmir/smir/__init__.py
@@ -0,0 +1 @@
+from .cargo import CargoPackage
diff --git a/kmir/src/kmir/smir/cargo.py b/kmir/src/kmir/smir/cargo.py
new file mode 100644
index 000000000..196e79ccc
--- /dev/null
+++ b/kmir/src/kmir/smir/cargo.py
@@ -0,0 +1,82 @@
+from __future__ import annotations
+
+import json
+import subprocess
+from functools import cached_property
+from pathlib import Path
+
+
+class CargoPackage:
+    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]

From 27f3fa076724e62bbf95c4f4267864b5f4df8602 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Wed, 9 Apr 2025 19:34:13 -0500
Subject: [PATCH 02/10] Update `kmir run` to use CargoPackage to find the smir
 json

---
 kmir/src/kmir/__main__.py | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
index 56babf827..81df2e35d 100644
--- a/kmir/src/kmir/__main__.py
+++ b/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.smir import CargoPackage
 
 if TYPE_CHECKING:
     from collections.abc import Sequence
@@ -27,7 +28,7 @@ class KMirOpts: ...
 
 @dataclass
 class RunOpts(KMirOpts):
-    input_file: Path
+    bin: str | None
     depth: int
     start_symbol: str
     haskell_backend: bool
@@ -80,7 +81,12 @@ 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')
+    cargo = CargoPackage(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)
@@ -169,7 +175,7 @@ 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_parser.add_argument('--bin', metavar='TARGET', help='Target to run')
     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'
@@ -212,7 +218,7 @@ def _parse_args(args: Sequence[str]) -> KMirOpts:
     match ns.command:
         case 'run':
             return RunOpts(
-                input_file=Path(ns.input_file).resolve(),
+                bin=ns.bin,
                 depth=ns.depth,
                 start_symbol=ns.start_symbol,
                 haskell_backend=ns.haskell_backend,

From c0c5aba862bc9437b06afa27e0b482f0f02f0606 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Wed, 9 Apr 2025 19:42:40 -0500
Subject: [PATCH 03/10] Generalize kmir.smir -> kmir.rust

---
 kmir/src/kmir/__main__.py                | 2 +-
 kmir/src/kmir/{smir => rust}/__init__.py | 0
 kmir/src/kmir/{smir => rust}/cargo.py    | 0
 3 files changed, 1 insertion(+), 1 deletion(-)
 rename kmir/src/kmir/{smir => rust}/__init__.py (100%)
 rename kmir/src/kmir/{smir => rust}/cargo.py (100%)

diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
index 81df2e35d..bfad2e133 100644
--- a/kmir/src/kmir/__main__.py
+++ b/kmir/src/kmir/__main__.py
@@ -16,7 +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.smir import CargoPackage
+from kmir.rust import CargoPackage
 
 if TYPE_CHECKING:
     from collections.abc import Sequence
diff --git a/kmir/src/kmir/smir/__init__.py b/kmir/src/kmir/rust/__init__.py
similarity index 100%
rename from kmir/src/kmir/smir/__init__.py
rename to kmir/src/kmir/rust/__init__.py
diff --git a/kmir/src/kmir/smir/cargo.py b/kmir/src/kmir/rust/cargo.py
similarity index 100%
rename from kmir/src/kmir/smir/cargo.py
rename to kmir/src/kmir/rust/cargo.py

From 5e797bc8496f967ffc087743a199a5a4d56e0a58 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Wed, 9 Apr 2025 19:45:42 -0500
Subject: [PATCH 04/10] update README

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 03b64749a..7e9a2c9e1 100644
--- a/README.md
+++ b/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. 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
\ No newline at end of file
+- Solana

From 36f90afcb9a0acd538c647ddb5426ce7c2ed91a7 Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Thu, 10 Apr 2025 00:54:34 +0000
Subject: [PATCH 05/10] Set Version: 0.3.115

---
 kmir/pyproject.toml       | 2 +-
 kmir/src/kmir/__init__.py | 2 +-
 package/version           | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml
index 8530c9147..83ce77b08 100644
--- a/kmir/pyproject.toml
+++ b/kmir/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.114"
+version = "0.3.115"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
index 05d59162f..b2980e369 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.114'
+VERSION: Final = '0.3.115'
diff --git a/package/version b/package/version
index 17101bd68..c31612a95 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.3.114
+0.3.115

From 3b56f322310ad81e304779c5bd441c9cb10063cb Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Thu, 10 Apr 2025 10:25:57 +0000
Subject: [PATCH 06/10] Set Version: 0.3.117

---
 kmir/pyproject.toml       | 2 +-
 kmir/src/kmir/__init__.py | 2 +-
 package/version           | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml
index f97e0bb45..cb83c03d9 100644
--- a/kmir/pyproject.toml
+++ b/kmir/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.116"
+version = "0.3.117"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
index 4bae2157a..22185c773 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.116'
+VERSION: Final = '0.3.117'
diff --git a/package/version b/package/version
index 0f068804e..4f252bf70 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.3.116
+0.3.117

From 993c0a2dfeeb04d956b96673d3f0def64456f807 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Wed, 9 Apr 2025 19:49:56 -0500
Subject: [PATCH 07/10] CargoPackage -> CargoProject

---
 kmir/src/kmir/__main__.py      | 4 ++--
 kmir/src/kmir/rust/__init__.py | 2 +-
 kmir/src/kmir/rust/cargo.py    | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
index bfad2e133..d2a230218 100644
--- a/kmir/src/kmir/__main__.py
+++ b/kmir/src/kmir/__main__.py
@@ -16,7 +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 CargoPackage
+from kmir.rust import CargoProject
 
 if TYPE_CHECKING:
     from collections.abc import Sequence
@@ -81,7 +81,7 @@ class ProveViewOpts(KMirOpts):
 def _kmir_run(opts: RunOpts) -> None:
     tools = haskell_semantics() if opts.haskell_backend else llvm_semantics()
 
-    cargo = CargoPackage(Path.cwd())
+    cargo = CargoProject(Path.cwd())
 
     target = opts.bin if opts.bin else cargo.default_target
     smir_file = cargo.smir_for(target)
diff --git a/kmir/src/kmir/rust/__init__.py b/kmir/src/kmir/rust/__init__.py
index 88deb7760..1583aa565 100644
--- a/kmir/src/kmir/rust/__init__.py
+++ b/kmir/src/kmir/rust/__init__.py
@@ -1 +1 @@
-from .cargo import CargoPackage
+from .cargo import CargoProject
diff --git a/kmir/src/kmir/rust/cargo.py b/kmir/src/kmir/rust/cargo.py
index 196e79ccc..967f2191b 100644
--- a/kmir/src/kmir/rust/cargo.py
+++ b/kmir/src/kmir/rust/cargo.py
@@ -6,7 +6,7 @@
 from pathlib import Path
 
 
-class CargoPackage:
+class CargoProject:
     working_directory: Path
 
     def __init__(self, working_directory: Path) -> None:

From b153b5cbce0c8a0f9d82e2b04d001dab8bbb4db3 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Fri, 11 Apr 2025 18:22:41 -0500
Subject: [PATCH 08/10] Add --file option to kmir run to pass a smir json
 directly

---
 kmir/src/kmir/__main__.py | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
index d2a230218..5a33193cc 100644
--- a/kmir/src/kmir/__main__.py
+++ b/kmir/src/kmir/__main__.py
@@ -29,6 +29,7 @@ class KMirOpts: ...
 @dataclass
 class RunOpts(KMirOpts):
     bin: str | None
+    file: str | None
     depth: int
     start_symbol: str
     haskell_backend: bool
@@ -81,10 +82,13 @@ class ProveViewOpts(KMirOpts):
 def _kmir_run(opts: RunOpts) -> None:
     tools = haskell_semantics() if opts.haskell_backend else llvm_semantics()
 
-    cargo = CargoProject(Path.cwd())
-
-    target = opts.bin if opts.bin else cargo.default_target
-    smir_file = cargo.smir_for(target)
+    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:
@@ -175,7 +179,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('--bin', metavar='TARGET', help='Target 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'
@@ -219,6 +225,7 @@ def _parse_args(args: Sequence[str]) -> KMirOpts:
         case 'run':
             return RunOpts(
                 bin=ns.bin,
+                file=ns.file,
                 depth=ns.depth,
                 start_symbol=ns.start_symbol,
                 haskell_backend=ns.haskell_backend,

From 04d376bb6804ad1db154181499518218547b16e5 Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Fri, 11 Apr 2025 23:37:30 +0000
Subject: [PATCH 09/10] Set Version: 0.3.118

---
 kmir/pyproject.toml       | 2 +-
 kmir/src/kmir/__init__.py | 2 +-
 package/version           | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml
index cb83c03d9..ffcec8045 100644
--- a/kmir/pyproject.toml
+++ b/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. <contact@runtimeverification.com>",
diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
index 22185c773..a7553876f 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.117'
+VERSION: Final = '0.3.118'
diff --git a/package/version b/package/version
index 4f252bf70..dfec1413b 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.3.117
+0.3.118

From 6b66357ca810988d04d3858ed104cf219cfb2b59 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 14 Apr 2025 12:44:17 -0500
Subject: [PATCH 10/10] Update README

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 7e9a2c9e1..e9380e91e 100644
--- a/README.md
+++ b/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 run a binary target in your cargo project. 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 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.