Typed dispatch from pinned interpret/operator.rs::binary_op/unary_op. Compiler classification and result layouts are required queries. Float and pointer operations remain explicit machine obligations.

inductive Miri.Interpreter.ScalarTypeClass : Type

• boolean : ScalarTypeClass
• character : ScalarTypeClass
• integer (kind : MIR.IntegerKind) : ScalarTypeClass
• floating : ScalarTypeClass
• pointer : ScalarTypeClass
• functionPointer : ScalarTypeClass

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqScalarTypeClass : DecidableEq ScalarTypeClass

Equations

• Miri.Interpreter.instDecidableEqScalarTypeClass = Miri.Interpreter.instDecidableEqScalarTypeClass.decEq

def Miri.Interpreter.instDecidableEqScalarTypeClass.decEq (x✝ x✝¹ : ScalarTypeClass) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq Miri.Interpreter.ScalarTypeClass.boolean Miri.Interpreter.ScalarTypeClass.boolean = isTrue ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq Miri.Interpreter.ScalarTypeClass.boolean (Miri.Interpreter.ScalarTypeClass.integer kind) = isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq Miri.Interpreter.ScalarTypeClass.character Miri.Interpreter.ScalarTypeClass.character = isTrue ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq Miri.Interpreter.ScalarTypeClass.character (Miri.Interpreter.ScalarTypeClass.integer kind) = isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq (Miri.Interpreter.ScalarTypeClass.integer kind) Miri.Interpreter.ScalarTypeClass.boolean = isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq (Miri.Interpreter.ScalarTypeClass.integer kind) Miri.Interpreter.ScalarTypeClass.character = isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq (Miri.Interpreter.ScalarTypeClass.integer a) (Miri.Interpreter.ScalarTypeClass.integer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq (Miri.Interpreter.ScalarTypeClass.integer kind) Miri.Interpreter.ScalarTypeClass.floating = isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq (Miri.Interpreter.ScalarTypeClass.integer kind) Miri.Interpreter.ScalarTypeClass.pointer = isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq (Miri.Interpreter.ScalarTypeClass.integer kind) Miri.Interpreter.ScalarTypeClass.functionPointer = isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq Miri.Interpreter.ScalarTypeClass.floating (Miri.Interpreter.ScalarTypeClass.integer kind) = isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq Miri.Interpreter.ScalarTypeClass.floating Miri.Interpreter.ScalarTypeClass.floating = isTrue ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq Miri.Interpreter.ScalarTypeClass.pointer (Miri.Interpreter.ScalarTypeClass.integer kind) = isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq Miri.Interpreter.ScalarTypeClass.pointer Miri.Interpreter.ScalarTypeClass.pointer = isTrue ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq Miri.Interpreter.ScalarTypeClass.functionPointer (Miri.Interpreter.ScalarTypeClass.integer kind) = isFalse ⋯
• Miri.Interpreter.instDecidableEqScalarTypeClass.decEq Miri.Interpreter.ScalarTypeClass.functionPointer Miri.Interpreter.ScalarTypeClass.functionPointer = isTrue ⋯

def Miri.Interpreter.instReprScalarTypeClass.repr : ScalarTypeClass → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprScalarTypeClass : Repr ScalarTypeClass

Equations

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

structure Miri.Interpreter.ScalarOpsHooks (Prov S C : Type) : Type

• classify : C → MIR.TyId → RvalueM S ScalarTypeClass
• boolLayout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)
• orderingLayout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)
• overflowLayout : C → ABI.TyAndLayout MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• metadataLayout : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• unitLayout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)
• floatBinary : C → MIR.BinOp → RvalueImmTy Prov → RvalueImmTy Prov → RvalueM S (RvalueImmTy Prov)
• pointerBinary : C → MIR.BinOp → RvalueImmTy Prov → RvalueImmTy Prov → RvalueM S (RvalueImmTy Prov)
• floatUnary : C → MIR.UnOp → RvalueImmTy Prov → RvalueM S (RvalueImmTy Prov)
• derefValidity : C → RvalueImmTy Prov → RvalueM S Unit

def Miri.Interpreter.ScalarOps.scalarIntError : Memory.ScalarIntError → StepError

Equations

• Miri.Interpreter.ScalarOps.scalarIntError (Miri.Memory.ScalarIntError.invalidBool value) = Miri.Interpreter.StepError.undefinedBehavior (toString (Miri.Memory.ScalarIntError.invalidBool value))
• Miri.Interpreter.ScalarOps.scalarIntError (Miri.Memory.ScalarIntError.invalidChar value) = Miri.Interpreter.StepError.undefinedBehavior (toString (Miri.Memory.ScalarIntError.invalidChar value))
• Miri.Interpreter.ScalarOps.scalarIntError x✝ = Miri.Interpreter.StepError.invalidProgram (toString x✝)

def Miri.Interpreter.ScalarOps.scalarError : Memory.ScalarError → StepError

Equations

• Miri.Interpreter.ScalarOps.scalarError (Miri.Memory.ScalarError.scalarInt e) = Miri.Interpreter.ScalarOps.scalarIntError e
• Miri.Interpreter.ScalarOps.scalarError Miri.Memory.ScalarError.readPointerAsInt = Miri.Interpreter.StepError.unsupported "read pointer as integer"
• Miri.Interpreter.ScalarOps.scalarError x✝ = Miri.Interpreter.StepError.invalidProgram (toString x✝)

def Miri.Interpreter.ScalarOps.immediateError : ImmediateError → StepError

Equations

• Miri.Interpreter.ScalarOps.immediateError (Miri.Interpreter.ImmediateError.scalar e) = Miri.Interpreter.ScalarOps.scalarError e
• Miri.Interpreter.ScalarOps.immediateError Miri.Interpreter.ImmediateError.unexpectedUninit = Miri.Interpreter.StepError.invalidProgram "uninitialized immediate reached scalar operator"
• Miri.Interpreter.ScalarOps.immediateError Miri.Interpreter.ImmediateError.expectedInteger = Miri.Interpreter.StepError.unsupported "read pointer as integer"
• Miri.Interpreter.ScalarOps.immediateError x✝ = Miri.Interpreter.StepError.invalidProgram (toString (repr x✝))

def Miri.Interpreter.ScalarOps.integerError : IntegerOpError → StepError

Equations

• Miri.Interpreter.ScalarOps.integerError (Miri.Interpreter.IntegerOpError.scalar e) = Miri.Interpreter.ScalarOps.scalarIntError e
• Miri.Interpreter.ScalarOps.integerError (Miri.Interpreter.IntegerOpError.undefinedBehavior e) = Miri.Interpreter.StepError.undefinedBehavior (toString (repr e))
• Miri.Interpreter.ScalarOps.integerError x✝ = Miri.Interpreter.StepError.invalidProgram (toString (repr x✝))

def Miri.Interpreter.ScalarOps.binary {Prov S C : Type} [Memory.PointerProvenance Prov] (h : ScalarOpsHooks Prov S C) (choice : C) (op : MIR.BinOp) (left right : RvalueImmTy Prov) : RvalueM S (RvalueImmTy Prov)

Match on the compiler-owned left type; differing type IDs remain distinct when their ABI sizes or scalar representations happen to agree.

Equations

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

def Miri.Interpreter.ScalarOps.unary {Prov S C : Type} [Memory.PointerProvenance Prov] (h : ScalarOpsHooks Prov S C) (choice : C) (op : MIR.UnOp) (value : RvalueImmTy Prov) : RvalueM S (RvalueImmTy Prov)

Equations

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