Source-shaped allocate/copy/deallocate from rustc memory.rs:301–337. No resize shortcut: allocation, initialization mask, access hooks, provenance copy and source-deallocation failures retain all preceding effects.

@[reducible, inline]

abbrev Miri.Interpreter.ReallocationDriver.User (U : Type) : Type

Equations

• Miri.Interpreter.ReallocationDriver.User = Miri.Interpreter.PointerMachine.User

@[reducible, inline]

abbrev Miri.Interpreter.ReallocationDriver.M (K U A : Type) : Type

Equations

• Miri.Interpreter.ReallocationDriver.M K U A = Miri.Interpreter.PointerMachine.M K U A

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

• driver : AllocationDriver.Hooks K U Payload
• access : PlaceMachine.AccessConfig K (User U)
• allocation : PlaceMachine.AllocationConfig K (User U)
• weakMemory : Bool
• globalKind : Option (Memory.MemoryKind K)

structure Miri.Interpreter.ReallocationDriver.CreationHooks (K U Payload : Type) : Type

Allocation creation requires shared extras and storage configuration, not a pointer/deallocation interpreter.

• extras : MemoryExtras.Hooks K (User U) Payload
• allocation : PlaceMachine.AllocationConfig K (User U)
• weakMemory : Bool
• globalKind : Option (Memory.MemoryKind K)

def Miri.Interpreter.ReallocationDriver.Hooks.creation {K U Payload : Type} (h : Hooks K U Payload) : CreationHooks K U Payload

Equations

• h.creation = { extras := h.driver.allocation.extras, allocation := h.allocation, weakMemory := h.weakMemory, globalKind := h.globalKind }

def Miri.Interpreter.ReallocationDriver.allocate {K U Payload : Type} [DecidableEq K] (h : Hooks K U Payload) (size : ABI.Size) (align : ABI.Align) (kind : Memory.MemoryKind K) (init : Memory.AllocInit) (choice : Memory.AllocAddresses.AddressRandomChoices) : M K U (Memory.Pointer Memory.Provenance)

Explicit-choice adapter retained for operation-level fixtures.

Equations

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

def Miri.Interpreter.ReallocationDriver.allocateSource {K U Payload : Type} [DecidableEq K] (h : Hooks K U Payload) (size : ABI.Size) (align : ABI.Align) (kind : Memory.MemoryKind K) (init : Memory.AllocInit) : M K U (Memory.Pointer Memory.Provenance)

Production allocation samples choices in the canonical root-address callback after insertion, never when constructing a foreign-call dictionary.

Equations

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

def Miri.Interpreter.ReallocationDriver.allocateSourceFrom {K U Payload : Type} [DecidableEq K] (h : CreationHooks K U Payload) (size : ABI.Size) (align : ABI.Align) (kind : Memory.MemoryKind K) (init : Memory.AllocInit) : M K U (Memory.Pointer Memory.Provenance)

Source allocation without unused pointer/deallocation capabilities.

Equations

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

def Miri.Interpreter.ReallocationDriver.allocateConfigured {K U : Type} [DecidableEq K] (config : PlaceMachine.AllocationConfig K (User U)) (size : ABI.Size) (align : ABI.Align) (kind : Memory.MemoryKind K) (init : Memory.AllocInit) : M K U (Memory.Pointer Memory.Provenance)

Use an already source-assembled allocation config. This is for startup allocations whose config already owns extras initialization and root-address choice; wrapping it in CreationHooks would initialize extras twice.

Equations

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

def Miri.Interpreter.ReallocationDriver.reallocate {K U Payload : Type} [DecidableEq K] (h : Hooks K U Payload) (pointer : Memory.Pointer (Option Memory.Provenance)) (oldLayout : Option (ABI.Size × ABI.Align)) (newSize : ABI.Size) (newAlign : ABI.Align) (kind : Memory.MemoryKind K) (initGrowth : Memory.AllocInit) (allocationChoice : Memory.AllocAddresses.AddressRandomChoices) (reuseChoice : Bool) : M K U (Memory.Pointer Memory.Provenance)

Equations

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

def Miri.Interpreter.ReallocationDriver.reallocateSource {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)) (newSize : ABI.Size) (newAlign : ABI.Align) (kind : Memory.MemoryKind K) (initGrowth : Memory.AllocInit) : M K U (Memory.Pointer Memory.Provenance)

Persistent draws occur at actual allocation and late deallocation events.

Equations

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

def Miri.Interpreter.ReallocationDriver.reallocateFrom {K U Payload : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K (User U)) (h : CreationHooks K U Payload) (arithmetic : Memory.PointerArithmetic) (destroy : Memory.Pointer (Option Memory.Provenance) → Option (ABI.Size × ABI.Align) → Memory.MemoryKind K → M K U Unit) (pointer : Memory.Pointer (Option Memory.Provenance)) (oldLayout : Option (ABI.Size × ABI.Align)) (newSize : ABI.Size) (newAlign : ABI.Align) (kind : Memory.MemoryKind K) (initGrowth : Memory.AllocInit) : M K U (Memory.Pointer Memory.Provenance)

Source reallocation with only creation/access and the actual late source-deallocation action. It shares the ordering of both legacy adapters.

Equations

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

def Miri.Interpreter.ReallocationDriver.reallocateConfiguredFrom {K U Payload : Type} [DecidableEq K] (access : PlaceMachine.AccessConfig K (User U)) (extras : MemoryExtras.Hooks K (User U) Payload) (arithmetic : Memory.PointerArithmetic) (config : PlaceMachine.AllocationConfig K (User U)) (destroy : Memory.Pointer (Option Memory.Provenance) → Option (ABI.Size × ABI.Align) → Memory.MemoryKind K → M K U Unit) (pointer : Memory.Pointer (Option Memory.Provenance)) (oldLayout : Option (ABI.Size × ABI.Align)) (newSize : ABI.Size) (newAlign : ABI.Align) (kind : Memory.MemoryKind K) (initGrowth : Memory.AllocInit) : M K U (Memory.Pointer Memory.Provenance)

Source reallocation when the allocation configuration already owns the canonical extras initialization and root-address choice. This mirrors reallocateFrom while avoiding a second MemoryExtras.bindAllocation pass. The new allocation, provenance-aware copy, and late destroy retain the source ordering and partial effects.

Equations

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