Documentation

Miri.Interpreter.IntrinsicX86.Float

source
inductive Miri.Interpreter.IntrinsicX86.FloatBin :
Type
Instances For
    source
    def Miri.Interpreter.IntrinsicX86.cmpImm {P S C V : Type} (h : Hooks P S C V) (choice : C) (name : String) (imm : Int8) :
    M S FloatBin
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Miri.Interpreter.IntrinsicX86.readFloat {P S : Type} [Memory.PointerProvenance P] (value : Memory.Scalar P) (format : FloatFormat) :
      M S FloatBits
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Miri.Interpreter.IntrinsicX86.floatScalar {S P : Type} (value : FloatBits) :
        M S (Memory.Scalar P)
        Equations
        Instances For
          source
          def Miri.Interpreter.IntrinsicX86.floatBin {P S : Type} [Memory.PointerProvenance P] (format : FloatFormat) (op : FloatBin) (left right : RvalueImmTy P) :
          M S (Memory.Scalar P)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Miri.Interpreter.IntrinsicX86.floatBinary {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (format : FloatFormat) (op : FloatBin) (first : Bool) (left right : OpTy P) (dest : V) :
            M S Unit
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Miri.Interpreter.IntrinsicX86.relativeError {P S C V : Type} (h : Hooks P S C V) (choice : C) (value : FloatBits) :
              M S FloatBits

              Source relative-error arithmetic, with all legal RNG choices explicit.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Miri.Interpreter.IntrinsicX86.floatUnary {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (rsqrt first : Bool) (source : OpTy P) (dest : V) :
                M S Unit
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Miri.Interpreter.IntrinsicX86.roundingImm (value : Int32) :
                  Except StepError FloatIntegralRound
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Miri.Interpreter.IntrinsicX86.roundFloat {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (format : FloatFormat) (left : Option (OpTy P)) (source rounding : OpTy P) (dest : V) :
                    M S Unit
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Miri.Interpreter.IntrinsicX86.checkedFloatToInt {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (source : RvalueImmTy P) (dest : ABI.TyAndLayout MIR.TyId) (rounding : FloatIntegralRound) :
                      M S (RvalueImmTy P)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Miri.Interpreter.IntrinsicX86.convertFloatToInt {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (source : OpTy P) (rounding : FloatIntegralRound) (dest : V) :
                        M S Unit
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For