Windows source-facing process completion. The Windows raw entry shares the canonical machine state and post-exit policy; retain its low-level RunResult API while providing a source entry that performs real leak checks.
def
Miri.Input.EvalWindowsSourceRunFinalization.runFromSourceAndFinalize
{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)
(ignoreLeaks : Bool)
(reports :
EvalSourceRunFinalization.ReportEffects Os R EvalSyncPayload.Payload H D
(EvalWindowsSourceRunConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant
System Native Profiler)
:
EStateM Interpreter.StepError External
(EvalSourceRunFinalization.Result
(EvalWindowsSourceRunConstruction.State Os R H D B Poll Instant System Native Profiler Raw Listener TcpStream
Error))
Windows raw-host startup and MIR execution followed by the same canonical thread and reachable-allocation finalization used by Unix. Reporting and the ignore-leaks setting remain explicit host capabilities.
Equations
- One or more equations did not get rendered due to their size.