Documentation

Miri.Interpreter.Panic

Pinned shims/panic.rs and mir/terminator.rs::AssertKind::panic_function. These operations call the actual panic lang item; a failed assertion is not silently converted into a normal return, UB, or a completed unwind.

source
inductive Miri.Interpreter.Panic.LangItem :
Type
Instances For
    source
    @[instance_reducible]
    instance Miri.Interpreter.Panic.instDecidableEqLangItem :
    DecidableEq LangItem
    Equations
    source
    @[instance_reducible]
    instance Miri.Interpreter.Panic.instReprLangItem :
    Repr LangItem
    Equations
    source
    def Miri.Interpreter.Panic.instReprLangItem.repr :
    LangItem → Nat → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Miri.Interpreter.Panic.assertLangItem :
      MIR.AssertKind → Except StepError LangItem

      Exact source mapping; bounds/misalignment use their argument-bearing special handlers and impossible overflowing operators are compiler errors.

      Equations
      Instances For
        source
        structure Miri.Interpreter.Panic.Hooks (K User C Other : Type) :
        Type
        Instances For
          source
          def Miri.Interpreter.Panic.start {K User C Other : Type} (h : Hooks K User C Other) (choice : C) (message : String) (unwind : MIR.UnwindAction) :
          MachineHooks.M K User Unit

          Allocate/deduplicate the message before resolving the panic lang item.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Miri.Interpreter.Panic.startNounwind {K User C Other : Type} (h : Hooks K User C Other) (choice : C) (message : String) :
            MachineHooks.M K User Unit
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Miri.Interpreter.Panic.assertPanic {K User C Other : Type} (h : Hooks K User C Other) (choice : C) (message : MIR.AssertKind) (unwind : MIR.UnwindAction) :
              MachineHooks.M K User Unit

              Read only the operands read by the source: index before length for bounds, required before found for alignment, no diagnostic operand reads otherwise.

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