Documentation

Miri.Interpreter.ExecutionCalls

Construct complete CallHooks from canonical runtime operations. Unlike a record-update adapter this accepts no independently supplied frame, local, copy, retag, varargs, virtual or lifecycle operation to overwrite later.

source
def Miri.Interpreter.ExecutionCalls.virtualHooks {K U C : Type} [DecidableEq K] (leaves : ExecutionCallLeaves.Virtual K U C) (access : PlaceMachine.AccessConfig K U) (operands : OperandMachine.Hooks K U C) (debugAssertions : Bool) :
VirtualCalls.Hooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra

Runtime receiver operations are the same actual reads/typed projections as ordinary operands. Source pointer construction caches alignment only.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Miri.Interpreter.ExecutionCalls.projectArgument {K U C : Type} (operands : OperandMachine.Hooks K U C) (choice : C) (argument : FnArg Memory.Provenance) (index : Nat) :
    MachineHooks.M K U (FnArg Memory.Provenance)

    Source fn_arg_project_field retains Copy versus InPlace.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Miri.Interpreter.ExecutionCalls.make {K U C Other Extern : Type} [DecidableEq K] (leaves : ExecutionCallLeaves.Hooks (MachineHooks.State K U) C Other Extern) (lifecycle : CallMachine.Lifecycle K U C) (access : PlaceMachine.AccessConfig K U) (allocation : PlaceMachine.AllocationConfig K U) (compiler : PlaceMachine.CompilerHooks K U C) (copy : PlaceCopyHooks Memory.Provenance (MachineHooks.State K U) C) (queries : TypedRetag.Hooks K U) (retagBudget virtualBudget : Nat) (operands : OperandMachine.Hooks K U C) (projection : PlaceProjectionHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra) (functions : FunctionPointers.Hooks K U Other) (virtual : VirtualCalls.Hooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra) (varargs : IntrinsicVarArgsHooks Memory.Provenance (MachineHooks.State K U) C (RuntimePlace Memory.Provenance)) (arithmetic : Memory.PointerArithmetic) (intrinsic : C → CallInstance → Array (OpTy Memory.Provenance) → RuntimeStackPlace Memory.Provenance → Option MIR.BasicBlockId → MIR.UnwindAction → MachineHooks.M K U (Option CallInstance)) :
      CallHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra 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.Interpreter.ExecutionCalls.helpers {K U C Extern Other : Type} (leaves : ExecutionCallLeaves.Helpers (MachineHooks.State K U) C Extern) (calls : CallHooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra Other Extern (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)) :
        FunctionCalls.Hooks Memory.Provenance (MachineHooks.State K U) C MachineHooks.FrameExtra Other Extern (ABI.FnAbi MIR.TyId) (ABI.ArgAbi MIR.TyId)

        Actual helpers.rs call/thread-root helper dictionary. Origin mutations keep all other thread/stack fields, including saved full frame identities.

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