Bedrock, Fault lines and Striking Gold by cds-amal · Pull Request #144 · runtimeverification/stable-mir-json

cds-amal · 2026-03-11T00:59:58Z

So far, the integration test golden files live next to the test programs (tests/integration/programs/*.expected), and the normalise filter uses hardcoded per-field rules to strip interned indices. This works fine when you only support one nightly. It stops working the moment you need to support multiple nightlies in parallel: each nightly may produce structurally different MIR output (new enum variants, removed fields, renamed types), so a single set of golden files can't serve as the expected output for all of them.

This PR introduces the infrastructure to solve that problem, in four parts:

build.rs breakpoint detection: parses rustc -vV's commit-date and emits cargo:rustc-cfg flags for 16 known API breakpoints. The compat layer uses these flags to gate match arms and import paths, so the same codebase compiles against any nightly from 2024-11-29 through 2026-01-15. The breakpoints table is date-sorted, with a naming convention (smir_has_ for additions, smir_no_ for removals) that makes it straightforward to extend.
Per-nightly golden file directories: expected outputs move from flat tests/integration/programs/*.expected to tests/integration/expected//. The Makefile's integration-test target auto-detects the active nightly from rustc -vV and selects the matching golden directory, falling back to the pinned nightly if no directory exists for the active one.
Receipt-driven normalise filter: the jq filter now reads the companion *.smir.receipts.json (from PR Keep the receipts: interned index tracking for deterministic normalization #143) and applies interned-index normalization generically. No more hardcoded per-field rules; the filter walks the JSON tree and strips any key, newtype, or array position that the receipts declare as interned. This is where the receipts system pays off: new interned fields are handled automatically without filter updates.
nightly_admin.py: a Python script (with Make targets nightly-add, nightly-check, nightly-bump) that formalizes the manual workflow for absorbing a new nightly. add installs the toolchain, generates golden files, and emits UI test lists; check runs integration + UI tests against a specific nightly; bump updates rust-toolchain.toml and README.md. What used to be a sequence of a dozen shell commands and file edits is now a single invocation.

This PR also includes the compat code for the first five breakpoints (nightly-2024-12-14 through nightly-2025-03-01) and the initial set of receipt-normalized golden files for nightly-2025-03-01. The subsequent nightly PRs in this stack each add one breakpoint and its corresponding golden files; they're small and mechanical by design, because all the infrastructure is here.

Test plan

cargo build passes (breakpoint detection should activate the first five flags)
cargo clippy -- -Dwarnings passes
make integration-test passes (auto-selects tests/integration/expected/nightly-2025-03-01/ golden files with receipt-driven normalization)
make golden regenerates golden files into the correct per-nightly directory

Copilot

Pull request overview

This PR introduces infrastructure to support multiple Rust nightly toolchains in parallel by adding compile-time breakpoint detection, per-nightly golden directories, and tooling to manage nightly workflows.

Changes:

Added build.rs to detect rustc commit-date and emit cfg flags for stable MIR API breakpoints.
Updated graph rendering/compat code to use breakpoint-gated match arms for nightly API differences.
Added scripts/nightly_admin.py to automate adding/checking/bumping nightlies; updated integration expected outputs under a per-nightly directory.

Reviewed changes

Copilot reviewed 15 out of 38 changed files in this pull request and generated 9 comments.

Show a summary per file

File	Description
tests/integration/expected/nightly-2025-03-01/enum.smir.json.expected	Updated per-nightly golden output for enum integration test
tests/integration/expected/nightly-2025-03-01/double-ref-deref.smir.json.expected	Updated per-nightly golden output for double-ref-deref integration test
tests/integration/expected/nightly-2025-03-01/div.smir.json.expected	Updated per-nightly golden output for div integration test
tests/integration/expected/nightly-2025-03-01/closure-no-args.smir.json.expected	Updated per-nightly golden output for closure-no-args integration test
tests/integration/expected/nightly-2025-03-01/char-trivial.smir.json.expected	Updated per-nightly golden output for char-trivial integration test
src/mk_graph/util.rs	Added breakpoint-gated handling for MIR enum variants in labeling and updated pattern matches
src/mk_graph/output/dot.rs	Updated terminator-kind pattern matching for DOT output
src/mk_graph/context.rs	Added breakpoint-gated rendering for API changes (e.g., `AddressOf`) and updated pattern matches
src/driver.rs	Added breakpoint-gated switch between `RunCompiler` and `run_compiler()`
src/compat/mono_collect.rs	Added breakpoint-gated handling for `collect_and_partition_mono_items()` return shape change
scripts/nightly_admin.py	New CLI tool to automate nightly add/check/bump workflows and artifact generation
build.rs	New build script emitting `cfg` flags based on rustc commit-date breakpoints

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-03-11T16:27:42Z

src/mk_graph/util.rs

 impl GraphLabelString for AggregateKind {
    fn label(&self) -> String {
        use AggregateKind::*;
        match &self {
            Array(_ty) => "Array".to_string(),
-            Tuple {} => "Tuple".to_string(),
+            Tuple => "Tuple".to_string(),
            Adt(_, idx, _, _, _) => format!("Adt{{{}}}", idx.to_index()),


Tuple here is matched as a unit variant, but older/newer stable MIR nightlies may represent AggregateKind::Tuple as a fieldless struct variant (Tuple {}), in which case Tuple will not compile. Given the PR’s stated goal of compiling across a nightly range, this needs a breakpoint-gated pair of arms (and a corresponding entry in build.rs) so both enum shapes are supported.

Copilot · 2026-03-11T16:27:43Z

src/mk_graph/util.rs

            result.push(targets.otherwise());
            result
        }
-        Resume {} | Abort {} | Return {} | Unreachable {} => vec![],
+        Resume | Abort | Return | Unreachable => vec![],
        Drop { target, unwind, .. } => {


Changing these patterns to unit-variant matches (Resume | Abort | ...) will fail to compile on nightlies where TerminatorKind::{Resume,Abort,Return,Unreachable} are fieldless struct variants (previously matched as Return {} etc.). To keep compatibility across supported nightlies, gate the pattern shape behind a breakpoint cfg (similar to the AddressOf handling) and add the breakpoint to build.rs.

Copilot · 2026-03-11T16:27:43Z

src/mk_graph/output/dot.rs

+                                    Resume => {
                                        label_strs.push("Resume".to_string());
                                    }
-                                    Abort {} => {
+                                    Abort => {
                                        label_strs.push("Abort".to_string());
                                    }
-                                    Return {} => {
+                                    Return => {
                                        label_strs.push("Return".to_string());
                                    }
-                                    Unreachable {} => {
+                                    Unreachable => {


Same issue as in terminator_targets: these unit-variant patterns won’t compile if the targeted nightly encodes these as fieldless struct variants. Since this code sits in the DOT output path, it should be breakpoint-gated for exhaustiveness/compilation on all supported nightlies.

Copilot · 2026-03-11T16:27:43Z

src/mk_graph/context.rs

+            ConstEvalCounter => "ConstEvalCounter".to_string(),
+            Nop => "Nop".to_string(),


These were previously matched as ConstEvalCounter {} / Nop {}; switching to unit-variant patterns will fail to compile on nightlies where they are fieldless struct variants. If the intent is cross-nightly support, add a breakpoint and gate these match arms (or provide both shapes under cfg), consistent with the PR’s compat strategy.

Copilot · 2026-03-11T16:27:44Z

src/driver.rs

+    #[cfg(not(smir_has_run_compiler_fn))]
    let _ = rustc_driver::RunCompiler::new(args_outer, &mut callbacks).run();
+    #[cfg(smir_has_run_compiler_fn)]
+    rustc_driver::run_compiler(args_outer, &mut callbacks);


If rustc_driver::run_compiler(...) returns a Result (common in rustc driver APIs), dropping it may trigger a must_use warning and break -Dwarnings. Consider mirroring the older branch’s behavior (e.g., explicitly binding to _ or handling the result) to avoid warnings on the nightlies where this branch is active.

Suggested change

rustc_driver::run_compiler(args_outer, &mut callbacks);

let _ = rustc_driver::run_compiler(args_outer, &mut callbacks);

Copilot · 2026-03-11T16:27:44Z

build.rs

+    let commit_date = detect_commit_date();
+    eprintln!("build.rs: rustc commit-date: {commit_date}");


Two issues here: (1) detect_commit_date() doesn’t check output.status.success(), so a failing rustc -vV can produce a confusing parse error instead of a clear failure message. (2) emitting diagnostics via eprintln! in build scripts can be noisy and non-standard; prefer println!(\"cargo:warning=...\") (or gate verbose logs behind an env var) so output is surfaced consistently by Cargo.

Copilot · 2026-03-11T16:27:44Z

build.rs

+    let output = Command::new("rustc")
+        .args(["-vV"])
+        .output()
+        .expect("failed to run `rustc -vV`");
+
+    let stdout = String::from_utf8(output.stdout).expect("rustc -vV produced non-UTF-8 output");


Two issues here: (1) detect_commit_date() doesn’t check output.status.success(), so a failing rustc -vV can produce a confusing parse error instead of a clear failure message. (2) emitting diagnostics via eprintln! in build scripts can be noisy and non-standard; prefer println!(\"cargo:warning=...\") (or gate verbose logs behind an env var) so output is surfaced consistently by Cargo.

Copilot · 2026-03-11T16:27:44Z

scripts/nightly_admin.py

+        1 for line in path.read_text().splitlines()
+        if line.strip() and not line.startswith("#")


count_lines() treats lines like ' # comment' as non-comment (because it checks line.startswith('#') before stripping). This can inflate counts and misreport effective list sizes. Use a stripped or left-stripped check for the comment prefix (e.g., check after lstrip()), keeping the behavior aligned with typical TSV comment handling.

Suggested change

1 for line in path.read_text().splitlines()

if line.strip() and not line.startswith("#")

1

for line in path.read_text().splitlines()

if (stripped := line.lstrip()) and not stripped.startswith("#")

Copilot · 2026-03-11T16:27:45Z

scripts/nightly_admin.py

+
+    # 4. Directive parser tests
+    log_step("Directive parser tests")
+    r = run(["make", "test-directives"], check=False)


check is described as running tests against a specific nightly, but this step doesn’t pass the toolchain-forcing environment (env=toolchain_env(...)). That means make test-directives may run under the caller’s default toolchain instead of the target nightly, producing inconsistent results. Pass the same env used by the other steps (or explicitly document why this target is toolchain-independent).

Suggested change

r = run(["make", "test-directives"], check=False)

r = run(["make", "test-directives"], env=env, check=False)

…structure Add build.rs with a breakpoint table that detects the active rustc nightly's commit-date and emits cfg flags for stable MIR API changes. Add nightly_admin.py for managing nightly toolchains (add/check/bump). Update normalise-filter.jq for receipt-driven normalization. Add pr.md to .gitignore.

…ough 2025-03-01)

Move integration test expected outputs from flat files in programs/ to per-nightly directories under expected/nightly-2025-03-01/, enabling the test harness to select the correct golden files for the active toolchain.

This was referenced Mar 11, 2026

Read the room, skip the rest #145

Open

All Nightlies Must Pass #146

Open

cds-amal requested review from Stevengre, Copilot and dkcumming March 11, 2026 16:24

Copilot AI reviewed Mar 11, 2026

View reviewed changes

cds-amal force-pushed the stack/pr2-receipts branch from 4f98f78 to 3a9432c Compare March 11, 2026 19:38

cds-amal force-pushed the stack/pr3-golden-infra branch from d440b10 to f7b4f55 Compare March 11, 2026 19:38

cds-amal added 3 commits March 12, 2026 21:11

feat(compat): add compat code for initial breakpoints (2025-01-24 thr…

293bd90

…ough 2025-03-01)

test: migrate golden files to per-nightly directories

273f002

Move integration test expected outputs from flat files in programs/ to per-nightly directories under expected/nightly-2025-03-01/, enabling the test harness to select the correct golden files for the active toolchain.

cds-amal force-pushed the stack/pr3-golden-infra branch from f7b4f55 to 273f002 Compare March 13, 2026 01:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Bedrock, Fault lines and Striking Gold#144

Bedrock, Fault lines and Striking Gold#144
cds-amal wants to merge 3 commits intostack/pr2-receiptsfrom
stack/pr3-golden-infra

cds-amal commented Mar 11, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Mar 11, 2026

Uh oh!

Copilot AI Mar 11, 2026

Uh oh!

Copilot AI Mar 11, 2026

Uh oh!

Copilot AI Mar 11, 2026

Uh oh!

Copilot AI Mar 11, 2026

Uh oh!

Copilot AI Mar 11, 2026

Uh oh!

Copilot AI Mar 11, 2026

Uh oh!

Copilot AI Mar 11, 2026

Uh oh!

Copilot AI Mar 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		ConstEvalCounter => "ConstEvalCounter".to_string(),
		Nop => "Nop".to_string(),

	rustc_driver::run_compiler(args_outer, &mut callbacks);
	let _ = rustc_driver::run_compiler(args_outer, &mut callbacks);

		let commit_date = detect_commit_date();
		eprintln!("build.rs: rustc commit-date: {commit_date}");

		1 for line in path.read_text().splitlines()
		if line.strip() and not line.startswith("#")

	r = run(["make", "test-directives"], check=False)
	r = run(["make", "test-directives"], env=env, check=False)

Conversation

cds-amal commented Mar 11, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Mar 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 11, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 11, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants