Target gate for the canonical Linux syscall algorithm. Core supplies the same algorithm's source branch capabilities, with missing futex/accept4 effects reported only after their pinned syscall prefixes are checked.

@[reducible, inline]

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

Equations

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

structure Miri.Interpreter.LinuxSyscallPartialDispatch.Hooks (S D MD Ptr B I F : Type) : Type

• os : String
• syscall : LinuxSyscall.SyscallHooks S D MD Ptr B I F
• prctl : LinuxSyscall.PrctlHooks S D MD Ptr B I

def Miri.Interpreter.LinuxSyscallPartialDispatch.emulate {S D MD Ptr B I F : Type} (h : Hooks 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 (Option ForeignItems.EmulateItemResult)

Equations

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