Pointer/global construction on the actual EvalWorld machine. Native libraries and address mode are fixed during initialization; validateMode checks their consistency. Source: alloc_addresses/mod.rs:110–198,415–451.

@[reducible, inline]

abbrev Miri.Input.EvalPointerSource.User (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalPointerSource.User = Miri.Input.EvalCoreMachine.User

@[reducible, inline]

abbrev Miri.Input.EvalPointerSource.Stored (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalPointerSource.Stored = Miri.Input.EvalCoreMachine.Stored

@[reducible, inline]

abbrev Miri.Input.EvalPointerSource.Control (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalPointerSource.Control Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.Control (Miri.Input.EvalPointerSource.Stored Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalPointerSource.Machine (Os R P H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalPointerSource.Machine Os R P H D O Aff B Host = Miri.Interpreter.MachineAddress.State Miri.Memory.MiriMemoryKind (Miri.Input.EvalPointerSource.Control Os R P H D O Aff B Host)

@[reducible, inline]

abbrev Miri.Input.EvalPointerSource.M (Os R P H D O Aff B Host A : Type) : Type

Equations

• Miri.Input.EvalPointerSource.M Os R P H D O Aff B Host A = EStateM Miri.Interpreter.StepError (Miri.Input.EvalPointerSource.Machine Os R P H D O Aff B Host) A

def Miri.Input.EvalPointerSource.tape {Os R P H D O Aff B Host : Type} : Interpreter.ExecutionChoices.Access (Machine Os R P H D O Aff B Host)

The exact tape already retained in the shared World, with no stack view.

Equations

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

structure Miri.Input.EvalPointerSource.Leaves (Os R P H D O Aff B Host C : Type) : Type

• nativeLibraryPaths : Host → Array String
• nativeHost : Option (CompilerNativeSignatures.Host Memory.MiriMemoryKind (Control Os R P H D O Aff B Host) C)

def Miri.Input.EvalPointerSource.arrays {Os R P H D O Aff B Host : Type} : RuntimeArrayQueries.Access (Machine Os R P H D O Aff B Host)

Equations

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

def Miri.Input.EvalPointerSource.nativeEffects {Os R P H D O Aff B Host C : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (leaves : Leaves Os R P H D O Aff B Host C) : Option (Interpreter.NativeAddressSource.Effects Memory.MiriMemoryKind (Control Os R P H D O Aff B Host) C)

Full function signatures and ABI/type queries are direct compiler catalog adapters. The optional host contains only actual backing and libffi effects.

Equations

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

def Miri.Input.EvalPointerSource.validateMode {Os R P H D O Aff B Host C : Type} (leaves : Leaves Os R P H D O Aff B Host C) : M Os R P H D O Aff B Host Unit

Equations

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

def Miri.Input.EvalPointerSource.address {Os R P H D O Aff B Host C : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (leaves : Leaves Os R P H D O Aff B Host C) (choice : C) : Interpreter.MachineAddress.Hooks Memory.MiriMemoryKind (Control Os R P H D O Aff B Host)

Equations

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

def Miri.Input.EvalPointerSource.bytes {Os R P H D O Aff B Host C : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (leaves : Leaves Os R P H D O Aff B Host C) (address : Interpreter.MachineAddress.Hooks Memory.MiriMemoryKind (Control Os R P H D O Aff B Host)) : Interpreter.GlobalAllocationMachine.Bytes Memory.MiriMemoryKind (User Os R P H D O Aff B Host)

Equations

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

structure Miri.Input.EvalPointerSource.Constructed (Os R P H D O Aff B Host : Type) : Type

• address : Interpreter.MachineAddress.Hooks Memory.MiriMemoryKind (Control Os R P H D O Aff B Host)
• rootPointer : Memory.Pointer Memory.CtfeProvenance → M Os R P H D O Aff B Host (Memory.Pointer Memory.Provenance)
• globals : Memory.GlobalAllocationHooks Memory.Provenance TreeBorrows.BorrowTree Memory.MiriMemoryKind (Interpreter.PlaceMachine.AccessState Memory.MiriMemoryKind (User Os R P H D O Aff B Host))
• pointers : Interpreter.PointerMachine.Hooks Memory.MiriMemoryKind (Control Os R P H D O Aff B Host)

def Miri.Input.EvalPointerSource.make {Os R P H D O Aff B Host C : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (User Os R P H D O Aff B Host) P) (leaves : Leaves Os R P H D O Aff B Host C) (choice : C) : Constructed Os R P H D O Aff B Host

Address effects do not depend on pointer hooks. This lets global conversion close first, and ensureTreeExtra then use that real lazy conversion.

Equations

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