From c03750efcfd2a4fd8a59e785beaf22574987497c Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 9 Mar 2026 10:12:11 +0800 Subject: [PATCH 1/5] docs: streamline README by removing duplication and adding proof workflow Consolidate repeated setup instructions (rustup, git clone, submodule init) into a single Quick Start section. Replace verbose per-command CLI docs with a command table (details available via --help). Add practical "Typical proof workflow" and "Debugging a stuck or failing proof" sections covering show, prune, section-edge, break-on-* flags, and module export/import. --- README.md | 285 +++++++++++++++++++----------------------------------- 1 file changed, 101 insertions(+), 184 deletions(-) diff --git a/README.md b/README.md index 1bb56c483..e348c4fa4 100644 --- a/README.md +++ b/README.md @@ -1,245 +1,162 @@ # MIR Semantics -In this repository, we provide a model of the semantics of Rust's Stable MIR in K to enable symbolic execution of Rust programs and proofs of program properties. +`mir-semantics` models the semantics of Rust Stable MIR in K. The repository also ships `kmir`, a Python CLI for building the semantics, running programs, generating specs, and inspecting proofs. -Also included is the `kmir` tool, a python script that acts as a front-end to the semantics. +For semantics details and specialized workflows, see [Further Reading](#further-reading). +## Quick Start -## For Developers +### Prerequisites -### KMIR Setup - -Pre-requisites: -- `python >= 3.10` +- [Python](https://www.python.org/) `>= 3.10` - [`uv`](https://docs.astral.sh/uv/) -- `pip >= 20.0.2` -- `gcc >= 11.4.0` -- `cargo == nightly-2024-11-29` -- K. The required K version is specified in `deps/k_release`. To install K, follow the steps available in [K's Quick Start instructions](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start). +- [`pip`](https://pip.pypa.io/) `>= 20.0.2` +- [`gcc`](https://gcc.gnu.org/) `>= 11.4.0` +- [Rust](https://rustup.rs/) via `rustup` +- [K Framework](https://github.com/runtimeverification/k?tab=readme-ov-file#quick-start), using the version pinned in [`deps/k_release`](deps/k_release) -```bash -make build -``` +### Clone and set up -Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list of available targets). +```bash +git clone --recurse-submodules https://github.com/runtimeverification/mir-semantics.git +cd mir-semantics -For interactive use, first sync the environment with `uv --directory kmir sync`, then either: -- Run Python directly: `uv --directory kmir run python` -- Activate the virtual environment: `source kmir/.venv/bin/activate` (on Unix/macOS) or `kmir\.venv\Scripts\activate` (on Windows) -- Or directly run commands from `mir-semantics` root: `uv --directory kmir run kmir ` +# If you cloned without --recurse-submodules: +git submodule update --init --recursive +``` -### Stable-MIR-JSON Setup +### Build -To interact with some of KMIR functionalities, it is necessary to provide the tool with a serialized JSON of a Rust program's Stable MIR. To be able to extract these serialized SMIR JSONs, you can use the `Stable-MIR-JSON` tool. +The pinned Rust toolchain and components are declared in [`rust-toolchain.toml`](rust-toolchain.toml) and installed automatically by `rustup` on first use. -#### Quick Start ```bash -git submodule update --init --recursive +# Build K semantics definitions (required for kmir) +make build + +# Build stable-mir-json (required for SMIR generation, integration tests) make stable-mir-json ``` -#### Generating SMIR JSON Files +`uv` will create and use the Python environment for the `kmir` project automatically. -After setting up stable-mir-json, you can generate SMIR JSON files from Rust source code: +### Verify the setup -**Using the stable-mir-json tool directly:** ```bash -# For single files -deps/.stable-mir-json/debug.sh -Zno-codegen your_file.rs +# Just kmir +uv --project kmir run kmir --help -# For cargo projects -RUSTC=deps/.stable-mir-json/debug.sh cargo build +# Full contributor check +make smir-parse-tests ``` -**Using the convenience script:** -```bash -# Generate JSON file -./scripts/generate-smir-json.sh your_file.rs . +## Common Workflows -# Generate with visualization (PNG, PDF, DOT) -./scripts/generate-smir-json.sh your_file.rs . png -./scripts/generate-smir-json.sh your_file.rs . pdf -./scripts/generate-smir-json.sh your_file.rs . dot -``` +### Task-to-command map -For more information on testing, installation, and general usage of this tool, please check [Stable-MIR-JSON's repository](https://github.com/runtimeverification/stable-mir-json/). +| Task | Command | Notes | +| --- | --- | --- | +| Build the semantics | `make build` | Requires K and the Python prerequisites. | +| Build `stable-mir-json` in-tree | `make stable-mir-json` | Requires initialized submodules and the pinned Rust nightly. | +| Run unit tests | `make test-unit` | Python-only tests under `kmir/src/tests/unit`. | +| Run integration tests | `make test-integration` | Depends on `stable-mir-json` and `build`. | +| Check Stable MIR parsing | `make smir-parse-tests` | Compiles Rust test programs to SMIR JSON and parses them with `kmir`. | -## Usage +`make test-integration` already depends on `make stable-mir-json` and `make build`, so it is the full contributor path for integration coverage. -Use `--help` with each command for more details. +## Using `kmir` -### Basic Commands +Every subcommand supports `--help` for the full option list. -**`kmir run`** - Execute a Rust program from SMIR JSON or directly from source -```bash -# Run from SMIR JSON file -uv --project kmir run kmir run --file path/to/program.smir.json +| Command | Purpose | +| --- | --- | +| `kmir run` | Execute a Rust program from SMIR JSON | +| `kmir prove-rs` | 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 | +| `kmir prune` | Remove a node (and its subtree) from a proof | +| `kmir section-edge` | Split a proof edge into finer sections | +| `kmir link` | Link multiple SMIR JSON files into one | +| `kmir info` | Show type information from a SMIR JSON file | -# Run with verbose output -uv --project kmir run kmir run --file path/to/program.smir.json --verbose -``` +### Typical proof workflow -**`kmir prove-rs`** - Directly prove properties of Rust source code (recommended) ```bash -# Basic proof -uv --project kmir run kmir prove-rs path/to/program.rs +# 1. Run a proof +uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs --verbose -# Detailed proof with output -uv --project kmir run kmir prove-rs path/to/program.rs --verbose --proof-dir ./proof_dir -``` +# 2. Overview — see all leaves and statistics +uv --project kmir run kmir show proof_id --proof-dir ./proofs --leaves --statistics -**`kmir gen-spec`** - Generate K specification from SMIR JSON -```bash -uv --project kmir run kmir gen-spec path/to/program.smir.json --output-file path/to/spec.k -``` +# 3. Zoom into specific nodes / transitions +uv --project kmir run kmir show proof_id --proof-dir ./proofs --nodes "4,5" --node-deltas "4:5" -**`kmir link`** - Link together multiple SMIR JSON files -```bash -# Link multiple SMIR JSON files into a single output file -uv --project kmir run kmir link file1.smir.json file2.smir.json file3.smir.json --output-file linked.smir.json +# 4. See which K rules fired on an edge +uv --project kmir run kmir show proof_id --proof-dir ./proofs --rules "4:5" -# Use default output filename (linker_output.smir.json) -uv --project kmir run kmir link file1.smir.json file2.smir.json +# 5. Full detail for deep debugging +uv --project kmir run kmir show proof_id --proof-dir ./proofs --nodes "5" \ + --full-printer --no-omit-static-info --no-omit-current-body ``` -**`kmir info`** - Inspect SMIR JSON metadata (currently: types) -```bash -# Show information about specific type IDs in a SMIR JSON -uv --project kmir run kmir info path/to/program.smir.json --types "1,2,3" - -# Notes -# - The --types option accepts a comma-separated list of numeric Stable MIR type IDs. -# - Output format: one line per requested type, e.g.: -# Type Ty(1): Int(....) -# Type Ty(2): StructT(name=..., adt_def=..., fields=[...]) -# - If --types is omitted, the command currently produces no output. -``` +### Debugging a stuck or failing proof -### Analysis Commands +When a proof does not close, the typical cycle is **inspect → refine → re-prove**: -**`kmir show`** - Display proof information with advanced filtering options ```bash -# Basic usage -uv --project kmir run kmir show proof_id --proof-dir ./proof_dir - -# Show specific nodes only -uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3" - -# Show node deltas (transitions between specific nodes) -uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2,3:4" +# Narrow down where things go wrong — break on every function call +uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs \ + --break-on-calls --max-depth 200 -# Show additional deltas after the main output, and also print rules for those edges -uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2" --node-deltas-pro "3:4" +# Or break only when a specific function is entered +uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs \ + --break-on-function "my_module::suspect_fn" -# Display full node information (default is compact) -uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer - -# Show static information cells (functions, types, etc.) -uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-static-info - -# Show current body cell content -uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-current-body - -# Omit specific cells from output -uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --omit-cells "cell1,cell2" - -# Combine multiple options for detailed analysis -uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info --nodes "1,2" --verbose -``` +# Split a large edge to find the exact divergence point +uv --project kmir run kmir section-edge proof_id "4,5" --proof-dir ./proofs --sections 4 -**`kmir view`** - Detailed view of proof results -```bash -uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose -``` +# Prune a bad subtree and re-run +uv --project kmir run kmir prune proof_id 5 --proof-dir ./proofs +uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs -**Rules within `kmir show`** - Show rules applied between nodes -```bash -uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --rules "SOURCE:TARGET[,SOURCE:TARGET...]" +# Export a proof subgraph as a reusable K module +uv --project kmir run kmir show proof_id --proof-dir ./proofs --to-module lemma.json --minimize-proof +# then re-prove with the lemma +uv --project kmir run kmir prove-rs program.rs --proof-dir ./proofs --add-module lemma.json ``` -### Recommended Workflow - -1. **Setup Environment**: - ```bash - make stable-mir-json # Setup stable-mir-json - make build # Build K definitions - ``` - -2. **Direct Proof** (Recommended): - ```bash - uv --project kmir run kmir prove-rs your_file.rs --verbose --proof-dir ./proof_dir - ``` - -3. **View Results**: - ```bash - # Quick overview (compact format, static info hidden) - uv --project kmir run kmir show proof_id --proof-dir ./proof_dir - - # Detailed analysis with full information - uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info - - # Focus on specific nodes - uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3" - - # Interactive view - uv --project kmir run kmir view proof_id --proof-dir ./proof_dir --verbose - ``` - -4. **Analyze Rules**: - ```bash - uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --rules "1:3" - ``` - -### Advanced Show Usage Examples - -**Debugging workflow:** -```bash -# 1. Start with a quick overview -uv --project kmir run kmir show my_proof --proof-dir ./proofs - -# 2. Focus on problematic nodes (e.g., nodes 5, 6, 7) -uv --project kmir run kmir show my_proof --proof-dir ./proofs --nodes "5,6,7" +Other useful `prove-rs` break flags: `--break-every-step`, `--break-every-terminator`, `--break-on-thunk`, `--terminate-on-thunk`. -# 3. Examine transitions between specific nodes -uv --project kmir run kmir show my_proof --proof-dir ./proofs --node-deltas "5:6,6:7" +### Generate Stable MIR JSON manually -# 4. Get full details for deep debugging -uv --project kmir run kmir show my_proof --proof-dir ./proofs --nodes "6" --full-printer --no-omit-static-info --no-omit-current-body -``` +After `make stable-mir-json`: -**Performance analysis:** ```bash -# Hide verbose cells but show execution flow -uv --project kmir run kmir show my_proof --proof-dir ./proofs --omit-cells "locals,heap" --verbose +# Single file +deps/.stable-mir-json/debug.sh -Zno-codegen your_file.rs -# Focus on function calls and type information -uv --project kmir run kmir show my_proof --proof-dir ./proofs --no-omit-static-info --omit-cells "currentBody" +# Cargo project +RUSTC=deps/.stable-mir-json/debug.sh cargo build + +# Convenience script (also supports png/pdf/dot visualization) +./scripts/generate-smir-json.sh your_file.rs . png ``` -### Command Options +## Troubleshooting -Most commands support: -- `--verbose, -v`: Detailed output -- `--debug`: Debug information -- `--proof-dir DIR`: Directory for proof results -- `--max-depth DEPTH`: Maximum execution depth -- `--max-iterations ITERATIONS`: Maximum iterations +- **Rust toolchain errors**: The toolchain is declared in [`rust-toolchain.toml`](rust-toolchain.toml) and should install automatically on first use. If not, run `rustup toolchain install nightly-2024-11-29 --component llvm-tools --component rustc-dev --component rust-src`. +- **`deps/stable-mir-json` is missing**: Run `git submodule update --init --recursive`. +- **Not sure which `make` target to run**: `make build` for basic `kmir`; add `make stable-mir-json` for SMIR generation; `make test-integration` for the full suite. -**`kmir show` specific options:** -- `--nodes NODES`: Comma separated list of node IDs to show (e.g., "1,2,3") -- `--node-deltas DELTAS`: Comma separated list of node deltas in format "source:target" (e.g., "1:2,3:4") -- `--node-deltas-pro DELTAS`: Additional node deltas (same format as `--node-deltas`). Equivalent to "print the corresponding deltas again, and automatically print the rules for these edges". -- `--rules EDGES`: Comma separated list of edges in format "source:target". Prints rules for each edge in Markdown link format `[label](file:///abs/path#LstartLine)` when available -- `--omit-cells CELLS`: Comma separated list of cell names to omit from output -- `--full-printer`: Display the full node in output (default is compact) -- `--no-omit-static-info`: Display static information cells (functions, start-symbol, types, adt-to-ty) -- `--no-omit-current-body`: Display the `` cell completely -- `--smir-info SMIR_INFO`: Path to SMIR JSON file to improve debug messaging +## Further Reading -For complete options, use `--help` with each command. +- [docs/semantics-of-mir.md](docs/semantics-of-mir.md) +- [docs/example-mir-execution-flow.md](docs/example-mir-execution-flow.md) +- [docs/dev/adding-intrinsics.md](docs/dev/adding-intrinsics.md) +- [docs/feature-checklist.md](docs/feature-checklist.md) +- [Stable-MIR-JSON repository](https://github.com/runtimeverification/stable-mir-json/) -### Supporters +## Supporters -KMIR / mir-semantics is supported by funding from the following sources: +KMIR / mir-semantics is supported by funding from: - [Polkadot Open Gov](https://polkadot.subsquare.io/referenda/749) - Solana From 569f9e2143b9240dade13b1f7acba737c8c6c627 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 9 Mar 2026 10:25:13 +0800 Subject: [PATCH 2/5] docs: improve CLI --help descriptions for info, show, and link - info --types: document output format and behavior when omitted - show --node-deltas-pro: clarify it also prints rules for the edges - show --rules: note output is Markdown links to K rule sources - link --output-file: show default value (linker_output.smir.json) --- kmir/src/kmir/__main__.py | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 0f9fff0db..99a02d6bd 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -300,7 +300,11 @@ def _arg_parser() -> ArgumentParser: 'info', help='Show information about a SMIR JSON file', parents=[kcli_args.logging_args] ) info_parser.add_argument('smir_file', metavar='FILE', help='SMIR JSON file to analyze') - info_parser.add_argument('--types', metavar='TYPES', help='Comma separated list of type IDs to show details for') + info_parser.add_argument( + '--types', + metavar='TYPES', + help='Comma separated list of type IDs to show (e.g. "1,2,3"). Output: one line per type, e.g. "Type Ty(1): Int(...)". Omit to produce no output.', + ) prove_args = ArgumentParser(add_help=False) prove_args.add_argument('--proof-dir', metavar='DIR', help='Proof directory') @@ -455,7 +459,9 @@ def _arg_parser() -> ArgumentParser: '--node-deltas', metavar='DELTAS', help='Comma separated list of node deltas in format "source:target"' ) show_parser.add_argument( - '--node-deltas-pro', metavar='DELTAS', help='Extra node deltas (printed after main output)' + '--node-deltas-pro', + metavar='DELTAS', + help='Extra node deltas in format "source:target" (printed after main output, also prints rules for these edges)', ) show_parser.add_argument( '--omit-cells', metavar='CELLS', help='Comma separated list of cell names to omit from output' @@ -485,7 +491,11 @@ def _arg_parser() -> ArgumentParser: help='Print the cell for each leaf node in the proof graph', ) - show_parser.add_argument('--rules', metavar='EDGES', help='Comma separated list of edges in format "source:target"') + show_parser.add_argument( + '--rules', + metavar='EDGES', + help='Comma separated list of edges in format "source:target". Prints the K rules applied on each edge as Markdown links.', + ) show_parser.add_argument( '--to-module', type=Path, @@ -547,7 +557,7 @@ def _arg_parser() -> ArgumentParser: ) link_parser.add_argument('smir_files', nargs='+', metavar='SMIR_JSON', help='SMIR JSON files to link') link_parser.add_argument( - '--output-file', '-o', metavar='FILE', help='Output file', default='linker_output.smir.json' + '--output-file', '-o', metavar='FILE', help='Output file (default: linker_output.smir.json)', default='linker_output.smir.json' ) return parser From f32e59544a74048b8e95b00affbb14b643e24585 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 9 Mar 2026 10:28:03 +0800 Subject: [PATCH 3/5] docs: improve CLI --help descriptions across all subcommands - run: clarify --bin is cargo target, --file is SMIR JSON, note mutual exclusivity; --depth explains "execution steps" - prove-rs: --max-depth explains KCFG edge semantics; --reload warns it discards progress; --break-on-function clarifies substring matching - show: --full-printer notes default is compact; --minimize-proof notes it requires --to-module - prune: NODE explains subtree removal - section-edge: edge help uses clearer wording - proof_args: PROOF_ID uses generic "operate on" instead of "view" --- kmir/src/kmir/__main__.py | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 99a02d6bd..27ba2ec6d 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -284,10 +284,10 @@ def _arg_parser() -> ArgumentParser: 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='Target to run') - run_target_selection.add_argument('--file', metavar='SMIR', help='SMIR json file to execute') + run_target_selection.add_argument('--bin', metavar='TARGET', help='Cargo binary target name to run (mutually exclusive with --file)') + run_target_selection.add_argument('--file', metavar='SMIR', help='SMIR JSON file to execute (mutually exclusive with --bin)') 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='Depth to execute') + run_parser.add_argument('--depth', type=int, metavar='DEPTH', help='Maximum number of execution steps') run_parser.add_argument( '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from' ) @@ -311,11 +311,13 @@ def _arg_parser() -> ArgumentParser: prove_args.add_argument('--haskell-target', metavar='TARGET', help='Haskell target to use') prove_args.add_argument('--llvm-lib-target', metavar='TARGET', help='LLVM lib target to use') prove_args.add_argument('--bug-report', metavar='PATH', help='path to optional bug report') - prove_args.add_argument('--max-depth', metavar='DEPTH', type=int, help='max steps to take between nodes in kcfg') + prove_args.add_argument( + '--max-depth', metavar='DEPTH', type=int, help='Maximum K rewrite steps to take on a single KCFG edge before creating a new node' + ) prove_args.add_argument( '--max-iterations', metavar='ITERATIONS', type=int, help='max number of proof iterations to take' ) - prove_args.add_argument('--reload', action='store_true', help='Force restarting proof') + prove_args.add_argument('--reload', action='store_true', help='Discard any existing proof progress and restart from scratch') prove_args.add_argument( '--fail-fast', dest='fail_fast', @@ -419,11 +421,11 @@ def _arg_parser() -> ArgumentParser: dest='break_on_function', action='append', default=None, - help='Break when calling functions / intrinsics matching this name (repeatable)', + help='Break when calling a function or intrinsic whose name contains this string (repeatable)', ) proof_args = ArgumentParser(add_help=False) - proof_args.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view') + proof_args.add_argument('id', metavar='PROOF_ID', help='The id of the proof to operate on') proof_args.add_argument('--proof-dir', metavar='DIR', help='Proof directory') display_args = ArgumentParser(add_help=False) @@ -432,7 +434,7 @@ def _arg_parser() -> ArgumentParser: dest='full_printer', action='store_true', default=False, - help='Display the full node in output.', + help='Display full K configuration for each node (default: compact view).', ) display_args.add_argument( '--smir-info', @@ -505,7 +507,7 @@ def _arg_parser() -> ArgumentParser: show_parser.add_argument( '--minimize-proof', action='store_true', - help='Minimize the proof KCFG before exporting to module', + help='Minimize the proof KCFG before exporting to module (only used with --to-module)', ) command_parser.add_parser( @@ -515,13 +517,13 @@ def _arg_parser() -> ArgumentParser: prune_parser = command_parser.add_parser( 'prune', help='Prune a proof from a given node', parents=[kcli_args.logging_args, proof_args] ) - prune_parser.add_argument('node_id', metavar='NODE', type=int, help='The node to prune') + prune_parser.add_argument('node_id', metavar='NODE', type=int, help='The node to prune (removes this node and its entire subtree)') section_edge_parser = command_parser.add_parser( 'section-edge', help='Break an edge into sections', parents=[kcli_args.logging_args, proof_args] ) section_edge_parser.add_argument( - 'edge', type=lambda s: tuple(s.split(',')), help='Edge to section in CFG (format: `source,target`)' + 'edge', type=lambda s: tuple(s.split(',')), help='Edge to split in the KCFG (format: "source,target")' ) section_edge_parser.add_argument( '--sections', type=int, default=2, help='Number of sections to make from edge (>= 2, default: 2)' From 90d42bf1aebdf8d621f20920d01f53313881a925 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 9 Mar 2026 10:30:25 +0800 Subject: [PATCH 4/5] style: apply black formatting to CLI help strings --- kmir/src/kmir/__main__.py | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index 27ba2ec6d..42d71ce5d 100644 --- a/kmir/src/kmir/__main__.py +++ b/kmir/src/kmir/__main__.py @@ -284,8 +284,12 @@ def _arg_parser() -> ArgumentParser: 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_target_selection.add_argument('--file', metavar='SMIR', help='SMIR JSON file to execute (mutually exclusive with --bin)') + run_target_selection.add_argument( + '--bin', metavar='TARGET', help='Cargo binary target name to run (mutually exclusive with --file)' + ) + run_target_selection.add_argument( + '--file', metavar='SMIR', help='SMIR JSON file to execute (mutually exclusive with --bin)' + ) 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') run_parser.add_argument( @@ -312,12 +316,17 @@ def _arg_parser() -> ArgumentParser: prove_args.add_argument('--llvm-lib-target', metavar='TARGET', help='LLVM lib target to use') prove_args.add_argument('--bug-report', metavar='PATH', help='path to optional bug report') prove_args.add_argument( - '--max-depth', metavar='DEPTH', type=int, help='Maximum K rewrite steps to take on a single KCFG edge before creating a new node' + '--max-depth', + metavar='DEPTH', + type=int, + help='Maximum K rewrite steps to take on a single KCFG edge before creating a new node', ) prove_args.add_argument( '--max-iterations', metavar='ITERATIONS', type=int, help='max number of proof iterations to take' ) - prove_args.add_argument('--reload', action='store_true', help='Discard any existing proof progress and restart from scratch') + prove_args.add_argument( + '--reload', action='store_true', help='Discard any existing proof progress and restart from scratch' + ) prove_args.add_argument( '--fail-fast', dest='fail_fast', @@ -517,7 +526,9 @@ def _arg_parser() -> ArgumentParser: prune_parser = command_parser.add_parser( 'prune', help='Prune a proof from a given node', parents=[kcli_args.logging_args, proof_args] ) - prune_parser.add_argument('node_id', metavar='NODE', type=int, help='The node to prune (removes this node and its entire subtree)') + prune_parser.add_argument( + 'node_id', metavar='NODE', type=int, help='The node to prune (removes this node and its entire subtree)' + ) section_edge_parser = command_parser.add_parser( 'section-edge', help='Break an edge into sections', parents=[kcli_args.logging_args, proof_args] @@ -559,7 +570,11 @@ def _arg_parser() -> ArgumentParser: ) link_parser.add_argument('smir_files', nargs='+', metavar='SMIR_JSON', help='SMIR JSON files to link') link_parser.add_argument( - '--output-file', '-o', metavar='FILE', help='Output file (default: linker_output.smir.json)', default='linker_output.smir.json' + '--output-file', + '-o', + metavar='FILE', + help='Output file (default: linker_output.smir.json)', + default='linker_output.smir.json', ) return parser From 0c9f5d1fd3677225afd2f86f0084ff0125f21805 Mon Sep 17 00:00:00 2001 From: JianHong Zhao Date: Tue, 10 Mar 2026 10:40:52 +0800 Subject: [PATCH 5/5] Clarify generate-smir-json.sh usage in README Updated script usage instructions in README. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index e348c4fa4..40cf7736c 100644 --- a/README.md +++ b/README.md @@ -138,7 +138,7 @@ deps/.stable-mir-json/debug.sh -Zno-codegen your_file.rs RUSTC=deps/.stable-mir-json/debug.sh cargo build # Convenience script (also supports png/pdf/dot visualization) -./scripts/generate-smir-json.sh your_file.rs . png +./scripts/generate-smir-json.sh [png|pdf|dot] ``` ## Troubleshooting