Pinned interpret/step.rs:160-300 dispatcher. Required machine operations are effectful obligations; every failure preserves its resulting state.

structure Miri.Interpreter.RvalueImmTy (Prov : Type) : Type

• imm : Immediate Prov
• layout : ABI.TyAndLayout MIR.TyId

def Miri.Interpreter.instDecidableEqRvalueImmTy.decEq {Prov✝ : Type} [DecidableEq Prov✝] (x✝ x✝¹ : RvalueImmTy Prov✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqRvalueImmTy.decEq { imm := a, layout := a_1 } { imm := b, layout := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqRvalueImmTy {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (RvalueImmTy Prov✝)

Equations

• Miri.Interpreter.instDecidableEqRvalueImmTy = Miri.Interpreter.instDecidableEqRvalueImmTy.decEq

def Miri.Interpreter.instReprRvalueImmTy.repr {Prov✝ : Type} [Repr Prov✝] : RvalueImmTy Prov✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprRvalueImmTy {Prov✝ : Type} [Repr Prov✝] : Repr (RvalueImmTy Prov✝)

Equations

• Miri.Interpreter.instReprRvalueImmTy = { reprPrec := Miri.Interpreter.instReprRvalueImmTy.repr }

@[reducible, inline]

abbrev Miri.Interpreter.RvalueM (S A : Type) : Type

Equations

• Miri.Interpreter.RvalueM S A = EStateM Miri.Interpreter.StepError S A

structure Miri.Interpreter.RvalueHooks (Prov S C V : Type) : Type 1

• placeLayout : V → ABI.TyAndLayout MIR.TyId
• evalPlace : C → MIR.Place → Bool → RvalueM S V
• evalOperand : C → MIR.Operand → Option (ABI.TyAndLayout MIR.TyId) → RvalueM S (OpTy Prov)
• evalOperandAt : C → OperandPath → MIR.Operand → Option (ABI.TyAndLayout MIR.TyId) → RvalueM S (OpTy Prov)
• evalPlaceToOp : C → MIR.Place → Option (ABI.TyAndLayout MIR.TyId) → RvalueM S (OpTy Prov)
• readImmediate : C → OpTy Prov → RvalueM S (RvalueImmTy Prov)
• writeImmediate : C → Immediate Prov → V → RvalueM S Unit
• writePointer : C → Memory.Pointer (Option Prov) → V → RvalueM S Unit
• threadLocalPointer : C → MIR.DefId → RvalueM S (Memory.Pointer (Option Prov))
• withRetagMode {A : Type} : C → TreeBorrows.RetagPolicy.RetagMode → RvalueM S A → RvalueM S A
• copyOp : C → OpTy Prov → V → RvalueM S Unit
• copyOpAllowTransmute : C → OpTy Prov → V → RvalueM S Unit
• binaryOp : C → MIR.BinOp → RvalueImmTy Prov → RvalueImmTy Prov → RvalueM S (RvalueImmTy Prov)
• unaryOp : C → MIR.UnOp → RvalueImmTy Prov → RvalueM S (RvalueImmTy Prov)
• writeAggregate : C → MIR.AggregateKind → Array MIR.Operand → V → RvalueM S Unit
• writeRepeat : C → MIR.Operand → V → RvalueM S Unit
• forceAllocation : C → V → RvalueM S (MemPlace Prov)
• toRef : C → MemPlace Prov → RvalueM S (Immediate Prov)
• enforceValidity : C → ABI.TyAndLayout MIR.TyId → RvalueM S Bool
• retagPtrValue : C → RvalueImmTy Prov → MIR.TyId → RvalueM S (Option (RvalueImmTy Prov))
• placeBaseRaw : C → MIR.Place → RvalueM S Bool
• normalize : C → MIR.TyId → RvalueM S MIR.TyId
• cast : C → OpTy Prov → MIR.CastKind → MIR.TyId → V → RvalueM S Unit
• readDiscriminant : C → OpTy Prov → RvalueM S MIR.VariantIndex
• discriminantForVariant : C → MIR.TyId → MIR.VariantIndex → RvalueM S (RvalueImmTy Prov)

def Miri.Interpreter.evalRvalueIntoPlace {P S C V : Type} (h : RvalueHooks P S C V) (choice : C) (rvalue : MIR.Rvalue) (place : MIR.Place) : RvalueM S Unit

Destination evaluation is always first, with the source's skip-validity flag. No hook has a default implementation or a default successful outcome.

Equations

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

def Miri.Interpreter.runRvalue {S A : Type} (action : RvalueM S A) (state : S) : StepResult S A

Adapt the effect result to the statement driver's state-preserving result.

Equations

• Miri.Interpreter.runRvalue action state = match action state with | EStateM.Result.ok value state => (state, Except.ok value) | EStateM.Result.error error state => (state, Except.error error)