Exact fn_abi_of_instance evidence. A full instance, ordered additional argument-type vector and explicit typing environment form the key. Runtime drop and virtual calls use the same table as observed direct/variadic calls.

structure Miri.Input.CompilerInstanceAbi.Entry : Type

• callee : Interpreter.CallInstance
• extra : Array MIR.TyId
• result : Except String (ABI.FnAbi MIR.TyId)

structure Miri.Input.CompilerInstanceAbi.Prepared : Type

• program : LoweredProgram
• entries : Array Entry
• index : Option (InstanceBuckets self.entries)

def Miri.Input.CompilerInstanceAbi.prepare (runtime : RuntimeMetadata) (program : LoweredProgram) (sourceEquality : Option (RuntimeMetadata.JsonReflexivity runtime.source.raw) := none) (abiCache : Option (CallResolution.FunctionAbiCache runtime) := none) : Except String Prepared

Equations

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

def Miri.Input.CompilerInstanceAbi.abiOfInstance (prepared : Prepared) (callee : Interpreter.CallInstance) (extra : Array MIR.TyId) : Except String (ABI.FnAbi MIR.TyId)

Equations

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

def Miri.Input.CompilerInstanceAbi.hooks {P S C E Other Extern : Type} (prepared : Prepared) (base : Interpreter.CallHooks P S C E Other Extern (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)) : Interpreter.CallHooks P S C E Other Extern (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)

Equations

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