Raw-host Windows process entry. Construct the canonical World once from the imported memory, runtime types, choice tape and HostRuntime lifecycle, then continue through the source-owned Windows startup and ordinary MIR runner.
def
Miri.Input.EvalWindowsRawSourceEntry.runFromSource
{Os R H D B Poll Instant System Native Profiler C External : Type}
[DecidableEq Os]
[DecidableEq Memory.MiriMemoryKind]
{Raw Listener TcpStream Error ErrorHost Meta Path AddrIter : Type}
(prepared : EvalPreparation.Prepared)
(bytes : CompilerGlobalBytes.Prepared)
(options : EvalConfigurationCore.Options)
(sourceLeaves :
EvalConfigurationCore.SourceLeaves Os R EvalSyncObjectAccess.Payload H D Interpreter.CpuAffinity.Mask B Poll Instant
System Native Profiler Raw Listener TcpStream Error ErrorHost Meta Path MIR.Place C Instant Interpreter.CallInstance
AddrIter)
(windowsHost :
EvalWindowsEnvironmentConstruction.HostEffects
(EvalWindowsSourceRunConstruction.State Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream Error)
Os Error)
(pathToOs : Path → Os)
(choice : C)
(initialConfiguration : InitialMachine.Configuration Interpreter.CpuAffinity.Mask B)
(initialMemory : Memory.MemoryState Memory.Provenance TreeBorrows.BorrowTree Memory.MiriMemoryKind)
(runtimeTypes : RuntimeArrayTypes.World)
(choiceTape : Interpreter.ExecutionChoices.Tape)
(hostRuntime : HostRuntime.Hooks External Poll Instant System Native Profiler)
(bootstrapConfiguration : EvalBootstrap.Configuration Os)
(limits : Interpreter.ExecutionMachine.Limits)
(capacity iterationFuel : Nat)
(outerChoices : List C)
:
EStateM Interpreter.StepError External
(EvalRunConstruction.RunResult
(EvalWindowsSourceRunConstruction.State Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream
Error))
Equations
- One or more equations did not get rendered due to their size.