The source Unix memory family can be attached before the wider FD/ LinuxForeign bundle exists. Common Unix memory calls use the canonical UnixMemory.emulate implementation; Linux mremap remains a separate later arm with its own compiler-backed variadic signature check.

@[reducible, inline]

abbrev Miri.Input.EvalUnixLinuxMemoryDispatchConstruction.RuntimeState (U : Type) : Type

Equations

• Miri.Input.EvalUnixLinuxMemoryDispatchConstruction.RuntimeState U = Miri.Input.EvalHostRuntimeConstruction.RuntimeState U

structure Miri.Input.EvalUnixLinuxMemoryDispatchConstruction.Components (S : Type) : Type

• memory : Interpreter.LinuxMemory.Hooks S MIR.Place Interpreter.LoadedBody Interpreter.CallInstance
• unixMemory : Interpreter.UnixForeign.OptionalHandler S
• linuxPlatform : Interpreter.UnixForeign.OptionalHandler S

def Miri.Input.EvalUnixLinuxMemoryDispatchConstruction.fromSource {U Os E C Payload : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (userRelevantCrates : Array Nat) (environment : Interpreter.UnixEnvironmentDispatch.Hooks (RuntimeState U) Os E Interpreter.EnvVars.Kind) (access : Interpreter.PlaceMachine.AccessConfig Memory.MiriMemoryKind (Interpreter.PointerMachine.User U)) (memory : EvalHostRuntimeConstruction.EnvironmentMemory U C Payload) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (Interpreter.PointerMachine.User U) Payload) (spans : Interpreter.AllocationDriver.SpanHooks) (place : Interpreter.PlaceHooks Memory.Provenance (RuntimeState U) C Interpreter.MachineHooks.FrameExtra) (choice : C) (pageSize : UInt64) (hostUsizeBits : Nat) (core : Interpreter.ForeignItems.Core Memory.Provenance (RuntimeState U) MIR.Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) Interpreter.LoadedBody Interpreter.CallInstance) : Except Interpreter.StepError (Components (RuntimeState U))

Equations

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