Source construction for Linux foreign-item runtime bindings over canonical inner EvalWorld memory. Function identity, static lookup and TLS registration read the one live function registry, static registry and TLS arena.

structure Miri.Input.EvalUnixLinuxConstruction.Components (S Place H D O E HM Os B I : Type) : Type

• linuxPlatform : Interpreter.LinuxForeign.Hooks S Place H D O E HM Os B I

@[reducible, inline]

abbrev Miri.Input.EvalUnixLinuxConstruction.SourceWorld (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixLinuxConstruction.SourceControl (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixLinuxConstruction.SourceUser (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Input.EvalUnixLinuxConstruction.SourceState (Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error : Type) : Type

Equations

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

def Miri.Input.EvalUnixLinuxConstruction.fromSource {Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error E ShimBody I HM C Path : Type} [DecidableEq Memory.MiriMemoryKind] (p : CompilerProviders.Prepared) (userRelevantCrates : Array Nat) (environment : Interpreter.UnixEnvironmentDispatch.Hooks (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) Os E Interpreter.EnvVars.Kind) (signatures : Interpreter.ShimSignatures.Hooks Memory.Provenance (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) MIR.Place (Interpreter.MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) ShimBody I) (fd : Interpreter.UnixFdDispatch.Hooks (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) H D (EvalSocketStorage.Other Raw Listener TcpStream Error) E HM Path) (unixGettid : String → EStateM Interpreter.StepError (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (Memory.Scalar Memory.Provenance)) (place : Interpreter.PlaceHooks Memory.Provenance (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C Interpreter.MachineHooks.FrameExtra) (choice : C) (pageSize : UInt64) (memory : EvalHostRuntimeConstruction.EnvironmentMemory (SourceControl Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) C P) (extras : Interpreter.MemoryExtras.Hooks Memory.MiriMemoryKind (SourceUser Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) P) (spans : Interpreter.AllocationDriver.SpanHooks) (functions : Interpreter.FunctionPointers.Hooks Memory.MiriMemoryKind (SourceUser Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) (EvalSocketStorage.Other Raw Listener TcpStream Error)) : Except Interpreter.StepError (Components (SourceState Os R P H D Aff B Poll Instant System Native Profiler Raw Listener TcpStream Error) MIR.Place H D (EvalSocketStorage.Other Raw Listener TcpStream Error) E HM Path ShimBody I)

Build the Linux component in the actual inner EvalWorld state. Its Unix memory fields come from EvalUnixMemoryConstruction.fromSource, including compiler-layout checked pointer-output dereference, source range validation, and Miri's Zero-growth mmap reallocation for mremap.

Equations

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