Remaining pinned Linux/Android foreign arms; shared filesystem/statx, thread-name/gettid, epoll/eventfd, syscall/prctl, strerror and std guards stay in their canonical modules and are composed by UnixForeign.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.LinuxForeign.Hooks (S Place H D Other E HM Os B I : Type) : Type

• signatures : ShimSignatures.Hooks Memory.Provenance S Place (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I
• signature : String → M S (ABI.FnAbi MIR.TyId)
• fd : UnixFdDispatch.Hooks S H D Other E HM Os
• memory : LinuxMemory.Hooks S Place B I
• errors : IoError.Hooks S E
• readScalar : OpTy Memory.Provenance → M S (Memory.Scalar Memory.Provenance)
• readI64 : OpTy Memory.Provenance → M S Int64
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• unixGettid : String → M S (Memory.Scalar Memory.Provenance)
• targetEnv : String
• dsoHandle : M S (Memory.Pointer (Option Memory.Provenance))
• getPtrFnInstance : Memory.Pointer (Option Memory.Provenance) → M S CallInstance
• addThreadAtexit : CallInstance → Memory.Scalar Memory.Provenance → M S Unit

def Miri.Interpreter.LinuxForeign.positional {S Place H D O E HM Os B I : Type} (h : Hooks S Place H D O E HM Os B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S Unit

Equations

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

def Miri.Interpreter.LinuxForeign.emulate {S Place H D O E HM Os B I : Type} (h : Hooks S Place H D O E HM Os B I) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S (Option ForeignItems.EmulateItemResult)

Equations

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