Source construction for the remaining Windows platform shims. Compiler ABI/layout, guest reads and writes, allocation identity, dynamic function identity, process exit and unwind are attached to the same prepared target and Main state. Host path and error text plus configured machine facts remain explicit leaves; the command line comes from the initialized Main entry root.

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsPlatformConstruction.Payload Os R P H D O Aff B Host = Miri.Input.EvalRuntimeConstruction.EntryUser Os R P H D O Aff B Host

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsPlatformConstruction.State Os R P H D O Aff B Host = Miri.Input.EvalStartupAssembly.State Os R P H D O Aff B Host

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsPlatformConstruction.Inner Os R P H D O Aff B Host = Miri.Input.EvalStartupAssembly.InnerControl Os R P H D O Aff B Host

@[reducible, inline]

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

Equations

• Miri.Input.EvalWindowsPlatformConstruction.InnerState Os R P H D O Aff B Host = Miri.Input.EvalStartupAssembly.InnerState Os R P H D O Aff B Host

@[reducible, inline]

abbrev Miri.Input.EvalWindowsPlatformConstruction.M (S A : Type) : Type

Equations

• Miri.Input.EvalWindowsPlatformConstruction.M S A = EStateM Miri.Interpreter.StepError S A

structure Miri.Input.EvalWindowsPlatformConstruction.HostEffects (S Os E : Type) : Type

• currentExe : M S (Option Os)
• hostErrorDisplay : Interpreter.IoError.HostError E → M S Os
• unknownMessageDisplay : Memory.Scalar Memory.Provenance → M S Os
• pageSize : UInt64
• numCpus : UInt32

def Miri.Input.EvalWindowsPlatformConstruction.fromSource [DecidableEq Memory.MiriMemoryKind] {Os R P H D O Aff B Host C Error F : Type} (p : CompilerProviders.Prepared) (main : 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 Interpreter.ProgramExitPoll) (environment : Interpreter.WindowsEnvironment.Hooks (State Os R P H D O Aff B Host) Os Error Interpreter.EnvVars.Kind) (memory : EvalWindowsEnvironmentConstruction.Memory Os R P H D O Aff B Host C) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (Interpreter.PointerMachine.User (Inner Os R P H D O Aff B Host)) P) (spans : Interpreter.AllocationDriver.SpanHooks) (handles : Interpreter.WindowsHandles.Hooks (State Os R P H D O Aff B Host) F) (embed : Interpreter.WindowsPlatform.DynamicSymbol → O) (place : Interpreter.PlaceHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (projection : Interpreter.PlaceProjectionHooks Memory.Provenance (State Os R P H D O Aff B Host) C Interpreter.MachineHooks.FrameExtra) (choice : C) (host : HostEffects (State Os R P H D O Aff B Host) Os Error) (startExit : Int32 → M (State Os R P H D O Aff B Host) Unit) (unwind : Interpreter.Unwind.Hooks Memory.MiriMemoryKind (Interpreter.ThreadStacks.Storage (Payload Os R P H D O Aff B Host)) C O) (compatibilityBudget : Nat) : Except Interpreter.StepError (Interpreter.WindowsPlatformDispatch.Hooks (State Os R P H D O Aff B Host) Os Error Interpreter.EnvVars.Kind F)

Equations

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