Construct Main/Thread/TLS hooks from the fixed execution configuration. Compiler constants and native deallocation remain explicit dependencies.

@[reducible, inline]

abbrev Miri.Input.EvalEntryMachine.W (Os R Payload H D O Aff B Host : Type) : Type

Equations

• Miri.Input.EvalEntryMachine.W = Miri.Input.EvalWorld.World

@[reducible, inline]

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

Equations

• Miri.Input.EvalEntryMachine.Payload Os R P H D O Aff B Host = Miri.Interpreter.ValidityMachine.UserState (Miri.Input.EvalEntryMachine.W Os R P H D O Aff B Host)

@[reducible, inline]

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

Equations

• Miri.Input.EvalEntryMachine.InnerUser Os R P H D O Aff B Host = Miri.Interpreter.ExecutionStateTransport.Inner (Miri.Input.EvalEntryMachine.W Os R P H D O Aff B Host)

@[reducible, inline]

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

Equations

• Miri.Input.EvalEntryMachine.S Os R P H D O Aff B Host = Miri.Interpreter.MachineHooks.State Miri.Memory.MiriMemoryKind (Miri.Input.EvalEntryMachine.InnerUser Os R P H D O Aff B Host)

structure Miri.Input.EvalEntryMachine.Layouts : Type

• arguments : Interpreter.EntryArguments.Layouts
• unitPtrMut : Interpreter.LocalLayout
• unitPtrConst : Interpreter.LocalLayout
• u32 : Interpreter.LocalLayout

def Miri.Input.EvalEntryMachine.layouts (p : CompilerProviders.Prepared) : Except String Layouts

Equations

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

structure Miri.Input.EvalEntryMachine.Physical (Os R P H D O Aff B Host C : Type) : Type 1

These are already assembled source engines, not fallback implementations for instructions. No source call, memory or cleanup callback is chosen here.

• access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (InnerUser Os R P H D O Aff B Host)
• allocation : Interpreter.PlaceMachine.AllocationConfig Memory.MiriMemoryKind (InnerUser Os R P H D O Aff B Host)
• compiler : Interpreter.PlaceMachine.CompilerHooks Memory.MiriMemoryKind (InnerUser Os R P H D O Aff B Host) C
• functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (InnerUser Os R P H D O Aff B Host) O
• helpers : Interpreter.FunctionCalls.Hooks Memory.Provenance (S Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)
• deallocationError : Memory.MemoryLifecycleError → Interpreter.StepError
• deallocate : Memory.Pointer (Option Memory.Provenance) → Option (ABI.Size × ABI.Align) → Memory.MemoryKind Memory.MiriMemoryKind → Interpreter.MachineHooks.M Memory.MiriMemoryKind (InnerUser Os R P H D O Aff B Host) Unit

def Miri.Input.EvalEntryMachine.physicalFromExecution {Os R P H D O Aff B Host C ClockHost : Type} (execution : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (InnerUser Os R P H D O Aff B Host) C O ABI.ExternAbi ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (deallocationError : Memory.MemoryLifecycleError → Interpreter.StepError) (deallocate : Memory.Pointer (Option Memory.Provenance) → Option (ABI.Size × ABI.Align) → Memory.MemoryKind Memory.MiriMemoryKind → Interpreter.MachineHooks.M Memory.MiriMemoryKind (InnerUser Os R P H D O Aff B Host) Unit) : Physical Os R P H D O Aff B Host C

Equations

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

def Miri.Input.EvalEntryMachine.main {Os R P H D O Aff B Host C : Type} (p : CompilerProviders.Prepared) (physical : Physical Os R P H D O Aff B Host C) (choice : C) (layout : Layouts) (spans : Interpreter.AllocationDriver.SpanHooks) (platform : Interpreter.TlsPlatform) (format : Interpreter.ConstructorBinaryFormat) (externStatic : MIR.DefId → Interpreter.MachineHooks.M Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (W Os R P H D O Aff B Host)) (Memory.Pointer Memory.Provenance)) (evalWindows : String → String → Interpreter.MachineHooks.M Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (W Os R P H D O Aff B Host)) (Memory.Scalar Memory.Provenance)) (state : Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (W Os R P H D O Aff B Host))) : Except Interpreter.StepError (Interpreter.MainMachine.Hooks (Payload Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P)

Build source policies against the real current backend selection and single World storage. All startup/compiler failures preserve their actual prefix.

Equations

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

def Miri.Input.EvalEntryMachine.mainFromExecution {Os R P H D O Aff B Host C ClockHost : Type} (p : CompilerProviders.Prepared) (execution : Interpreter.ExecutionMachine.Config Memory.MiriMemoryKind (InnerUser Os R P H D O Aff B Host) C O ABI.ExternAbi ClockHost) (limits : Interpreter.ExecutionMachine.Limits) (deallocationError : Memory.MemoryLifecycleError → Interpreter.StepError) (deallocate : Memory.Pointer (Option Memory.Provenance) → Option (ABI.Size × ABI.Align) → Memory.MemoryKind Memory.MiriMemoryKind → Interpreter.MachineHooks.M Memory.MiriMemoryKind (InnerUser Os R P H D O Aff B Host) Unit) (choice : C) (layout : Layouts) (spans : Interpreter.AllocationDriver.SpanHooks) (platform : Interpreter.TlsPlatform) (format : Interpreter.ConstructorBinaryFormat) (externStatic : MIR.DefId → Interpreter.MachineHooks.M Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (W Os R P H D O Aff B Host)) (Memory.Pointer Memory.Provenance)) (evalWindows : String → String → Interpreter.MachineHooks.M Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (W Os R P H D O Aff B Host)) (Memory.Scalar Memory.Provenance)) (state : Interpreter.MachineHooks.State Memory.MiriMemoryKind (Interpreter.ExecutionStateTransport.Outer (W Os R P H D O Aff B Host))) : Except Interpreter.StepError (Interpreter.MainMachine.Hooks (Payload Os R P H D O Aff B Host) C O ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId) Aff P)

Standard startup assembly from the same fixed interpreter Config. Compiler entry metadata, full-instance call/return behavior, TLS operations, and main callbacks are delegated to the source constructors above.

Equations

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