fix(printer): recover non-builtin static/vtable alloc typing

[Stevengre]

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 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.

[cds-amal]

Hey @Stevengre , the split, made this easy to review.

So I went digging into this a bit, and here's what I found: the assert! calls that used to live in the Static and VTable arms (the ones that would panic on non-builtin-deref types) were actually already removed in #126 as part of the broader provenance resolution rework. That means the panic this was originally guarding against is already gone on master.

What this PR is doing now is something subtly different: it's a correctness improvement. On master, those arms just unconditionally record the outer ty, which could be a container type rather than the actual pointee when builtin_deref returns None. This PR recovers the real pointee via get_prov_ty (or falls back to an opaque Ty::to_val(0) when recovery fails). That's a strictly better policy than: record whatever we were handed and hope for the best.

That said: I wasn't able to actually trigger the non-builtin-deref path. I tried the existing integration suite (none of the 28 programs exercise GlobalAlloc::Static or GlobalAlloc::VTable in a way that reaches this branch), and I wrote a couple of hand-rolled programs with statics, trait objects, Box<dyn Trait>, nested structs with &'static fields, etc. Everything came through with builtin_deref returning Some, so the recovery logic never fired.

A natural question: do you have a concrete example (or know of a UI test) where this path actually gets hit? I'd feel a lot better landing this with a test that validates the fix. Right now we're adding recovery logic for a case we can't reproduce, which makes it hard to verify it's doing the right thing.

Thanks in advance!

[Stevengre]

Additional note using the same input case tests/integration/programs/static-vtable-nonbuiltin-deref.rs (local A/B where only the #131 Static/VTable fallback logic is toggled):

What this change does in this example (diff-based)

Comparing the ty associated with the Static / VTable allocs shows:

--- nofix
+++ fix
@@
- "ty_def": {
-   "ArrayType": {
-     "elem_type": 33,
-     "layout": { "abi": { "Aggregate": { "sized": true } }, ... }
-   }
- },
- "ty_id": 34
+ "ty_def": {
+   "DynType": {
+     "name": "dyn std::fmt::Debug",
+     "layout": { "abi": { "Aggregate": { "sized": false } }, ... }
+   }
+ },
+ "ty_id": 46

So:

• Before (nofix): Static/VTable allocs keep the outer container type (ArrayType).
• After (fix): Static/VTable allocs use the recovered pointee type (DynType(dyn Debug)).

This is exactly the collect_alloc path where GlobalAlloc::Static / GlobalAlloc::VTable on non-builtin-deref now attempts get_prov_ty(...) first.

Why this is not directly visible in expected snapshots

The integration normalizer removes alloc type fields:

# tests/integration/normalise-filter.jq
.allocs = ( .allocs | map(del(.alloc_id)) | map(del(.ty)) )

So expected files only assert alloc kind presence (Static / VTable) and not the internal alloc.ty precision. The behavior change is present in raw .smir.json, but intentionally normalized out from snapshot diffs.

[Stevengre]

@cds-amal Thanks for asking for an example! Above gives the example!

[cds-amal]

Hey @Stevengre, it's taking me some time to review this, and I think the merge commits are a big part of why: they make it hard to tell which changes are yours versus what came in from upstream. I wanted to share a quick workflow note while my notes are fresh; I'll follow up with a code review shortly.

Looking at the original history on codex/static-vtable-alloc-fallback, there were 12 commits including two merge commits where you pulled origin/master into the branch (likely via GitHub's "Update branch" button or git merge origin/master). Those merges pulled in upstream PRs (#122, #129) as ancestors of your branch, and then you needed a follow-up commit (9d8015c) to fix up the test expectations after the merge.

Here's the original branch graph:

⌽ a85eb0e fix(printer): avoid panic on non-builtin static/vtable alloc pointers
⌽ 7282617 docs(printer): clarify static/vtable fallback typing policy
⌽ 8d73970 test(integration): cover static and vtable fallback behavior
⌽ 7621532 fix(tests): reuse SMIR command in fallback check
⌽ 93b40f1 docs(comments): shorten fallback annotations
⌽ 23cb8fb test(integration): use golden case for static/vtable fallback
⌽ f57e1f5 chore(printer): revert unrelated function comment edit
⌽ f1b95e4 docs(test): annotate expected impact for fallback case
⌽ 11180ce docs(test): inline concise comments and remove extra notes file
⌽ 7c8aa5c (merge commit) merge(printer): resolve #131 against latest master
⌽ f54e442 (merge commit) Merge remote-tracking branch 'origin/master' into codex/...
⌽ codex/static-vtable-alloc-fallback  test(integration): refresh static-vtable expected after master merge

That's 12 commits (including 2 merge commits and a post-merge fixup) for a change that touches 4 files. When I open this for review, git log master..HEAD shows me all 12, and it's hard to tell what's your work versus what came in from master. GitHub's PR diff tab handles this okay (it shows the net diff against the base), but anyone reviewing commit-by-commit (which is often the most useful way to review) has to mentally separate your changes from the merge noise.

After rebasing onto master and squashing the iterative work:

⌽ master fix(printer): record closure Ty in type table after instance traversal (#129)
⌽ cacf4d4 fix(printer): avoid panic on non-builtin static/vtable alloc pointers
⌽ rebase/codex/svta-fb  test(integration): cover static and vtable fallback behavior

Two commits, linear, each doing one thing.

The fix is to rebase instead of merge when you need to pick up upstream changes:

git fetch origin
git rebase origin/master

This replays your commits on top of the latest master, so your branch stays a clean, linear sequence of just your work. If there are conflicts, you resolve them inline during the rebase (same conflict resolution, just applied differently), and the result is a branch where every commit is yours.

One thing that makes rebasing less painful: enable git-rerere ("reuse recorded resolution"). It remembers how you resolved conflicts, so if you rebase again later and hit the same conflict, git resolves it automatically:

git config --global rerere.enabled true
git config --global rerere.autoupdate true

The first setting tells git to record every conflict resolution you make. The second automatically stages the re-applied resolution (without it, rerere replays the resolution but leaves the file unstaged, so you have to git add it manually before continuing the rebase).

One caveat: rebasing rewrites commit hashes, so if you've already pushed the branch remotely, you'll need git push --force-with-lease afterward. That's fine for feature branches (it's your branch), but worth being aware of.

[Stevengre]

Hi @cds-amal ! Thank you for sharing these things. I'll use rebase to make it easy to review.

[dkcumming]

Nice! Love the teamwork @Stevengre @cds-amal - I think we can do a bit of a common functionality refactor by the look of things but let's get this in so it unblocks that aspect of your SPL proofs Jianhong