Source unix/foreign_items.rs outer poll and connected Unix/OS shim chain. Unknown arms remain NotSupported, with no invented fallback OS implementation.

@[reducible, inline]

abbrev Miri.Interpreter.UnixForeign.M (σ α : Type) : Type

Equations

• Miri.Interpreter.UnixForeign.M = EStateM Miri.Interpreter.StepError

@[reducible, inline]

abbrev Miri.Interpreter.UnixForeign.FD (H D O : Type) : Type

Equations

• Miri.Interpreter.UnixForeign.FD H D O = Miri.Interpreter.Files.Ref (Miri.Interpreter.Files.Description H D O)

structure Miri.Interpreter.UnixForeign.Hooks (S Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System TZ Timestamp B I : Type) : Type

• communicate : Bool
• pollAndUnblockZero : M S Unit

  Source poll_and_unblock(Some(Duration::ZERO)), exactly once per entry.

• pthreadBudget : Nat
• pollBudget : Nat
• environment : UnixEnvironmentDispatch.Hooks S Os E Kind
• fdControl : UnixFdControlDispatch.Hooks S H D Other E HM Place B I
• vector : UnixVectoredDispatch.Hooks S H D Other E HM Place B I
• dynamic : UnixDynamic.Hooks S Place B I
• fd : UnixFdDispatch.Hooks S H D Other E HM Os
• fs : UnixFsDispatch.Hooks S (FD H D Other) D Os HM Time E Kind H ReadDir DirEntry
• poll : PollDispatch.Hooks S (FD H D Other) PollIter
• pthread : PthreadDispatch.Hooks S R Duration
• socket : SocketDispatch.Hooks S (FD H D Other) E AddrIter
• memory : UnixMemory.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) B I
• tls : UnixTlsDispatch.Hooks S Place B I
• thread : UnixThreadDispatch.Hooks S Place B I
• affinity : CpuAffinityDispatch.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) B I
• event : EventFdDispatch.Hooks S (FD H D Other) Place (MPlaceTy Memory.Provenance) B I
• linuxPlatform : LinuxForeign.Hooks S Place H D Other E HM Os B I
• linux : LinuxSyscall.Hooks S R (FD H D Other) Place B I
• random : UnixRandomDispatch.Hooks S Place B I
• time : TimeShimDispatch.Hooks S Host System TZ Timestamp
• macos : MacOsForeign.Hooks S R Duration Os E Kind
• freebsd : FreeBsdForeign.Hooks S R Place E B I
• solarish : SolarishForeign.Hooks S (FD H D Other) PollIter Place E B I
• netbsd : NetBsdForeign.Hooks S Os E Kind Place B I
• stdOnly : StdOnlyShims.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) B I

@[reducible, inline]

abbrev Miri.Interpreter.UnixForeign.Handler (S : Type) : Type

Equations

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

@[reducible, inline]

abbrev Miri.Interpreter.UnixForeign.OptionalHandler (S : Type) : Type

Equations

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

structure Miri.Interpreter.UnixForeign.SourceDispatchers (S : Type) : Type

Source-owned ordered dispatch actions. The legacy complete Hooks record is one producer; the runtime source constructor can instead populate supported components and install exact-name unavailable arms without inventing the static fields of unrelated subsystems.

• os : String
• communicate : Bool
• validate : M S Unit
• pollAndUnblockZero : M S Unit
• environment : Handler S
• fd : Handler S
• fdControl : OptionalHandler S
• vector : OptionalHandler S
• fs : Handler S
• poll : Handler S
• pthread : Handler S
• socket : Handler S
• memory : OptionalHandler S
• thread : OptionalHandler S
• tls : OptionalHandler S
• affinity : OptionalHandler S
• event : OptionalHandler S
• linux : OptionalHandler S
• random : OptionalHandler S
• time : Handler S
• linuxPlatform : OptionalHandler S
• androidPlatform : OptionalHandler S
• dynamic : OptionalHandler S
• macos : OptionalHandler S
• freebsd : OptionalHandler S
• solarish : OptionalHandler S
• netbsd : OptionalHandler S
• stdOnly : Handler S

inductive Miri.Interpreter.UnixForeign.SourceGap : Type

Recognized source arms whose operation bodies have not yet been connected to the runtime factory. The matcher is kept here beside the source-order dispatcher so a missing port cannot silently fall through to native/MIR resolution. These are temporary, demand-local coverage boundaries.

• fd : SourceGap
• fdControl : SourceGap
• vector : SourceGap
• fs : SourceGap
• poll : SourceGap
• pthread : SourceGap
• socket : SourceGap
• memory : SourceGap
• thread : SourceGap
• tls : SourceGap
• affinity : SourceGap
• event : SourceGap
• linux : SourceGap
• random : SourceGap
• time : SourceGap
• linuxPlatform : SourceGap
• androidPlatform : SourceGap
• dynamic : SourceGap
• macos : SourceGap
• freebsd : SourceGap
• solarish : SourceGap
• netbsd : SourceGap

@[instance_reducible]

instance Miri.Interpreter.UnixForeign.instDecidableEqSourceGap : DecidableEq SourceGap

Equations

• Miri.Interpreter.UnixForeign.instDecidableEqSourceGap x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.UnixForeign.instReprSourceGap.repr : SourceGap → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.UnixForeign.instReprSourceGap : Repr SourceGap

Equations

• Miri.Interpreter.UnixForeign.instReprSourceGap = { reprPrec := Miri.Interpreter.UnixForeign.instReprSourceGap.repr }

def Miri.Interpreter.UnixForeign.gapRecognizes (group : SourceGap) (os env name : String) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.fd os env name = (Miri.Interpreter.UnixFdDispatch.parse name).isSome
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.fdControl os env name = (name == "fcntl" || name == "ioctl")
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.vector os env name = #["readv", "writev", "preadv", "pwritev"].contains name
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.fs os env name = (Miri.Interpreter.UnixFsDispatch.parse os name).isSome
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.poll os env name = (Miri.Interpreter.PollDispatch.parse os name).isSome
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.pthread os env name = (Miri.Interpreter.PthreadDispatch.parse name).isSome
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.socket os env name = (Miri.Interpreter.SocketDispatch.parseTarget os name).isSome
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.event os env name = ((os == "linux" || os == "android") && name == "eventfd")
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.linux os env name = ((os == "linux" || os == "android") && #["syscall", "prctl"].contains name)
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.random os env name = #["getentropy", "getrandom", "arc4random_buf"].contains name
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.androidPlatform os env name = (os == "android" && #["pread64", "pwrite64", "__errno", "gettid"].contains name)
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.dynamic os env name = (name == "dlsym" || name == "_Unwind_RaiseException")
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.freebsd os env name = (os == "freebsd" && #["__error", "_umtx_op"].contains name)
• Miri.Interpreter.UnixForeign.gapRecognizes Miri.Interpreter.UnixForeign.SourceGap.netbsd os env name = (os == "netbsd" && #["__errno", "__unsetenv13"].contains name)

def Miri.Interpreter.UnixForeign.unavailableError (os env : String) (group : SourceGap) (name : String) : StepError

Equations

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

def Miri.Interpreter.UnixForeign.unavailableHandler {S : Type} (os env : String) (group : SourceGap) : Handler S

Equations

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

def Miri.Interpreter.UnixForeign.unavailableOptional {S : Type} (os env : String) (group : SourceGap) : OptionalHandler S

Equations

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

def Miri.Interpreter.UnixForeign.dispatchSource {S Place B I : Type} (h : SourceDispatchers S) (base : ForeignItems.Core Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S ForeignItems.EmulateItemResult

The sole source-order implementation. Both complete interpreter records and source-owned component/gap assemblies route through this exact function.

Equations

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

def Miri.Interpreter.UnixForeign.environmentStdOnlySource {S : Type} (os targetEnv : String) (communicate : Bool) (environment stdOnly : Handler S) : SourceDispatchers S

Assemble a source-ordered resolver when only the environment and std-only families are currently connected. Every known Unix group is still matched at its original source position and fails closed on demand; unrecognized symbols continue to the ordinary foreign resolver. The initial pre-entry poll remains an explicit Unsupported boundary whenever communication is enabled.

Equations

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

def Miri.Interpreter.UnixForeign.dispatch {S Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System TZ Timestamp B I : Type} (h : Hooks S Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System TZ Timestamp B I) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S ForeignItems.EmulateItemResult

Equations

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

def Miri.Interpreter.UnixForeign.bindSource {S Place B I : Type} (h : SourceDispatchers S) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I

Bind a source-owned ordered dispatch chain while preserving the common ForeignItems core and all non-Unix callback arms. This is the construction boundary used by canonical runtime factories.

Equations

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

def Miri.Interpreter.UnixForeign.bind {S Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System TZ Timestamp B I : Type} (h : Hooks S Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System TZ Timestamp B I) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I

No nested fallback chain; the outer foreign resolver owns missing/native/MIR behavior after a terminal NotSupported platform response.

Equations

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

def Miri.Interpreter.UnixForeign.dynamicCall {S Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System TZ Timestamp B I : Type} (h : Hooks S Place H D Other Os HM Time E Kind ReadDir DirEntry R Duration PollIter AddrIter Host System TZ Timestamp B I) (base : ForeignItems.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) (symbol : UnixDynamic.Symbol) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : Place) (ret : Option MIR.BasicBlockId) (unwind : MIR.UnwindAction) : M S Unit

Resolve FnVal::Other through this same source foreign dispatcher, including normal return/unwind control transfer. Dynamic symbols cannot delegate to MIR.

Equations

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