Pinned linux_like/syscall.rs and thread.rs::prctl. Extra varargs may be ignored, but every argument preceding a used one must be checked first.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.LinuxSyscall.Hooks (S R F D B I : Type) : Type

• signatures : ShimSignatures.Hooks Memory.Provenance S D (MPlaceTy Memory.Provenance) (Memory.Pointer (Option Memory.Provenance)) B I
• signature : String → M S (ABI.FnAbi MIR.TyId)
• argumentTypes : Array LinuxFutex.ArgType → M S (Array MIR.TyId)
• typeBudget : Nat
• libcUsize : String → M S UInt64
• libcI32 : String → M S Int32
• readUsize : OpTy Memory.Provenance → M S UInt64
• readI32 : OpTy Memory.Provenance → M S Int32
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• writeTargetUsize : UInt64 → MPlaceTy Memory.Provenance → M S Unit
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• writeScalar : Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• random : RandomMemory.Hooks S
• futex : LinuxFutex.Hooks S R
• event : EventFd.Hooks S F
• unixGettid : String → M S UInt32
• accept4 : OpTy Memory.Provenance → OpTy Memory.Provenance → OpTy Memory.Provenance → OpTy Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• thread : UnixThread.Hooks S
• checkAccess : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S Unit

structure Miri.Interpreter.LinuxSyscall.SyscallHooks (S D MD Ptr B I F : Type) : Type

Common source syscall algorithm with only the futex and accept4 effects parameterized. The normal constructor supplies their complete semantics; source assemblies missing either capability can retain the same syscall prefix and exact branch checks before returning demand-local Unsupported.

• signatures : ShimSignatures.Hooks Memory.Provenance S D MD Ptr B I
• signature : String → M S (ABI.FnAbi MIR.TyId)
• argumentTypes : Array LinuxFutex.ArgType → M S (Array MIR.TyId)
• typeBudget : Nat
• libcUsize : String → M S UInt64
• readUsize : OpTy Memory.Provenance → M S UInt64
• readI32 : OpTy Memory.Provenance → M S Int32
• readPointer : OpTy Memory.Provenance → M S (Memory.Pointer (Option Memory.Provenance))
• writeTargetUsize : UInt64 → MPlaceTy Memory.Provenance → M S Unit
• writeInt : Int → MPlaceTy Memory.Provenance → M S Unit
• writeScalar : Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• random : RandomMemory.Hooks S
• event : EventFd.Hooks S F
• unixGettid : String → M S UInt32
• futex : ShimSignatures.Varargs Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• accept4 : Array (OpTy Memory.Provenance) → MPlaceTy Memory.Provenance → M S Unit

structure Miri.Interpreter.LinuxSyscall.PrctlHooks (S D MD Ptr B I : Type) : Type

• signatures : ShimSignatures.Hooks Memory.Provenance S D MD Ptr B I
• signature : String → M S (ABI.FnAbi MIR.TyId)
• argumentTypes : Array LinuxFutex.ArgType → M S (Array MIR.TyId)
• typeBudget : Nat
• libcI32 : String → M S Int32
• readI32 : OpTy Memory.Provenance → M S Int32
• writeScalar : Memory.Scalar Memory.Provenance → MPlaceTy Memory.Provenance → M S Unit
• thread : Option (UnixThread.Hooks S)
• checkAccess : Memory.Pointer (Option Memory.Provenance) → ABI.Size → M S Unit

def Miri.Interpreter.LinuxSyscall.syscallCore {S D MD Ptr B I F : Type} (h : SyscallHooks S D MD Ptr B I F) (name : String) (abi : ABI.FnAbi MIR.TyId) (args : Array (OpTy Memory.Provenance)) (dest : MPlaceTy Memory.Provenance) : M S Unit

All five constant lookups precede the opcode read, regardless of branch.

Equations

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

def Miri.Interpreter.LinuxSyscall.prctlCore {S D MD Ptr B I : Type} (h : PrctlHooks S D MD Ptr 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.LinuxSyscall.prctl {S R F D B I : Type} (h : Hooks S R F D 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.LinuxSyscall.syscall {S R F D B I : Type} (h : Hooks S R F D 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.LinuxSyscall.bindFutexArgs {S R F D B I : Type} (h : Hooks S R F D B I) : LinuxFutex.Hooks S R

Install the real source type checker for futex vararg prefixes.

Equations

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