diff --git a/README.md b/README.md index 03b64749a..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 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 \ No newline at end of file +- Solana 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. ", 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/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 76eae7a9f..db9e41aa0 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.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, diff --git a/kmir/src/kmir/rust/__init__.py b/kmir/src/kmir/rust/__init__.py new file mode 100644 index 000000000..1583aa565 --- /dev/null +++ b/kmir/src/kmir/rust/__init__.py @@ -0,0 +1 @@ +from .cargo import CargoProject diff --git a/kmir/src/kmir/rust/cargo.py b/kmir/src/kmir/rust/cargo.py new file mode 100644 index 000000000..967f2191b --- /dev/null +++ b/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] 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