Documentation

Miri.Interpreter.Step

Small-step driver port of pinned rustc interpret/step.rs:41-154. Callbacks are mandatory semantic obligations, including their mutations on failure.

source
structure Miri.Interpreter.StepState (Prov Layout Extra Machine : Type) :
Type
  • stack : Stack Prov Layout Extra
  • machine : Machine
Instances For
    source
    inductive Miri.Interpreter.StepError :
    Type
    Instances For
      source
      @[instance_reducible]
      instance Miri.Interpreter.instReprStepError :
      Repr StepError
      Equations
      source
      def Miri.Interpreter.instReprStepError.repr :
      StepError → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance Miri.Interpreter.instDecidableEqStepError :
        DecidableEq StepError
        Equations
        source
        def Miri.Interpreter.instDecidableEqStepError.decEq (x✝ x✝¹ : StepError) :
        Decidable (x✝ = x✝¹)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[reducible, inline]
          abbrev Miri.Interpreter.StepResult (S A : Type) :
          Type
          Equations
          Instances For
            source
            structure Miri.Interpreter.StepHooks (Prov Layout Extra Machine Choice PlaceValue : Type) :
            Type

            Required interpreter operations. Choice inputs are explicit; no operation has a default successful implementation. evalPlace receives the source's skip_validity_for_simple_deref = false argument.

            Instances For
              source
              def Miri.Interpreter.Step.evalStatement {P L E M C V : Type} (hooks : StepHooks P L E M C V) (choice : C) (stmt : MIR.Statement) (state : StepState P L E M) :
              StepResult (StepState P L E M) Unit
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Miri.Interpreter.Step.step {P L E M C V : Type} (hooks : StepHooks P L E M C V) (choice : C) (state : StepState P L E M) :
                StepResult (StepState P L E M) Bool

                Execute exactly one source driver iteration. A callback failure retains its resulting state and stops immediately, before any subsequent operation.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Miri.Interpreter.Step.AllowedStep {P L E M C V : Type} (hooks : StepHooks P L E M C V) (allowedChoice : StepState P L E M → C → Prop) (before after : StepState P L E M) (outcome : Except StepError Bool) :
                  Prop

                  Relational semantics quantifies over permitted explicit choice inputs. No enumeration or finite-support assumption is imposed on machine choices.

                  Equations
                  Instances For