Connected machine deallocation: rustc memory.rs deallocate_ptr and Miri machine.rs:1790–1838. The live allocation is removed before machine checks, including failures; clock, tree and synchronization failures retain effects.

structure Miri.Interpreter.AllocationMachine.DeallocationHooks (K User Payload : Type) : Type

• extras : MemoryExtras.Hooks K User Payload
• resolvePointer : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree K → PlaceMachine.AccessState K User → Memory.Pointer (Option Memory.Provenance) → Int → Memory.PointerResolutionResult Memory.Provenance TreeBorrows.BorrowTree K (PlaceMachine.AccessState K User) Memory.ProvenanceExtra
• diagnostic : Memory.AllocId → PlaceMachine.MachineM K User Unit
• currentSpan : PlaceMachine.MachineM K User MIR.SpanRef

  Source current_user_relevant_span; no default fabricated span.

• freeAllocId : Memory.AllocId → ABI.Size → ABI.Align → Memory.MemoryKind K → PlaceMachine.MachineM K User Unit

  Source address-reuse/free_alloc_id including canonical address map.

• retainDetached : Memory.Allocation Memory.Provenance TreeBorrows.BorrowTree → PlaceMachine.Machine K User → PlaceMachine.Machine K User

  Preserve a failed detached allocation's mutated tree for diagnostics/GC.

• nativeDrop : Option (Memory.Allocation Memory.Provenance TreeBorrows.BorrowTree → MachineHooks.M K User Unit)
• error : Memory.MemoryLifecycleError → StepError

def Miri.Interpreter.AllocationMachine.deallocationError : Memory.MemoryLifecycleError → StepError

Pinned memory.rs::deallocate_ptr failures. Machine-hook typed failures are recovered from AccessState.pendingError before this classification.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.AllocationMachine.deallocationError x✝ = Miri.Interpreter.StepError.invalidProgram (toString "unexpected deallocation source failure: " ++ toString (reprStr x✝))

def Miri.Interpreter.AllocationMachine.deallocate {K User Payload : Type} [DecidableEq K] (h : DeallocationHooks K User Payload) (pointer : Memory.Pointer (Option Memory.Provenance)) (oldLayout : Option (ABI.Size × ABI.Align)) (kind : Memory.MemoryKind K) : MachineHooks.M K User Unit

Actual MemoryLifecycle owns kind/layout checks and removed/dead maps; the callback owns ordered diagnostic/race/TB/sync/address-release machine effects.

Equations

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