Build the source Unix/Linux memory shims over the execution's canonical memory, allocation, provenance, Tree Borrows and errno state. Host resources do not participate in these operations.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixMemoryConstruction.M (U A : Type) : Type

Equations

• Miri.Input.EvalUnixMemoryConstruction.M U A = Miri.Input.EvalHostRuntimeConstruction.RuntimeM U A

fromSource derives target layouts, constants, frame policy and ABI from the prepared compiler. The supplied memory bundle is the one used by MIR, so pointer-output writes and remap allocation retain the live execution state.

def Miri.Input.EvalUnixMemoryConstruction.fromSource {U Os E B I C Payload : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (userRelevantCrates : Array Nat) (environment : Interpreter.UnixEnvironmentDispatch.Hooks (RuntimeState U) Os E Interpreter.EnvVars.Kind) (signatures : Interpreter.ShimSignatures.Hooks Memory.Provenance (RuntimeState U) MIR.Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) (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) : Except Interpreter.StepError (Interpreter.LinuxMemory.Hooks (RuntimeState U) MIR.Place B I)

Equations

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