Documentation

Miri.Input.CompilerFunctionFacts

step.rs::eval_fn_call: normalized original signature and function kind, plus fn_abi_of_fn_ptr keyed by original function type and ordered extra types. The ExternAbi remains the exact compiler payload; its interpretation is explicit. No indirect runtime target is converted into a fabricated static instance.

source
structure Miri.Input.CompilerFunctionFacts.Function :
Type
Instances For
    source
    structure Miri.Input.CompilerFunctionFacts.PointerAbi :
    Type
    Instances For
      source
      structure Miri.Input.CompilerFunctionFacts.Prepared :
      Type
      Instances For
        source
        def Miri.Input.CompilerFunctionFacts.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.
        Instances For
          source
          def Miri.Input.CompilerFunctionFacts.signature (prepared : Prepared) (ty : MIR.TyId) :
          Except String (Nat × Lean.Json)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Miri.Input.CompilerFunctionFacts.kind (prepared : Prepared) (ty : MIR.TyId) :
            Except String Interpreter.CallFunctionKind
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Miri.Input.CompilerFunctionFacts.pointerAbi (prepared : Prepared) (ty : MIR.TyId) (extra : Array MIR.TyId) :
              Except String (ABI.FnAbi MIR.TyId)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Miri.Input.CompilerFunctionFacts.hooks {Extern P S C E Other : Type} (prepared : Prepared) (extern : Lean.Json → Except String Extern) (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.
                Instances For
                  source
                  def Miri.Input.CompilerFunctionFacts.concreteHooks {P S C E Other : Type} (prepared : Prepared) (base : Interpreter.CallHooks P S C E Other ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)) :
                  Interpreter.CallHooks P S C E Other ABI.ExternAbi (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)

                  Production ExternAbi identity retains every pinned source variant/unwind field, independently of the target canonical calling convention.

                  Equations
                  Instances For