Documentation

Miri.Input.CompilerPlaceTypes

Exact debug-only place/operand type checks, place.rs:626–643 and operand.rs:805–830. The compiler's instantiated body supplies each expected place type. Runtime projection/layouts never substitute for that query.

source
def Miri.Input.CompilerPlaceTypes.expectedLayout (p : CompilerProviders.Prepared) (frame : CompilerFrameContext.ActualFrame) (requested : MIR.Place) :
Except String Interpreter.LocalLayout
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Miri.Input.CompilerPlaceTypes.check {K U : Type} (p : CompilerProviders.Prepared) (debugAssertions : Bool) (relateCovariantly : Interpreter.LocalLayout → Interpreter.LocalLayout → Interpreter.MachineHooks.M K U Bool) (requested : MIR.Place) (actual : Interpreter.LocalLayout) :
    Interpreter.MachineHooks.M K U Unit
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Miri.Input.CompilerPlaceTypes.operand {K U : Type} {C : Sort u_1} (p : CompilerProviders.Prepared) (debugAssertions : Bool) (relateCovariantly : Interpreter.LocalLayout → Interpreter.LocalLayout → Interpreter.MachineHooks.M K U Bool) :
      C → (requested : MIR.Place) → (value : Interpreter.OpTy Memory.Provenance) → Interpreter.MachineHooks.M K U Unit
      Equations
      Instances For
        source
        def Miri.Input.CompilerPlaceTypes.place {K U : Type} {C : Sort u_1} (p : CompilerProviders.Prepared) (debugAssertions : Bool) (relateCovariantly : Interpreter.LocalLayout → Interpreter.LocalLayout → Interpreter.MachineHooks.M K U Bool) :
        C → (requested : MIR.Place) → (value : Interpreter.RuntimePlace Memory.Provenance) → Interpreter.MachineHooks.M K U Unit
        Equations
        Instances For