Skip to content

Commit 2e6c1b8

Browse files
gtreptarv-auditorjberthold
authored
Update kmir run to behave more like cargo run (#524)
- Introduce `CargoProject` class which can be used to gather information about a cargo project. - `kmir run` now uses `CargoProject` which finds the `.smir.json` artifact in the target directory after invoking `cargo build`. Note that currently either `RUSTC` will need to be set to the `stable-mir-json` install, or the smir json files should already have been built that way and exist in the target directory. Later, we can get rid of this requirement when we package `stable-mir-json` with `kmir`. --------- Co-authored-by: devops <[email protected]> Co-authored-by: Jost Berthold <[email protected]>
1 parent b5e58dc commit 2e6c1b8

File tree

7 files changed

+105
-9
lines changed

7 files changed

+105
-9
lines changed

README.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ Use `--help` with each command for more details.
3636

3737
`parse` to parse a Stable MIR JSON file (`*.smir.json`) file to a K AST
3838

39-
`kmir run` to load an SMIR JSON generated by the `stable-mir-json` tool.
39+
`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`.
4040

4141
`kmir gen-spec` to take a SMIR JSON and create a K specification module that ensures termination of the program.
4242

@@ -48,4 +48,4 @@ Use `--help` with each command for more details.
4848

4949
KMIR / mir-semantics is supported by funding from the following sources:
5050
- [Polkadot Open Gov](https://polkadot.subsquare.io/referenda/749)
51-
- Solana
51+
- Solana

kmir/pyproject.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "kmir"
7-
version = "0.3.117"
7+
version = "0.3.118"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

kmir/src/kmir/__init__.py

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
from typing import Final
22

3-
VERSION: Final = '0.3.117'
3+
VERSION: Final = '0.3.118'

kmir/src/kmir/__main__.py

+17-4
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
from kmir.build import HASKELL_DEF_DIR, LLVM_LIB_DIR, haskell_semantics, llvm_semantics
1717
from kmir.kmir import KMIR, KMIRAPRNodePrinter
1818
from kmir.parse.parser import parse_json
19+
from kmir.rust import CargoProject
1920

2021
if TYPE_CHECKING:
2122
from collections.abc import Sequence
@@ -27,7 +28,8 @@ class KMirOpts: ...
2728

2829
@dataclass
2930
class RunOpts(KMirOpts):
30-
input_file: Path
31+
bin: str | None
32+
file: str | None
3133
depth: int
3234
start_symbol: str
3335
haskell_backend: bool
@@ -80,7 +82,15 @@ class ProveViewOpts(KMirOpts):
8082
def _kmir_run(opts: RunOpts) -> None:
8183
tools = haskell_semantics() if opts.haskell_backend else llvm_semantics()
8284

83-
parse_result = parse_json(tools.definition, opts.input_file, 'Pgm')
85+
smir_file: Path
86+
if opts.file:
87+
smir_file = Path(opts.file).resolve()
88+
else:
89+
cargo = CargoProject(Path.cwd())
90+
target = opts.bin if opts.bin else cargo.default_target
91+
smir_file = cargo.smir_for(target)
92+
93+
parse_result = parse_json(tools.definition, smir_file, 'Pgm')
8494
if parse_result is None:
8595
print('Parse error!', file=sys.stderr)
8696
sys.exit(1)
@@ -170,7 +180,9 @@ def _arg_parser() -> ArgumentParser:
170180
command_parser = parser.add_subparsers(dest='command', required=True)
171181

172182
run_parser = command_parser.add_parser('run', help='run stable MIR programs')
173-
run_parser.add_argument('input_file', metavar='FILE', help='MIR program to run')
183+
run_target_selection = run_parser.add_mutually_exclusive_group()
184+
run_target_selection.add_argument('--bin', metavar='TARGET', help='Target to run')
185+
run_target_selection.add_argument('--file', metavar='SMIR', help='SMIR json file to execute')
174186
run_parser.add_argument('--depth', type=int, metavar='DEPTH', help='Depth to execute')
175187
run_parser.add_argument(
176188
'--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:
213225
match ns.command:
214226
case 'run':
215227
return RunOpts(
216-
input_file=Path(ns.input_file).resolve(),
228+
bin=ns.bin,
229+
file=ns.file,
217230
depth=ns.depth,
218231
start_symbol=ns.start_symbol,
219232
haskell_backend=ns.haskell_backend,

kmir/src/kmir/rust/__init__.py

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
from .cargo import CargoProject

kmir/src/kmir/rust/cargo.py

+82
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
from __future__ import annotations
2+
3+
import json
4+
import subprocess
5+
from functools import cached_property
6+
from pathlib import Path
7+
8+
9+
class CargoProject:
10+
working_directory: Path
11+
12+
def __init__(self, working_directory: Path) -> None:
13+
self.working_directory = working_directory
14+
15+
@cached_property
16+
def metadata(self) -> dict:
17+
"""Metadata about the cargo project"""
18+
19+
command = ['cargo', 'metadata', '--format-version', '1']
20+
command_result = subprocess.run(command, capture_output=True, text=True, cwd=self.working_directory)
21+
metadata = json.loads(command_result.stdout)
22+
return metadata
23+
24+
@cached_property
25+
def manifest(self) -> dict:
26+
"""Information about the Cargo.toml file"""
27+
28+
command = ['cargo', 'read-manifest']
29+
command_result = subprocess.run(command, capture_output=True, text=True, cwd=self.working_directory)
30+
manifest = json.loads(command_result.stdout)
31+
return manifest
32+
33+
@property
34+
def build_messages(self) -> list[dict]:
35+
"""Output of messages from `cargo build`"""
36+
37+
command = ['cargo', 'build', '--message-format=json']
38+
command_result = subprocess.run(command, capture_output=True, text=True, cwd=self.working_directory)
39+
split_command_result = command_result.stdout.splitlines()
40+
messages = [json.loads(message) for message in split_command_result]
41+
return messages
42+
43+
def smir_for(self, target: str) -> Path:
44+
"""Gets the latest smir json in the target directory for the given target. Raises a RuntimeError if none exist."""
45+
46+
is_artifact = lambda message: message.get('reason') == 'compiler-artifact'
47+
is_my_target = lambda artifact: artifact.get('target', {}).get('name') == target
48+
artifact = next(message for message in self.build_messages if is_artifact(message) and is_my_target(message))
49+
executable_name = Path(artifact['executable'])
50+
deps_dir = executable_name.parent / 'deps'
51+
52+
# Get the smir file(s) and sort them by modified time
53+
smir_files = deps_dir.glob(f'{target}*.smir.json')
54+
sorted_smir_files = sorted(smir_files, key=lambda f: f.stat().st_mtime, reverse=True)
55+
56+
if len(sorted_smir_files) == 0:
57+
raise RuntimeError(
58+
f'Unable to find smir json for target {target!r}. Have you built it using stable-mir-json?'
59+
)
60+
61+
# Return the most recently modified smir file
62+
return sorted_smir_files[0]
63+
64+
@cached_property
65+
def default_target(self) -> str:
66+
"""Returns the name of the default binary target. If it can't find a default, raises a RuntimeError"""
67+
68+
default_run = self.manifest.get('default_run')
69+
if isinstance(default_run, str):
70+
return default_run
71+
72+
is_bin = lambda target: any(kind == 'bin' for kind in target.get('kind'))
73+
targets = self.manifest.get('targets')
74+
assert isinstance(targets, list)
75+
bin_targets = [target.get('name') for target in targets if is_bin(target)]
76+
77+
if len(bin_targets) != 1:
78+
raise RuntimeError(
79+
f"Can't determine which binary to run. Use --bin, or the 'default-run' manifest key. Found {bin_targets}"
80+
)
81+
82+
return bin_targets[0]

package/version

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.3.117
1+
0.3.118

0 commit comments

Comments
 (0)