Native mod.rs::call_native_raw direct orchestration. Source lines96–126 publish the actual InterpCx interchange pointer, run Supervisor::do_ffi, clear that pointer, then return its result (including an interpreter error). Actual libffi invocation and stable host storage remain explicit external effects.

@[reducible, inline]

abbrev Miri.Interpreter.NativeExecutor.State (K U : Type) : Type

Equations

• Miri.Interpreter.NativeExecutor.State = Miri.Interpreter.NativeMachine.State

@[reducible, inline]

abbrev Miri.Interpreter.NativeExecutor.M (K U A : Type) : Type

Equations

• Miri.Interpreter.NativeExecutor.M = Miri.Interpreter.NativeMachine.M

structure Miri.Interpreter.NativeExecutor.Hooks (K U C Code : Type) : Type

• supervisor : Native.Trace.ChildHooks (State K U) C
• ffi : (Memory.AllocId → Array UInt8 → M K U Unit) → C → Code → Array Native.OwnedArg → Native.FfiType → ABI.Size → M K U (Array UInt8)

  Build source Cif descriptors, consume each once, allocate a zeroed return buffer of precisely size, perform the actual FFI call, and report changed backings via publish on every returning outcome. Arbitrary native code may diverge; this is not a termination or safety contract.

def Miri.Interpreter.NativeExecutor.execute {K U C Code : Type} (h : Hooks K U C Code) (publish : Memory.AllocId → Array UInt8 → M K U Unit) (choice : C) (code : Code) (arguments : Array Native.OwnedArg) (resultType : Native.FfiType) (size : ABI.Size) : M K U (Array UInt8 × Option (Array Native.AccessEvent))

Source supervisor locking/tracing/protection order is executed by the ported driver, rather than supplied as a replacement whole rawCall callback.

Equations

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