Skip to content

crucible-mir: tolerant parsing of Unsupported instance shims - #1840

Draft
AmeliaRose802 wants to merge 1 commit into
GaloisInc:masterfrom
AmeliaRose802:saw/cm/tolerant-unsupported-shims
Draft

crucible-mir: tolerant parsing of Unsupported instance shims#1840
AmeliaRose802 wants to merge 1 commit into
GaloisInc:masterfrom
AmeliaRose802:saw/cm/tolerant-unsupported-shims

Conversation

@AmeliaRose802

@AmeliaRose802 AmeliaRose802 commented May 26, 2026

Copy link
Copy Markdown

Problem

mir-json emits {"kind": "Unsupported"} for six instance shim variants it does not yet model:

  • ConstructCoroutineInClosureShim
  • ThreadLocalShim
  • FutureDropPollShim
  • FnPtrAddrShim
  • AsyncDropGlueCtorShim
  • AsyncDropGlue

These appear in the intrinsics array of any compiled crate that exercises async Rust, thread-locals, or function-pointer-address taking — even when the user's verified function never touches those code paths.

Today the crucible-mir JSON parser at crucible-mir/src/Mir/JSON.hs:159 fails the entire mir_load_module call with "unsupported instance: Just (Object [\"kind\" .= \"Unsupported\"])" the moment it encounters one of these. This blocks SAW from verifying ordinary Rust code that happens to be in a crate or transitive dependency containing async machinery.

Fix

Add a new IkUnsupported Text constructor to InstanceKind and accept "kind": "Unsupported" in the JSON parser. The optional shim_kind payload carries the original mir-json shim name so any downstream consumer can produce a clear, actionable error if the shim is actually called during translation.

This is a tolerant-parse change: the module loads, the verified function (which doesn't reach the shim) succeeds, and a clear error is deferred to translation time should anyone ever try to compile or invoke the IkUnsupported instance.

Diff

crucible-mir/src/Mir/JSON.hs | 16 ++++++++++++++++
crucible-mir/src/Mir/Mir.hs  |  9 ++++++++-
2 files changed, 24 insertions(+), 1 deletion(-)

No behavior change for modules that don't contain Unsupported instances. Existing tests under crux-mir/test/conc_eval/ are not affected.

Companion PR

  • GaloisInc/mir-json#272 — adds the shim_kind field to mir-json's Unsupported emissions so the deferred error message can name the specific shim. (This crucible-mir PR works fine without the mir-json companion — if shim_kind is absent, it falls back to "unknown".)

End-to-end validation

I ran this fix against the test in intTests/test_mir_async_basic/ (synchronous helper alongside async fn) plus a hand-crafted module containing an injected Unsupported entry, and confirmed:

  1. ✅ Modules containing Unsupported instances load successfully (previously failed at parse time).
  2. mir_verify on a function that doesn't reach the shim succeeds.
  3. ✅ Genuinely unknown kind strings (e.g. "GarbageKind") still produce the original "unsupported instance: …" error — the fix is scoped to "Unsupported" only.

Filed as draft for upstream review.

Adds a new IkUnsupported InstanceKind that the JSON parser accepts
when mir-json emits "kind": "Unsupported" for shim types it does
not yet model (ConstructCoroutineInClosureShim, FutureDropPollShim,
AsyncDropGlueCtorShim, AsyncDropGlue, ThreadLocalShim, FnPtrAddrShim).

Previously mir_load_module would fail to parse the entire
linked-mir.json if ANY function in the module referenced one of
these shims, even when the user only intended to verify other
functions.

After this change, modules containing Unsupported shims load
successfully; the error is deferred to translation/call time if
the shim is actually reached.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant