Single-pass body analysis with AllocMap coherence checks (#121)

## What's this about?

So, #120 fixed the immediate alloc-id mismatch by carrying collected
items forward instead of re-fetching them. That was the right call. But
it left the underlying structure intact: three separate phases (mk_item,
collect_unevaluated_constant_items, collect_interned_values), each with
full access to `TyCtxt`, each free to call `inst.body()` or any other
side-effecting rustc query whenever it felt like it. Nothing in the
types prevented that, and the bug was a direct consequence: one phase
called `inst.body()` a second time, rustc minted fresh AllocIds, and
suddenly the alloc map had ids that didn't correspond to anything in the
stored bodies.

The question is: how do we make that class of bug structurally
impossible, rather than just fixed for the one case we caught?

The full decision record is in
[`ADR-002`](https://github.com/cds-rs/stable-mir-json/blob/dc/declarative-spike/docs/adr/002-declarative-pipeline-with-allocmap-coherence.md).

### The restructuring

The fix is to split the pipeline into phases with type signatures that
enforce the boundary:

```rust
collect_and_analyze_items(HashMap<String, Item>)
  -> (CollectedCrate, DerivedInfo)

assemble_smir(CollectedCrate, DerivedInfo) -> SmirJson
```

`CollectedCrate` holds items and unevaluated consts (the output of
talking to rustc). `DerivedInfo` holds calls, allocs, types, and spans
(the output of walking bodies). `assemble_smir` takes both by value and
does pure data transformation; it structurally cannot call `inst.body()`
because it has no `MonoItem` or `Instance` to call it on. That's the
whole point: if you can't reach the query, you can't accidentally call
it.

The two body-walking visitors (`InternedValueCollector` and
`UnevaluatedConstCollector`) are merged into a single `BodyAnalyzer`
that walks each body exactly once. The fixpoint loop for transitive
unevaluated constant discovery is integrated: when `BodyAnalyzer` finds
an unevaluated const, it records it; the outer loop creates the new
`Item` (the one place `inst.body()` is called) and enqueues it.

### But what about catching regressions?

Turns out the existing integration tests normalize away `alloc_id`s (via
the jq filter), so they literally cannot catch this class of bug. The
golden files don't contain alloc ids at all; you could scramble every id
in the output and the tests would still pass.

`AllocMap` replaces the bare `HashMap<AllocId, ...>` with a newtype
that, under `#[cfg(debug_assertions)]`, tracks every insertion and flags
duplicates. After the collect/analyze phase completes,
`verify_coherence` walks every stored `Item` body with an
`AllocIdCollector` visitor and asserts that each referenced `AllocId`
exists in the map. This catches both "walked a stale body" (missing ids)
and "walked the same body twice" (duplicate insertions) at dev time;
zero cost in release builds.

### Other things that fell out of this

- Static items now store their body in `MonoItemKind::MonoItemStatic`
(collected once in `mk_item`), so the analysis phase never goes back to
rustc for static bodies
- `get_item_details` takes the pre-collected body as a parameter instead
of calling `inst.body()` independently
- The `items_clone` full HashMap clone is replaced by a `HashSet` of
original item names (which is all the static fixup actually needed)
- [we uncovered and fixed a very old
bug](#121 (comment))

### What's deleted

`InternedValueCollector`, `UnevaluatedConstCollector`,
`collect_interned_values`, `collect_unevaluated_constant_items`, the
`InternedValues` type alias, and `items_clone`. Good riddance.

### Downstream impact

The tighter allocs representation has already shown positive downstream
effects in KMIR: the proof engine can now decode allocations inline
(resolving to concrete values like `StringVal("123")`) instead of
deferring them as opaque thunks. @dkcumming 's `offset-u8` test went
from thunking through `#decodeConstant(constantKindAllo...)` to directly
producing `toAlloc(allocId(0)), StringVal("123")`. The test's expected
output needed updating, but the new failure mode is semantically
grounded in actual data rather than deferred interpretation.

### Test plan

- [x] `cargo build` compiles
- [x] `cargo clippy` clean
- [x] `cargo fmt` clean
- [x] `make integration-test` passes (all 28 tests, identical output)
- [x] KMIR downstream: `test_prove_rs[offset-u8-fail]` expected output
updated

Author: cds-amal

CHANGELOG.md

@@ -0,0 +1,80 @@
+# Changelog
+
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
+
+Note: this changelog was introduced at 0.2.0. The 0.1.0 section is a
+retroactive best-effort summary; earlier changes were not formally tracked.
+
+## [0.2.0] - 2026-02-21
+
+### Added
+- D2 and Mermaid graph renderers alongside existing DOT, with index-first architecture for richer allocation/type lookup in rendered output ([#111])
+- `--d2` flag for D2 diagram output
+- `MachineInfo` in JSON output: pointer width, endianness ([#80])
+- `Span` information in JSON output ([#74])
+- Type visitor collecting full type metadata: ADT fields, discriminants, layouts ([#68], [#69], [#82], [#93], [#94])
+- `TyKind` in `GlobalAlloc` entries ([#84])
+- Extract discriminant information for enums ([#62])
+- ADT def and field type metadata for structs and enums ([#64], [#82], [#105])
+- UI test infrastructure ([#66])
+- `cargo_stable_mir_json` helper binary for cargo integration ([#47])
+- Nix derivation for reproducible builds ([#96])
+- macOS support ([#97])
+
+### Changed
+- Restructured `printer.rs` into a declarative 3-phase pipeline: `collect_items` -> `collect_and_analyze_items` -> `assemble_smir`, with `CollectedCrate`/`DerivedInfo` interface types enforcing the boundary between collection and assembly
+- Added `AllocMap` with debug-mode coherence checking (`verify_coherence`): asserts that every `AllocId` in stored bodies exists in the alloc map and that no body is walked twice; zero cost in release builds
+- Removed dead static-item fixup from `assemble_smir` (violated the phase boundary, misclassified statics as functions; never triggered in integration tests)
+- Switched from compiler build to `rustup`-managed toolchain ([#33])
+- Removed forked rust dependency ([#19])
+
+### Fixed
+- Fixed early `return` in `BodyAnalyzer::visit_terminator` that skipped `super_terminator()`, causing alloc/type/span collection to miss everything inside `Call` terminators with non-`ZeroSized` function operands (const-evaluated function pointers); bug present since [`aff2dd0`](https://github.com/runtimeverification/stable-mir-json/commit/aff2dd0)
+- Avoided duplicate `inst.body()` calls that were reallocating `AllocId`s ([#120])
+- Prevented svg/png generation when `dot` is unavailable ([#117])
+- Removed unreachable early return in D2 legend rendering ([#118])
+- Included ZeroSized FnDef consts in functions map ([#112])
+- Support `GlobalAlloc::Function` with non-fn-ptr type ([#102])
+- Emitted correct `Alloc` ty for each allocation ([#100])
+- Normalized field types before emitting them ([#95])
+- Fixed monomorphisation bug for FnDef and ClosureDef ([#53])
+
+[#19]: https://github.com/runtimeverification/stable-mir-json/pull/19
+[#33]: https://github.com/runtimeverification/stable-mir-json/pull/33
+[#47]: https://github.com/runtimeverification/stable-mir-json/pull/47
+[#53]: https://github.com/runtimeverification/stable-mir-json/pull/53
+[#62]: https://github.com/runtimeverification/stable-mir-json/pull/62
+[#64]: https://github.com/runtimeverification/stable-mir-json/pull/64
+[#66]: https://github.com/runtimeverification/stable-mir-json/pull/66
+[#68]: https://github.com/runtimeverification/stable-mir-json/pull/68
+[#69]: https://github.com/runtimeverification/stable-mir-json/pull/69
+[#74]: https://github.com/runtimeverification/stable-mir-json/pull/74
+[#80]: https://github.com/runtimeverification/stable-mir-json/pull/80
+[#82]: https://github.com/runtimeverification/stable-mir-json/pull/82
+[#84]: https://github.com/runtimeverification/stable-mir-json/pull/84
+[#93]: https://github.com/runtimeverification/stable-mir-json/pull/93
+[#94]: https://github.com/runtimeverification/stable-mir-json/pull/94
+[#95]: https://github.com/runtimeverification/stable-mir-json/pull/95
+[#96]: https://github.com/runtimeverification/stable-mir-json/pull/96
+[#97]: https://github.com/runtimeverification/stable-mir-json/pull/97
+[#100]: https://github.com/runtimeverification/stable-mir-json/pull/100
+[#102]: https://github.com/runtimeverification/stable-mir-json/pull/102
+[#105]: https://github.com/runtimeverification/stable-mir-json/pull/105
+[#111]: https://github.com/runtimeverification/stable-mir-json/pull/111
+[#112]: https://github.com/runtimeverification/stable-mir-json/pull/112
+[#117]: https://github.com/runtimeverification/stable-mir-json/pull/117
+[#118]: https://github.com/runtimeverification/stable-mir-json/pull/118
+[#120]: https://github.com/runtimeverification/stable-mir-json/pull/120
+
+## [0.1.0] - 2024-11-29
+
+Initial release.
+
+### Added
+- Compiler driver hooking into rustc's `after_analysis` phase
+- JSON serialization of Stable MIR: monomorphized items, allocations, interned values
+- `--json` flag (default) for JSON output, `--dot` flag for graphviz DOT output
+- Function link map tracking monomorphized function symbols
+- Integration test harness with `.smir.json.expected` golden files and jq normalization

Cargo.lock

@@ -1,6 +1,6 @@
 [package]
 name = "stable_mir_json"
-version = "0.1.0"
+version = "0.2.0"
 edition = "2021"
 default-run = "stable_mir_json"
 
@@ -20,4 +20,4 @@ debug_log = []
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.
-rustc_private=true
+rustc_private=true

Cargo.toml

@@ -0,0 +1,54 @@
+# ADR-002: Declarative collect/analyze/assemble pipeline with AllocMap coherence
+
+**Status:** Accepted
+**Date:** 2026-02-21
+
+## Context
+
+The original `printer.rs` pipeline had three separate phases: `mk_item`, `collect_unevaluated_constant_items`, and `collect_interned_values`. Each phase had full access to `TyCtxt` and was free to call `inst.body()` or any other side-effecting rustc query whenever it felt like it. Nothing in the types prevented that.
+
+This caused a real bug (#120): one phase called `inst.body()` a second time, rustc minted fresh AllocIds (because that's what rustc does), and suddenly the alloc map had ids that didn't correspond to anything in the stored bodies. The downstream effect was that KMIR's proof engine couldn't decode allocations properly; they came out as opaque thunks instead of concrete values.
+
+The fix in #120 was correct (carry collected items forward instead of re-fetching), but it left the underlying structure intact. The question was: how do we make that class of bug structurally impossible rather than just fixed for the one case we caught?
+
+## Decision
+
+Split the pipeline into phases whose type signatures enforce the boundary:
+
+```rust
+collect_and_analyze_items(HashMap<String, Item>)
+  -> (CollectedCrate, DerivedInfo)
+
+assemble_smir(CollectedCrate, DerivedInfo) -> SmirJson
+```
+
+`CollectedCrate` holds items and unevaluated consts (the output of talking to rustc). `DerivedInfo` holds calls, allocs, types, and spans (the output of walking bodies). `assemble_smir` takes both by value and does pure data transformation; it structurally cannot call `inst.body()` because it has no `MonoItem` or `Instance` to call it on. If you can't reach the query, you can't accidentally call it.
+
+The two body-walking visitors (`InternedValueCollector` and `UnevaluatedConstCollector`) are merged into a single `BodyAnalyzer` that walks each body exactly once. The fixpoint loop for transitive unevaluated constant discovery is integrated: when `BodyAnalyzer` finds an unevaluated const, it records it; the outer loop creates the new `Item` (the one place `inst.body()` is called) and enqueues it.
+
+### AllocMap coherence verification
+
+The existing integration tests normalize away `alloc_id`s (via the jq filter), so they literally cannot catch this class of bug. The golden files don't contain alloc ids at all; you could scramble every id and the tests would still pass.
+
+`AllocMap` replaces the bare `HashMap<AllocId, ...>` with a newtype that, under `#[cfg(debug_assertions)]`, tracks every insertion and flags duplicates. After the collect/analyze phase completes, `verify_coherence` walks every stored `Item` body with an `AllocIdCollector` visitor and asserts that each referenced `AllocId` exists in the map. This catches both "walked a stale body" (missing ids) and "walked the same body twice" (duplicate insertions) at dev time; zero cost in release builds.
+
+## Consequences
+
+**What's enforced by types:**
+- `assemble_smir` cannot call `inst.body()` because it receives `CollectedCrate` and `DerivedInfo`, neither of which contains `Instance` or `MonoItem` handles
+- Each body is walked exactly once in `collect_and_analyze_items`; the single `BodyAnalyzer` pass replaces two separate visitor passes
+
+**What's enforced at dev-time (debug builds only):**
+- Duplicate `AllocId` insertions are flagged (indicates a body was walked more than once)
+- Missing `AllocId`s in the map (referenced in stored bodies but not collected) are flagged (indicates the analysis walked a different body than what's stored)
+
+**What got deleted:**
+`InternedValueCollector`, `UnevaluatedConstCollector`, `collect_interned_values`, `collect_unevaluated_constant_items`, the `InternedValues` type alias, and `items_clone`. The `items_clone` is particularly worth noting: it was a full `HashMap` clone that existed only so the static fixup pass could check "was this item in the original collection?" That's now a `HashSet<String>` of original item names.
+
+**Other things that fell out of this:**
+- Static items now store their body in `MonoItemKind::MonoItemStatic` (collected once in `mk_item`), so the analysis phase never goes back to rustc for static bodies
+- `get_item_details` takes the pre-collected body as a parameter instead of calling `inst.body()` independently
+- The `Item` type gains `body_and_locals()` and `warn_missing_body()` helpers that centralize the body-access pattern
+
+**Downstream impact:**
+The tighter allocs representation has already shown positive effects in KMIR: the proof engine can now decode allocations inline (resolving to concrete values like `StringVal("123")`) instead of deferring them as opaque thunks.

docs/adr/002-declarative-pipeline-with-allocmap-coherence.md

@@ -295,11 +295,7 @@ impl SmirJson<'_> {
                         let mut n = graph.node_named(short_name(&asm));
                         n.set_label(&asm.lines().collect::<String>()[..]);
                     }
-                    MonoItemKind::MonoItemStatic {
-                        name,
-                        id: _,
-                        allocation: _,
-                    } => {
+                    MonoItemKind::MonoItemStatic { name, .. } => {
                         let mut n = graph.node_named(short_name(&name));
                         n.set_label(&name[..]);
                     }