Skip to content

feat(rt): stabilize pointer cast address allocation#1003

Draft
Stevengre wants to merge 4 commits intomasterfrom
jh/address-alloc-model
Draft

feat(rt): stabilize pointer cast address allocation#1003
Stevengre wants to merge 4 commits intomasterfrom
jh/address-alloc-model

Conversation

@Stevengre
Copy link
Copy Markdown
Contributor

@Stevengre Stevengre commented Mar 26, 2026

Summary

Refactors the pointer-to-integer work in #1002 into a reviewable red/green history and fixes the remaining symbolic regressions in the address model.

This PR now does four things:

  • adds a focused cross-frame reproducer showing what master cannot prove today
  • introduces a stable stack allocation identity for pointer casts via frameId
  • fixes pointer-to-integer address computation to recover layout from the actual stack slot instead of relying only on the cast source pointee type
  • promotes the pointer-cast regressions that are now fully proved from *-fail cases into normal passing prove tests

Implementation highlights:

  • adds stable frame ids to the runtime configuration and stack frames
  • keys <addressMap> / <exposedSet> by stable allocation identity instead of relative stack depth
  • keeps lazy address allocation for pointer-to-integer casts and PointerExposeAddress
  • recovers byte step and allocation layout from the referenced stack slot, which fixes ZST-wrapper and element-offset alignment cases

Commit Guide

  1. test(prove): add cross-frame pointer cast reproducer
    • adds a red proof and expected output demonstrating the missing behavior on master
  2. feat(rt): stabilize stack allocation identity for ptr casts
    • introduces stable frame ids and uses them for address allocation identity
  3. fix(rt): recover pointer cast layout from stack slots
    • fixes byte-step / allocation-layout recovery for pointer-to-integer casts
  4. test(prove): promote resolved pointer cast regressions
    • restores the original PR coverage as passing prove tests and removes obsolete *-fail expectations

Verification

Local validation run on the rewritten branch:

uv --directory kmir run pytest src/tests/integration/test_integration.py -v --timeout=600 -k 'alignment-check or interior-mut3 or local-raw or ptr-through-wrapper or ptr-transmute-nonzero or ptr-transmute-two-locals or ptr_offset or raw-ptr-cast or ref-ptr-cast-elem-offset or ref-ptr-cast-elem or ptr-cast-cross-frame-eq'

Result:

  • 11 passed, 266 deselected

Additional proof checks used while validating the migrated regressions:

  • raw-ptr-cast-fail, ptr-through-wrapper-fail, local-raw-fail, ref-ptr-cast-elem-offset-fail, ref-ptr-cast-elem-fail, and interior-mut3-fail now each report ProofStatus.PASSED with stuck: 0 and failing: 0, which is why they are promoted to normal pass tests in the final commit

GitHub Actions on the rewritten history are currently in progress and should be treated as the remaining readiness gate.

Related

@Stevengre Stevengre force-pushed the jh/address-alloc-model branch 2 times, most recently from ba94541 to 3e7d29b Compare April 2, 2026 06:48
@Stevengre Stevengre changed the title feat(rt): add address allocation model for pointer-to-integer semantics feat(rt): stabilize pointer cast address allocation Apr 2, 2026
@Stevengre Stevengre force-pushed the jh/address-alloc-model branch from 3e7d29b to 5c19ae0 Compare April 2, 2026 14:08
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.

feat: add address allocation model for pointer-to-integer semantics Extend pointer emulation to pass alignment check

1 participant