Canonical source process completion. The low-level bounded runner continues to expose RunResult; this module applies eval.rs's final thread and memory leak policy to real source exits before a source-facing caller receives the exit status. Diagnostics remain explicit host effects.

@[reducible, inline]

abbrev Miri.Input.EvalSourceRunFinalization.SourceState (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalSourceRunFinalization.SourceOuter (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

Equations

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

structure Miri.Input.EvalSourceRunFinalization.ReportEffects (Os R P H D O Aff B Poll Instant System Native Profiler : Type) : Type

• reportThreadLeak : Interpreter.MachineHooks.M Memory.MiriMemoryKind (SourceOuter Os R P H D O Aff B Poll Instant System Native Profiler) Unit
• reportLeaks : Interpreter.EntryResult.Leaks → Interpreter.MachineHooks.M Memory.MiriMemoryKind (SourceOuter Os R P H D O Aff B Poll Instant System Native Profiler) Unit
• ignoreLeaksNote : Interpreter.MachineHooks.M Memory.MiriMemoryKind (SourceOuter Os R P H D O Aff B Poll Instant System Native Profiler) Unit
• failureCode : Int32

inductive Miri.Input.EvalSourceRunFinalization.Result (S : Type) : Type

• finished {S : Type} (state : S) (exitCode : Int32) : Result S
• undefinedBehavior {S : Type} (state : S) (error : Interpreter.StepError) : Result S
• unsupported {S : Type} (state : S) (error : Interpreter.StepError) : Result S
• failed {S : Type} (state : S) (error : Interpreter.StepError) : Result S
• pending {S : Type} (state : S) (cause : EvalRunConstruction.PendingCause) : Result S

def Miri.Input.EvalSourceRunFinalization.instReprResult.repr {S✝ : Type} [Repr S✝] : Result S✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.EvalSourceRunFinalization.instReprResult {S✝ : Type} [Repr S✝] : Repr (Result S✝)

Equations

• Miri.Input.EvalSourceRunFinalization.instReprResult = { reprPrec := Miri.Input.EvalSourceRunFinalization.instReprResult.repr }

def Miri.Input.EvalSourceRunFinalization.finishResultProfiled {Os R H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler : Type} (profile : Lean.Options) (reports : ReportEffects Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) (ignoreLeaks : Bool) (result : EvalRunConstruction.RunResult (EvalRunConstruction.State Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) : Result (EvalRunConstruction.State Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)

Apply the pinned post-exit policy to an actual exited machine state. The thread status, TLS static roots and allocation graph come from that state; only diagnostic output and the ignore-leaks setting remain host capabilities. Pending and non-exit outcomes retain their original classification.

Equations

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

def Miri.Input.EvalSourceRunFinalization.finishResult {Os R H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler : Type} (reports : ReportEffects Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) (ignoreLeaks : Bool) (result : EvalRunConstruction.RunResult (EvalRunConstruction.State Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) : Result (EvalRunConstruction.State Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)

Equations

• Miri.Input.EvalSourceRunFinalization.finishResult reports ignoreLeaks result = Miri.Input.EvalSourceRunFinalization.finishResultProfiled ∅ reports ignoreLeaks result

theorem Miri.Input.EvalSourceRunFinalization.finishResultProfiled_eq_finishResult {Os R H D Raw Listener TcpStream Error Aff B Poll Instant System Native Profiler : Type} (profile : Lean.Options) (reports : ReportEffects Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler) (ignoreLeaks : Bool) (result : EvalRunConstruction.RunResult (EvalRunConstruction.State Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Aff B Poll Instant System Native Profiler)) : finishResultProfiled profile reports ignoreLeaks result = finishResult reports ignoreLeaks result

def Miri.Input.EvalSourceRunFinalization.runFromSourceAndFinalizeProfiled {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} (profile : Lean.Options) (prepared : EvalPreparation.Prepared) (image : AllocationImage.Imported) (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 EvalSyncObjectAccess.Payload AddrIter) (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 : ReportEffects Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler) (stableChoice : Option (EvalSourceRunConstruction.StableChoice choice) := none) : EStateM Interpreter.StepError External (Result (EvalRunConstruction.State Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler))

Full raw-host entry followed by Miri's source exit finalizer. Unlike runFromSource, this source-facing API returns an exit code only after thread-leak and reachable-allocation checks have run on the actual terminal World. The lower-level runner remains available to composed callers.

Equations

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

def Miri.Input.EvalSourceRunFinalization.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) (image : AllocationImage.Imported) (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 EvalSyncObjectAccess.Payload AddrIter) (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 : ReportEffects Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler) (stableChoice : Option (EvalSourceRunConstruction.StableChoice choice) := none) : EStateM Interpreter.StepError External (Result (EvalRunConstruction.State Os R EvalSyncPayload.Payload H D (EvalUnixSourceConstruction.Other Raw Listener TcpStream Error) Interpreter.CpuAffinity.Mask B Poll Instant System Native Profiler))

Compatibility entry with the original positional API. Profiling is opt-in through runFromSourceAndFinalizeProfiled; this entry preserves all old calls.

Equations

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