Remaining solarish/foreign_items.rs operations. Existing thread/socket/ __sysconf wrappers are dispatched by their canonical shared modules.

@[reducible, inline]

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

Equations

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

def Miri.Interpreter.SolarishForeign.dynamicSymbol (name : String) : Bool

Equations

• Miri.Interpreter.SolarishForeign.dynamicSymbol name = (name == "pthread_setname_np")

structure Miri.Interpreter.SolarishForeign.Hooks (S F Iter D E B I : Type) : Type

• foreign : ForeignItems.Hooks Memory.Provenance S D (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I
• errors : IoError.Hooks S E
• epoll : EpollShims.Hooks S F Iter
• event : EventFd.Hooks S F
• pollBudget : Nat
• readI32 : OpTy Memory.Provenance → M S Int32
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• isNull : Memory.Pointer (Option Memory.Provenance) → M S Bool
• libcI32 : String → M S Int32
• derefStack : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• derefU32 : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• projectNamed : MPlaceTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• stackAddress : UInt64
• stackSize : UInt64
• numCpus : UInt32

structure Miri.Interpreter.SolarishForeign.CoreHooks (S F Iter D E B I : Type) : Type

Narrow source constructor interface for the Solarish arms. Their shim semantics use only the shared nonrecursive foreign-item core, so callers that build a platform arm must not fabricate unrelated math/Unix/Windows dispatch callbacks just to provide symbol checking and pointer writes.

• foreign : ForeignItems.Core Memory.Provenance S D (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I
• errors : IoError.Hooks S E
• epoll : EpollShims.Hooks S F Iter
• event : EventFd.Hooks S F
• pollBudget : Nat
• readI32 : OpTy Memory.Provenance → M S Int32
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• isNull : Memory.Pointer (Option Memory.Provenance) → M S Bool
• libcI32 : String → M S Int32
• derefStack : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• derefU32 : OpTy Memory.Provenance → M S (MPlaceTy Memory.Provenance)
• projectNamed : MPlaceTy Memory.Provenance → String → M S (MPlaceTy Memory.Provenance)
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• stackAddress : UInt64
• stackSize : UInt64
• numCpus : UInt32

def Miri.Interpreter.SolarishForeign.emulateCore {S F Iter D E B I : Type} (h : CoreHooks S F Iter D E 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.

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

Compatibility entry point for the legacy complete foreign-item record. The actual Solarish arms project only its common source Core.

Equations

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