Source allocation driver closure: thread.rs:231–283 and rustc interpret/stack.rs:312–321 determine the diagnostic span; PointerMachine executes actual free_alloc_id/address-reuse release-clock operations.

@[reducible, inline]

abbrev Miri.Interpreter.AllocationDriver.ActualFrame : Type

Equations

• Miri.Interpreter.AllocationDriver.ActualFrame = Miri.Interpreter.Frame Miri.Memory.Provenance Miri.Interpreter.LocalLayout Miri.Interpreter.MachineHooks.FrameExtra

structure Miri.Interpreter.AllocationDriver.SpanHooks : Type

• dummy : MIR.SpanRef

  Canonical exported DUMMY_SP, used only for an empty actual stack.

• debugAssertions : Bool

def Miri.Interpreter.AllocationDriver.frameSpan (frame : ActualFrame) : Except StepError MIR.SpanRef

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.AllocationDriver.currentUserRelevantSpan {K User : Type} (h : SpanHooks) : MachineHooks.M K User MIR.SpanRef

Read the source-maintained cache belonging to the actual active thread.

Equations

• Miri.Interpreter.AllocationDriver.currentUserRelevantSpan h = Miri.Interpreter.FrameRelevance.currentUserRelevantSpan h.debugAssertions h.dummy

structure Miri.Interpreter.AllocationDriver.Hooks (K U Payload : Type) : Type

• allocation : AllocationMachine.DeallocationHooks K (PointerMachine.User U) Payload
• pointer : PointerMachine.Hooks K U
• spans : SpanHooks
• addressKind : Memory.MemoryKind K → Except StepError Memory.AllocAddresses.AddressMemoryKind

  Exact machine MemoryKind classification, not allocation-size inference.

def Miri.Interpreter.AllocationDriver.deallocate {K U Payload : Type} [DecidableEq K] (h : Hooks K U Payload) (reuseChoice : Bool) (pointer : Memory.Pointer (Option Memory.Provenance)) (oldLayout : Option (ABI.Size × ABI.Align)) (kind : Memory.MemoryKind K) : PointerMachine.M K U Unit

The source span is computed at its original late stage, after sync checks. No fallback source span is fabricated when a frame location is invalid.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.AllocationDriver.deallocateSource {K U Payload : Type} [DecidableEq K] (choices : ExecutionChoices.Access (PointerMachine.State K U)) (h : Hooks K U Payload) (pointer : Memory.Pointer (Option Memory.Provenance)) (oldLayout : Option (ABI.Size × ABI.Align)) (kind : Memory.MemoryKind K) : PointerMachine.M K U Unit

Production deallocation samples address-reuse choices only after source borrow/race/synchronization checks and inverse-address removal.

Equations

• One or more equations did not get rendered due to their size.