def Miri.Interpreter.Native.withSupervisor {P S C V Code : Type} (h : Hooks P S C V Code) (child : Trace.ChildHooks S C) (ffi : C → Code → Array OwnedArg → FfiType → ABI.Size → RvalueM S (Array UInt8)) : Hooks P S C V Code

Install the concrete Rust supervisor/interchange pipeline around the only remaining actual libffi invocation leaf. The external implementation must build the source Cif from descriptors, consume each descriptor exactly once, and allocate the return buffer of the supplied byte size before invoking the code.

Equations

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

def Miri.Interpreter.Native.callFnArgs {P S C V Code : Type} [Memory.PointerProvenance P] (h : Hooks P S C V Code) (choice : C) (fuel : Nat) (name : String) (dest : V) (args : Array (FnArg P)) : RvalueM S Bool

Canonical call operands retain InPlace arguments as their original memory places. This matches source copy_fn_args; moving/resetting them is not invented.

Equations

• Miri.Interpreter.Native.callFnArgs h choice fuel name dest args = Miri.Interpreter.Native.call h choice fuel name dest (Array.map Miri.Interpreter.FnArg.copyFnArg args)