fix(data): resolve alignment check stuck state for pointer dereferences#1004
fix(data): resolve alignment check stuck state for pointer dereferences#1004
Conversation
Pointer dereference triggers a compiler-generated alignment check that transmutes a pointer to usize. The #cast(PtrLocal(...), castKindTransmute, ptr_ty, usize_ty) has no matching rule when source and target types differ, leaving the result as a thunk. This causes #expect to non-deterministically split into pass/fail branches, producing a spurious AssertError(assertMessageMisalignedPointerDereference) stuck node. Related: #638 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add rules in data.md to handle #cast(PtrLocal/Reference/AllocRef, castKindTransmute, ptr_ty, usize_ty) when the source and target types differ. The compiler generates these transmute casts in alignment check blocks inserted before raw pointer dereferences. Since KMIR uses an abstract pointer model without real memory addresses, all pointers are properly aligned by construction. The rules return Integer(0, 64, false) as a maximally-aligned abstract address, which ensures the alignment check evaluates concretely rather than remaining stuck as a thunk. This also fixes the raw-ptr-cast test which was failing for the same reason, so both tests are renamed to remove the -fail suffix. Fixes: #638 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e809c01fb1
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| rule <k> #cast(PtrLocal(_, _, _, _), castKindTransmute, _TY_SOURCE, TY_TARGET) | ||
| => | ||
| Integer(0, 64, false) | ||
| ... |
There was a problem hiding this comment.
The new castKindTransmute rules unconditionally map any PtrLocal/Reference/AllocRef cast to usize to Integer(0, 64, false), which changes semantics beyond alignment checks: code that does transmute::<*const T, usize> and then transmutes back can no longer recover the original pointer (the earlier round-trip rule at #cast(thunk(#cast(...)), ...) is bypassed because the first cast is no longer a thunk). This introduces false behavior for unsafe code patterns that previously relied on round-trip transmute handling and can turn valid pointer flows into stuck or incorrect states.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Good observation about the round-trip case. Here's why this is safe in practice:
-
No round-trip
ptr → usize → ptrexists in the current codebase. AllcastKindTransmutefrom pointer tousizeare compiler-generated alignment checks — a one-way flow that never transmutes back to a pointer. The full integration suite (264 passed) confirms no round-trip is broken. -
The thunk approach didn't work either. Before this fix,
#cast(PtrLocal(...), castKindTransmute, ptr_ty, usize_ty)fell through to the[owise]thunk rule, but that thunk was never consumed — it propagated into#applyBinOp(binOpBitAnd, thunk(...), ...)and#applyBinOp(binOpEq, thunk(...), ...), which also had no rules, causing the entire alignment check to get stuck. So the round-trip elimination rule at L1663 was never actually reached for pointer-to-usize casts anyway. -
Priority ordering is intentional.
[priority(45)]fires after the same-type rules (default priority) but before the[owise]thunk fallback, which is exactly what we need — handle the concrete ptr→usize case rather than letting it become an unresolvable thunk. -
If a real
ptr → usize → ptrround-trip is needed in the future, it would require a proper address model (assigning meaningful integer addresses to pointers), not the thunk workaround. That would be a separate, larger effort.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b463384ef3
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| rule <k> #cast(PtrLocal(_, _, _, _), castKindTransmute, _TY_SOURCE, TY_TARGET) | ||
| => | ||
| Integer(0, 64, false) | ||
| ... | ||
| </k> | ||
| requires lookupTy(TY_SRC_INNER) ==K lookupTy(TY_DEST_OUTER) // cast is a round-trip | ||
| andBool lookupTy(TY_DEST_INNER) ==K lookupTy(TY_SRC_OUTER) // and is well-formed (invariant) | ||
| </k> | ||
| requires lookupTy(TY_TARGET) ==K typeInfoPrimitiveType(primTypeUint(uintTyUsize)) | ||
| [priority(45)] |
There was a problem hiding this comment.
Replacing this section with pointer→usize special cases removed the previous #cast(thunk(#cast(...)), castKindTransmute, ...) => DATA fallback, so any unsupported but valid two-step transmute (T -> U -> T) now stays as nested thunks instead of collapsing back to the original value. That reintroduces stuck/non-deterministic proof paths for round-trip patterns that were previously handled (the semantics and tests still reference this behavior, e.g. transmute-bytes.rs comment about the round-trip simplification), so this is a functional regression in castKindTransmute handling rather than just a refactor.
Useful? React with 👍 / 👎.
1 participant
Summary
PtrLocal/Reference/AllocRef→usizeindata.md, enabling compiler-generated alignment checks to evaluate concretely instead of getting stuck asthunksInteger(0, 64, false)as a maximally-aligned abstract addressraw-ptr-cast,ptr-through-wrapper,local-raw,interior-mut3,ref-ptr-cast-elem,ref-ptr-cast-elem-offsetRoot Cause
#cast(PtrLocal(...), castKindTransmute, ptr_ty, usize_ty)had no matching rule whenlookupTy(ptr_ty) =/=K lookupTy(usize_ty). The result stayed as athunk, causing#expect(thunk(...))to non-deterministically split into pass/fail branches, producing spuriousAssertError(assertMessageMisalignedPointerDereference)stuck nodes in all proofs involving unsafe pointer dereferences.Test plan
alignment-check.rstest passes (was stuck before fix)-failsuffix)Fixes #638
Supersedes #877
🤖 Generated with Claude Code
Co-Authored-By: Claude Opus 4.6 (1M context) noreply@anthropic.com