inductive Miri.Interpreter.IntrinsicX86.FloatErrorMode : Type

• none : FloatErrorMode
• random : FloatErrorMode
• max : FloatErrorMode

@[instance_reducible]

instance Miri.Interpreter.IntrinsicX86.instDecidableEqFloatErrorMode : DecidableEq FloatErrorMode

Equations

• Miri.Interpreter.IntrinsicX86.instDecidableEqFloatErrorMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.IntrinsicX86.instReprFloatErrorMode.repr : FloatErrorMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.IntrinsicX86.instReprFloatErrorMode : Repr FloatErrorMode

Equations

• Miri.Interpreter.IntrinsicX86.instReprFloatErrorMode = { reprPrec := Miri.Interpreter.IntrinsicX86.instReprFloatErrorMode.repr }

structure Miri.Interpreter.IntrinsicX86.Hooks (P S C V : Type) : Type

• architecture : ArchitectureHooks P S C V
• x86_64 : Bool
• sse2Enabled : Bool
• yieldThread : C → RvalueM S Unit
• arrayLayout : C → MIR.TyId → UInt64 → RvalueM S (ABI.TyAndLayout MIR.TyId)
• integerLayout : C → Nat → Bool → RvalueM S (ABI.TyAndLayout MIR.TyId)
• transmuteRead : C → OpTy P → ABI.TyAndLayout MIR.TyId → RvalueM S (OpTy P)
• transmuteWrite : C → V → ABI.TyAndLayout MIR.TyId → RvalueM S V
• twiceWideLayout : C → MIR.TyId → RvalueM S (ABI.TyAndLayout MIR.TyId)
• sqrt : C → FloatBits → RvalueM S FloatBits

  Source uses host sqrt for rsqrt; this is its explicit numerical boundary.

• floatNondet : Bool
• roundingError : FloatErrorMode
• errorMagnitude : C → Nat → RvalueM S Nat
• errorNegative : C → RvalueM S Bool
• memCopy : C → Memory.Pointer (Option P) → Memory.Pointer (Option P) → ABI.Size → Bool → RvalueM S Unit

@[reducible, inline]

abbrev Miri.Interpreter.IntrinsicX86.M (S A : Type) : Type

Equations

• Miri.Interpreter.IntrinsicX86.M S A = Miri.Interpreter.RvalueM S A

def Miri.Interpreter.IntrinsicX86.invalid {S A : Type} (message : String) : M S A

Equations

• Miri.Interpreter.IntrinsicX86.invalid message = throw (Miri.Interpreter.StepError.invalidProgram message)

def Miri.Interpreter.IntrinsicX86.liftResult {A S : Type} (result : Except StepError A) : M S A

Equations

• Miri.Interpreter.IntrinsicX86.liftResult (Except.ok value) = pure value
• Miri.Interpreter.IntrinsicX86.liftResult (Except.error error) = throw error

def Miri.Interpreter.IntrinsicX86.scalarResult {A S : Type} (result : Except Memory.ScalarError A) : M S A

Equations

• Miri.Interpreter.IntrinsicX86.scalarResult result = Miri.Interpreter.IntrinsicX86.liftResult (Except.mapError Miri.Interpreter.ScalarOps.scalarError result)

def Miri.Interpreter.IntrinsicX86.floatResult {A S : Type} (result : Except FloatError A) : M S A

Equations

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

def Miri.Interpreter.IntrinsicX86.sizeResult {A S : Type} (result : Except ABI.SizeError A) : M S A

Equations

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

def Miri.Interpreter.IntrinsicX86.arg {P S : Type} (args : Array (OpTy P)) (i : Nat) : M S (OpTy P)

Equations

• Miri.Interpreter.IntrinsicX86.arg args i = match args[i]? with | some value => pure value | none => Miri.Interpreter.IntrinsicX86.invalid "x86 argument missing"

def Miri.Interpreter.IntrinsicX86.signature {P S C V : Type} (h : Hooks P S C V) (choice : C) (name : String) (args : Array (OpTy P)) (n : Nat) : M S Unit

Equations

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

def Miri.Interpreter.IntrinsicX86.feature {P S C V : Type} (h : Hooks P S C V) (choice : C) (name feature : String) : M S Unit

Equations

• Miri.Interpreter.IntrinsicX86.feature h choice name feature = h.architecture.expectFeature choice name feature

def Miri.Interpreter.IntrinsicX86.scalar {P S : Type} (value : RvalueImmTy P) : M S (Memory.Scalar P)

Equations

• Miri.Interpreter.IntrinsicX86.scalar value = Miri.Interpreter.IntrinsicX86.liftResult (Except.mapError Miri.Interpreter.ScalarOps.immediateError value.imm.toScalar)

def Miri.Interpreter.IntrinsicX86.read {P S C V : Type} (h : Hooks P S C V) (choice : C) (op : OpTy P) : M S (Memory.Scalar P)

Equations

• Miri.Interpreter.IntrinsicX86.read h choice op = do let __do_lift ← h.architecture.simd.readImmediate choice op Miri.Interpreter.IntrinsicX86.scalar __do_lift

def Miri.Interpreter.IntrinsicX86.readLane {P S C V : Type} (h : Hooks P S C V) (choice : C) (op : OpTy P) (i : UInt64) : M S (RvalueImmTy P)

Equations

• Miri.Interpreter.IntrinsicX86.readLane h choice op i = do let __do_lift ← h.architecture.simd.indexRead choice op i h.architecture.simd.readImmediate choice __do_lift

def Miri.Interpreter.IntrinsicX86.readScalarLane {P S C V : Type} (h : Hooks P S C V) (choice : C) (op : OpTy P) (i : UInt64) : M S (Memory.Scalar P)

Equations

• Miri.Interpreter.IntrinsicX86.readScalarLane h choice op i = do let __do_lift ← h.architecture.simd.indexRead choice op i Miri.Interpreter.IntrinsicX86.read h choice __do_lift

def Miri.Interpreter.IntrinsicX86.write {P S C V : Type} (h : Hooks P S C V) (choice : C) (value : Memory.Scalar P) (dest : V) : M S Unit

Equations

• Miri.Interpreter.IntrinsicX86.write h choice value dest = h.architecture.simd.writeImmediate choice (Miri.Interpreter.Immediate.scalar value) dest

def Miri.Interpreter.IntrinsicX86.length {S : Type} (layout : ABI.TyAndLayout MIR.TyId) : M S UInt64

Equations

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

def Miri.Interpreter.IntrinsicX86.projectRead {P S C V : Type} (h : Hooks P S C V) (choice : C) (op : OpTy P) : M S (OpTy P × UInt64)

Equations

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

def Miri.Interpreter.IntrinsicX86.projectWrite {P S C V : Type} (h : Hooks P S C V) (choice : C) (dest : V) : M S (V × UInt64)

Equations

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

def Miri.Interpreter.IntrinsicX86.same {S : Type} (a b : UInt64) : M S Unit

Equations

• Miri.Interpreter.IntrinsicX86.same a b = if (a == b) = true then pure () else Miri.Interpreter.IntrinsicX86.invalid "x86 vector length mismatch"

def Miri.Interpreter.IntrinsicX86.checkedIndex {S : Type} (n : Nat) : M S UInt64

Equations

• Miri.Interpreter.IntrinsicX86.checkedIndex n = if n < 2 ^ 64 then pure (UInt64.ofNat n) else Miri.Interpreter.IntrinsicX86.invalid "x86 strict index arithmetic overflow"

def Miri.Interpreter.IntrinsicX86.fromUInt {S P : Type} (value : Nat) (size : ABI.Size) : M S (Memory.Scalar P)

Equations

• Miri.Interpreter.IntrinsicX86.fromUInt value size = Miri.Interpreter.IntrinsicX86.scalarResult (Miri.Memory.Scalar.fromUInt (BitVec.ofNat 128 value) size)

def Miri.Interpreter.IntrinsicX86.fromInt {S P : Type} (value : Int) (size : ABI.Size) : M S (Memory.Scalar P)

Equations

• Miri.Interpreter.IntrinsicX86.fromInt value size = Miri.Interpreter.IntrinsicX86.scalarResult (Miri.Memory.Scalar.fromInt value size)

def Miri.Interpreter.IntrinsicX86.truncInt {S P : Type} (value : Int) (size : ABI.Size) : M S (Memory.Scalar P)

Equations

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

def Miri.Interpreter.IntrinsicX86.makeImm {S P : Type} (value : Int) (layout : ABI.TyAndLayout MIR.TyId) : M S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.IntrinsicX86.castInt {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (value : RvalueImmTy P) (dest : ABI.TyAndLayout MIR.TyId) : M S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.IntrinsicX86.splitRead {P S C V : Type} (h : Hooks P S C V) (choice : C) (op : OpTy P) : M S (UInt64 × UInt64 × OpTy P)

Equations

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

def Miri.Interpreter.IntrinsicX86.splitWrite {P S C V : Type} (h : Hooks P S C V) (choice : C) (dest : V) : M S (UInt64 × UInt64 × V)

Equations

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

def Miri.Interpreter.IntrinsicX86.copyRest {P S C V : Type} (h : Hooks P S C V) (choice : C) (source : OpTy P) (dest : V) (n : UInt64) : M S Unit

Equations

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