Auto merge of #126608 - tgross35:f16-f128-library, r=Mark-Simulacrum · model-checking/verify-rust-std@a8b311e (original) (raw)

`@@ -489,6 +489,21 @@ impl f64 {

489

`#[stable(feature = "assoc_int_consts", since = "1.43.0")]

490

`pub const NEG_INFINITY: f64 = -1.0_f64 / 0.0_f64;

491

492

/// Sign bit

493

const SIGN_MASK: u64 = 0x8000_0000_0000_0000;

494

+

495

/// Exponent mask

496

const EXP_MASK: u64 = 0x7ff0_0000_0000_0000;

497

+

498

/// Mantissa mask

499

const MAN_MASK: u64 = 0x000f_ffff_ffff_ffff;

500

+

501

/// Minimum representable positive value (min subnormal)

502

const TINY_BITS: u64 = 0x1;

503

+

504

/// Minimum representable negative value (min negative subnormal)

505

const NEG_TINY_BITS: u64 = Self::TINY_BITS | Self::SIGN_MASK;

506

+

492

507

`` /// Returns true if this value is NaN.

493

508

`///

494

509

```` /// ```

````

`@@ -514,9 +529,7 @@ impl f64 {

514

529

`#[rustc_const_unstable(feature = "const_float_classify", issue = "72505")]

515

530

`pub(crate) const fn abs_private(self) -> f64 {

516

531

`// SAFETY: This transmutation is fine. Probably. For the reasons std is using it.

517

unsafe {

518

mem::transmute::<u64, f64>(mem::transmute::<f64, u64>(self) & 0x7fff_ffff_ffff_ffff)

519

}

532

unsafe { mem::transmute::<u64, f64>(mem::transmute::<f64, u64>(self) & !Self::SIGN_MASK) }

520

533

521

534

522

535

`` /// Returns true if this value is positive infinity or negative infinity, and

`@@ -673,13 +686,10 @@ impl f64 {

673

686

`// and some normal floating point numbers truncated from an x87 FPU.

674

687

`#[rustc_const_unstable(feature = "const_float_classify", issue = "72505")]

675

688

`const unsafe fn partial_classify(self) -> FpCategory {

676

const EXP_MASK: u64 = 0x7ff0000000000000;

677

const MAN_MASK: u64 = 0x000fffffffffffff;

678

-

679

689

`// SAFETY: The caller is not asking questions for which this will tell lies.

680

690

`let b = unsafe { mem::transmute::<f64, u64>(self) };

681

match (b & MAN_MASK, b & EXP_MASK) {

682

(0, EXP_MASK) => FpCategory::Infinite,

691

match (b & Self::MAN_MASK, b & Self::EXP_MASK) {

692

(0, Self::EXP_MASK) => FpCategory::Infinite,

683

693

`(0, 0) => FpCategory::Zero,

684

694

`(_, 0) => FpCategory::Subnormal,

685

695

` _ => FpCategory::Normal,

`@@ -691,12 +701,9 @@ impl f64 {

691

701

`// plus a transmute. We do not live in a just world, but we can make it more so.

692

702

`#[rustc_const_unstable(feature = "const_float_classify", issue = "72505")]

693

703

`const fn classify_bits(b: u64) -> FpCategory {

694

const EXP_MASK: u64 = 0x7ff0000000000000;

695

const MAN_MASK: u64 = 0x000fffffffffffff;

696

-

697

match (b & MAN_MASK, b & EXP_MASK) {

698

(0, EXP_MASK) => FpCategory::Infinite,

699

(_, EXP_MASK) => FpCategory::Nan,

704

match (b & Self::MAN_MASK, b & Self::EXP_MASK) {

705

(0, Self::EXP_MASK) => FpCategory::Infinite,

706

(_, Self::EXP_MASK) => FpCategory::Nan,

700

707

`(0, 0) => FpCategory::Zero,

701

708

`(_, 0) => FpCategory::Subnormal,

702

709

` _ => FpCategory::Normal,

`@@ -756,7 +763,7 @@ impl f64 {

756

763

`// IEEE754 says: isSignMinus(x) is true if and only if x has negative sign. isSignMinus

757

764

`// applies to zeros and NaNs as well.

758

765

`// SAFETY: This is just transmuting to get the sign bit, it's fine.

759

unsafe { mem::transmute::<f64, u64>(self) & 0x8000_0000_0000_0000 != 0 }

766

unsafe { mem::transmute::<f64, u64>(self) & Self::SIGN_MASK != 0 }

760

767

761

768

762

769

`#[must_use]

`@@ -797,19 +804,17 @@ impl f64 {

797

804

`#[unstable(feature = "float_next_up_down", issue = "91399")]

798

805

`#[rustc_const_unstable(feature = "float_next_up_down", issue = "91399")]

799

806

`pub const fn next_up(self) -> Self {

800

// We must use strictly integer arithmetic to prevent denormals from

801

// flushing to zero after an arithmetic operation on some platforms.

802

const TINY_BITS: u64 = 0x1; // Smallest positive f64.

803

const CLEAR_SIGN_MASK: u64 = 0x7fff_ffff_ffff_ffff;

804

-

807

// Some targets violate Rust's assumption of IEEE semantics, e.g. by flushing

808

// denormals to zero. This is in general unsound and unsupported, but here

809

// we do our best to still produce the correct result on such targets.

805

810

`let bits = self.to_bits();

806

811

`if self.is_nan() || bits == Self::INFINITY.to_bits() {

807

812

`return self;

808

813

809

814

810

let abs = bits & CLEAR_SIGN_MASK;

815

let abs = bits & !Self::SIGN_MASK;

811

816

`let next_bits = if abs == 0 {

812

TINY_BITS

817

Self::TINY_BITS

813

818

`} else if bits == abs {

814

819

` bits + 1

815

820

`} else {

`@@ -847,19 +852,17 @@ impl f64 {

847

852

`#[unstable(feature = "float_next_up_down", issue = "91399")]

848

853

`#[rustc_const_unstable(feature = "float_next_up_down", issue = "91399")]

849

854

`pub const fn next_down(self) -> Self {

850

// We must use strictly integer arithmetic to prevent denormals from

851

// flushing to zero after an arithmetic operation on some platforms.

852

const NEG_TINY_BITS: u64 = 0x8000_0000_0000_0001; // Smallest (in magnitude) negative f64.

853

const CLEAR_SIGN_MASK: u64 = 0x7fff_ffff_ffff_ffff;

854

-

855

// Some targets violate Rust's assumption of IEEE semantics, e.g. by flushing

856

// denormals to zero. This is in general unsound and unsupported, but here

857

// we do our best to still produce the correct result on such targets.

855

858

`let bits = self.to_bits();

856

859

`if self.is_nan() || bits == Self::NEG_INFINITY.to_bits() {

857

860

`return self;

858

861

859

862

860

let abs = bits & CLEAR_SIGN_MASK;

863

let abs = bits & !Self::SIGN_MASK;

861

864

`let next_bits = if abs == 0 {

862

NEG_TINY_BITS

865

Self::NEG_TINY_BITS

863

866

`} else if bits == abs {

864

867

` bits - 1

865

868

`} else {