Compiler global images are decoded into actual Allocation records only through checked memory APIs. Export IDs never become runtime AllocIds; every relocation is remapped through MemoryState.importedGlobalIds. Import is not runtime access: getGlobalAlloc retains lazy initializer and machine-hook order. Source: rustc_middle/mir/interpret/{allocation,mod}.rs and interpret/memory.rs.

@[reducible, inline]

abbrev Miri.Input.AllocationImage.Result (α : Type u_1) : Type u_1

Equations

• Miri.Input.AllocationImage.Result = Except String

def Miri.Input.AllocationImage.runtimeId {P E K : Type} (memory : Memory.MemoryState P E K) (exportId : AllocationId) : Result Memory.AllocId

Resolve source graph identity; never use the decoder's reversible +1 embedding of export IDs as runtime allocation identity.

Equations

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

def Miri.Input.AllocationImage.provenance {P E K : Type} (memory : Memory.MemoryState P E K) (exportId : AllocationId) (immutable sharedRef : Bool) : Result Memory.CtfeProvenance

Equations

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

def Miri.Input.AllocationImage.decode {P E K : Type} (target : ABI.RuntimeTargetDataLayout) (memory : Memory.MemoryState P E K) (source : AllocationMemory) : Result Memory.Allocation

Preserve exact storage, initialized bytes, relocation offsets and CTFE flags. Arbitrary initialization and pointer provenance are imported independently; no pointer-containing byte range is silently cleared or normalized.

Equations

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

structure Miri.Input.AllocationImage.StaticInfo : Type

Source static predicates/layout queries are independent of initializer materialization. They cannot be inferred from an initializer or target triple.

• size : ABI.Size
• align : ABI.Align
• mutability : Memory.Mutability
• isStatic : Bool
• foreignItem : Bool

structure Miri.Input.AllocationImage.Queries : Type

• staticInfo : StaticAllocation → Result StaticInfo

structure Miri.Input.AllocationImage.SourceIndex (source : Array AllocationNode) : Type

• positions : Memory.KeyedArray Nat (Nat × Nat) Prod.fst
• exact : self.positions = Miri.Input.AllocationImage.sourcePositions✝ source

structure Miri.Input.AllocationImage.Imported : Type

• source : Array AllocationNode
• initializers : Array (Nat × Memory.Allocation)
• sourceIndex : Option (Miri.Input.AllocationImage.SourceIndex self.source)

def Miri.Input.AllocationImage.Imported.ofSource (source : Array AllocationNode) (initializers : Array (Nat × Memory.Allocation)) : Imported

Construct a manually assembled image without a cached source lookup index. This keeps direct test images compatible with the historical array lookup.

Equations

• Miri.Input.AllocationImage.Imported.ofSource source initializers = { source := source, initializers := initializers }

def Miri.Input.AllocationImage.Imported.withSourceIndex (source : Array AllocationNode) (initializers : Array (Nat × Memory.Allocation)) : Imported

Construct a manually assembled image with a fresh index tied to this exact source array. Replacing the source cannot reuse this dependent cache.

Equations

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

structure Miri.Input.AllocationImage.ImportResult (P E K : Type) : Type

• memory : Memory.MemoryState P E K
• outcome : Result Imported

def Miri.Input.AllocationImage.importGraph {K P E : Type} [DecidableEq K] (target : ABI.RuntimeTargetDataLayout) (definitions : Array DefinitionId) (queries : Queries) (nodes : Array AllocationNode) (initial : Memory.MemoryState P E K) : ImportResult P E K

Register identities before reconstructing any bytes: cycles and forward relocations therefore resolve through a complete source→runtime map. A failure returns all IDs already consumed by the source allocation-ID supply.

Equations

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

def Miri.Input.AllocationImage.Imported.sourceNode {P E K : Type} (image : Imported) (memory : Memory.MemoryState P E K) (id : Memory.AllocId) : Result AllocationNode

Recover the exact compiler node for a runtime global identity. Function, vtable, type-id, static and TLS leaf queries consume this retained metadata; they are never approximated by interpreting memory bytes as a code pointer.

Equations

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

def Miri.Input.AllocationImage.Imported.evaluateStaticInitializer {S : Type} (image : Imported) (state : S) (definition : Nat) : Memory.MachineHookResult S Memory.Allocation

Reuse an exported successful eval_static_initializer query at the source lazy-access hook. It remains fallible and never fabricates external/TLS data.

Equations

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