fix(printer): record closure Ty in type table after instance traversal#129
Merged
automergerpr-permission-manager[bot] merged 12 commits intomasterfrom Mar 2, 2026
Merged
Conversation
After resolving a closure instance, the visitor early-returned without inserting the closure's Ty into the types collection. This caused downstream consumers (kmir) to miss closure type metadata, leading to thunked zero-sized constants that blocked execution. Now the closure's Ty, kind, and layout shape are recorded in the type table after successful instance traversal.
Stevengre
changed the title
Stevengre
changed the title
Collaborator
|
If there isn't a pressing need Is it possible for this to merge after #122? |
Collaborator
dkcumming
pushed a commit
that referenced
this pull request
Mar 3, 2026
### Summary - In `src/printer.rs`, `collect_alloc` no longer panics on non-`builtin_deref` `GlobalAlloc::Static` / `GlobalAlloc::VTable` paths. - It now attempts `get_prov_ty(ty, offset)` first, and falls back to opaque `Ty::to_val(0)` when recovery is not possible. - Existing behavior for direct `builtin_deref` pointer/reference paths is unchanged. - Added a regression test using the existing integration golden framework: - `tests/integration/programs/static-vtable-nonbuiltin-deref.rs` - `tests/integration/programs/static-vtable-nonbuiltin-deref.smir.json.expected` - minimal normalization update in `tests/integration/normalise-filter.jq` (strip unstable `def_id`). ### Context This PR was split from [stable-mir-json#129](#129) so `#129` can stay focused on closure type-table metadata. The failure mode here was assert-based panic in pre-fix code when a provenance edge reached `Static`/`VTable` through a non-`builtin_deref` container type. ### Testing Automated (local): - RED (pre-fix baseline on `origin/master`): - `make integration-test TESTS=tests/integration/programs/static-vtable-nonbuiltin-deref.rs` - Result: fails with `Allocated pointer is not a built-in pointer type` panic at `src/printer.rs:789`. - GREEN (this branch): - `make integration-test TESTS=tests/integration/programs/static-vtable-nonbuiltin-deref.rs` ✅ - `make integration-test TESTS=tests/integration/programs/assert_eq.rs` ✅ - `cargo +nightly-2024-11-29 fmt --check` ✅ - `cargo +nightly-2024-11-29 clippy -- -Dwarnings` ✅ GitHub checks: - New run for head `11180ce` is in progress.
dkcumming
added a commit
to runtimeverification/mir-semantics
that referenced
this pull request
Mar 3, 2026
- [stable-mir-json PR 122](https://github.com/runtimeverification/stable-mir-json/pull/122/changes#diff-f3fb88e143d9d90b06c9086e1c660a3e28674c1c1cebf1870de06d73156e3d54R413-R416) Added `Dyn` which needed corresponding K and python productions added to AST - [stable-mir-json PR 129](runtimeverification/stable-mir-json#129) or [131](runtimeverification/stable-mir-json#131) changes closures which do not have corresponding K updates in this PR, proofs `and_then_closure` and `closure_acces_struct` are regressed to failing for now with semantics for correct usage expected to come after merging --------- Co-authored-by: devops <[email protected]> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: Daniel Cumming <[email protected]> Co-authored-by: dkcumming <[email protected]>
automergerpr-permission-manager bot
pushed a commit
to runtimeverification/mir-semantics
that referenced
this pull request
Mar 4, 2026
#956 added handles `FunType` for closures instead of `VoidType` for that come from [stable mir json 129](runtimeverification/stable-mir-json#129) for `setupCalleeClosure2`. This PR adds the same thing to `setupCalleeClosure`. (Fixes regressed proofs for P-Token) - Added explicit `FnOnce` test `closure_fnonce_tuple_arg.rs` - Fixed `and_then_closure.rs`
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
TyCollector::visit_ty(src/printer.rs), after successful closure instance traversal, record closureTymetadata intypes.tests/integration/programs/*.smir.json.expected) to match emitted closureFunTypemetadata.Makefileintegration path asTESTDIR=tests/integration/programsto keep closure fixture output paths stable.Context
In the closure arm of
TyCollector::visit_ty, the code resolved and visited the closure instance but returned without inserting the closureTyintotypes. Other type families were inserted; closures were the exception.This made downstream closure type lookup incomplete (notably for kmir proof paths that consume exported type metadata). Recording closure
Tycloses that gap.Related split: static/vtable alloc fallback changes were moved out to stable-mir-json#131 so this PR stays focused on closure metadata.
Dependency context: this PR is depended on by mir-semantics#957.