Documentation

Miri.ABI.WrappingRange

The inclusive wrapping ranges used by rustc_abi::WrappingRange.

Range endpoints are machine-width u128 values (BitVec 128 in Lean). Values are compared as unsigned integers except in noSignedWraparound, which applies the source Size.sign_extend interpretation. Operations which call a panicking Size helper propagate that failure explicitly.

source
structure Miri.ABI.WrappingRange :
Type
Instances For
    source
    def Miri.ABI.instDecidableEqWrappingRange.decEq (x✝ x✝¹ : WrappingRange) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Miri.ABI.instDecidableEqWrappingRange :
      DecidableEq WrappingRange
      Equations
      source
      def Miri.ABI.instReprWrappingRange.repr :
      WrappingRange → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance Miri.ABI.instReprWrappingRange :
        Repr WrappingRange
        Equations
        source
        inductive Miri.ABI.WrappingRangeError :
        Type
        Instances For
          source
          @[instance_reducible]
          instance Miri.ABI.instReprWrappingRangeError :
          Repr WrappingRangeError
          Equations
          source
          def Miri.ABI.instReprWrappingRangeError.repr :
          WrappingRangeError → Nat → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[instance_reducible]
            instance Miri.ABI.instDecidableEqWrappingRangeError :
            DecidableEq WrappingRangeError
            Equations
            source
            def Miri.ABI.instDecidableEqWrappingRangeError.decEq (x✝ x✝¹ : WrappingRangeError) :
            Decidable (x✝ = x✝¹)
            Equations
            Instances For
              source
              inductive Miri.ABI.WrapStatus :
              Type
              Instances For
                source
                @[instance_reducible]
                instance Miri.ABI.instDecidableEqWrapStatus :
                DecidableEq WrapStatus
                Equations
                source
                def Miri.ABI.instReprWrapStatus.repr :
                WrapStatus → Nat → Std.Format
                Equations
                Instances For
                  source
                  @[instance_reducible]
                  instance Miri.ABI.instReprWrapStatus :
                  Repr WrapStatus
                  Equations
                  source
                  @[inline]
                  def Miri.ABI.WrappingRange.full (size : Size) :
                  Except WrappingRangeError WrappingRange
                  Equations
                  Instances For
                    source
                    @[inline]
                    def Miri.ABI.WrappingRange.contains (range : WrappingRange) (value : U128) :
                    Bool
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[inline]
                      def Miri.ABI.WrappingRange.isFullFor (range : WrappingRange) (size : Size) :
                      Except WrappingRangeError Bool
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[inline]
                        def Miri.ABI.WrappingRange.containsRange (range other : WrappingRange) (size : Size) :
                        Except WrappingRangeError Bool
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[inline]
                          def Miri.ABI.WrappingRange.withStart (range : WrappingRange) (start : U128) :
                          WrappingRange
                          Equations
                          Instances For
                            source
                            @[inline]
                            def Miri.ABI.WrappingRange.withEnd (range : WrappingRange) (endValue : U128) :
                            WrappingRange
                            Equations
                            Instances For
                              source
                              @[inline]
                              def Miri.ABI.WrappingRange.noUnsignedWraparound (range : WrappingRange) (size : Size) :
                              Except WrappingRangeError WrapStatus
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                @[inline]
                                def Miri.ABI.WrappingRange.noSignedWraparound (range : WrappingRange) (size : Size) :
                                Except WrappingRangeError WrapStatus
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Match the upstream algorithm: use the obvious interval if it is no larger than any wraparound candidate; otherwise examine intervals between adjacent sorted values and keep the first minimum-width range.

                                  source
                                  def Miri.ABI.WrappingRange.smallestRangeContaining (values : List U128) (size : Size) :
                                  Except WrappingRangeError (Option WrappingRange)
                                  Equations
                                  Instances For