Source unix/foreign_items.rs random wrappers. OS checks precede ABI construction; arc4random_buf has unit return and performs no destination write.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.UnixRandomDispatch.Hooks (S D B I : Type) : Type

• random : RandomMemory.Hooks S
• signatures : ShimSignatures.CoreHooks Memory.Provenance S D (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I

  These shims depend only on ABI, symbol and operand primitives. Keeping the nonrecursive projection here lets the random family be constructed before the Unix dispatcher itself exists.

• signature : String → M S (ABI.FnAbi MIR.TyId)
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• readUsize : OpTy Memory.Provenance → M S UInt64
• readI32 : OpTy Memory.Provenance → M S Int32
• errnoNegOne : String → MPlaceTy Memory.Provenance → M S Unit
• writeNull : MPlaceTy Memory.Provenance → M S Unit
• writeTargetUsize : UInt64 → MPlaceTy Memory.Provenance → M S Unit

def Miri.Interpreter.UnixRandomDispatch.sourceHooks {S D B I : Type} (foreign : ForeignItems.Core Memory.Provenance S D (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I) (random : RandomMemory.Hooks S) (signature : String → M S (ABI.FnAbi MIR.TyId)) (errnoNegOne : String → MPlaceTy Memory.Provenance → M S Unit) (writeTargetUsize : UInt64 → MPlaceTy Memory.Provenance → M S Unit) : Hooks S D B I

Build the random family directly from source primitives. random must be the configured helpers.rs::gen_random effects (including its host fill or isolated choice tape); errno and target-isize result writes are supplied by their actual host/compiler bindings. No whole Unix or ForeignItems dispatch is needed to construct this family.

Equations

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

def Miri.Interpreter.UnixRandomDispatch.emulate {S D B I : Type} (h : Hooks S D 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.UnixRandomDispatch.dispatch {S D B I : Type} (h : Hooks S D B I) (other : String → ABI.FnAbi MIR.TyId → Array (OpTy Memory.Provenance) → MPlaceTy Memory.Provenance → M S ForeignItems.EmulateItemResult) (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.