Extract repeated constants from `f32` and `f64` source · model-checking/verify-rust-std@6839ec5 (original) (raw)

`@@ -2,6 +2,45 @@ use crate::f32::consts;

2

`use crate::num::FpCategory as Fp;

3

`use crate::num::*;

4

5

/// Smallest number

6

#[allow(dead_code)] // unused on x86

7

const TINY_BITS: u32 = 0x1;

8

+

9

/// Next smallest number

10

#[allow(dead_code)] // unused on x86

11

const TINY_UP_BITS: u32 = 0x2;

12

+

13

/// Exponent = 0b11...10, Sifnificand 0b1111..10. Min val > 0

14

#[allow(dead_code)] // unused on x86

15

const MAX_DOWN_BITS: u32 = 0x7f7f_fffe;

16

+

17

/// Zeroed exponent, full significant

18

#[allow(dead_code)] // unused on x86

19

const LARGEST_SUBNORMAL_BITS: u32 = 0x007f_ffff;

20

+

21

/// Exponent = 0b1, zeroed significand

22

#[allow(dead_code)] // unused on x86

23

const SMALLEST_NORMAL_BITS: u32 = 0x0080_0000;

24

+

25

/// First pattern over the mantissa

26

#[allow(dead_code)] // unused on x86

27

const NAN_MASK1: u32 = 0x002a_aaaa;

28

+

29

/// Second pattern over the mantissa

30

#[allow(dead_code)] // unused on x86

31

const NAN_MASK2: u32 = 0x0055_5555;

32

+

33

#[allow(unused_macros)]

34

macro_rules! assert_f32_biteq {

35

($left : expr, $right : expr) => {

36

let l: &f32 = &$left;

37

let r: &f32 = &$right;

38

let lb = l.to_bits();

39

let rb = r.to_bits();

40

assert_eq!(lb, rb, "float {l} ({lb:#010x}) is not bitequal to {r} ({rb:#010x})");

41

};

42

}

43

+

5

44

`#[test]

6

45

`fn test_num_f32() {

7

46

`test_num(10f32, 2f32);

`@@ -315,27 +354,16 @@ fn test_is_sign_negative() {

315

354

`assert!((-f32::NAN).is_sign_negative());

316

355

317

356

318

#[allow(unused_macros)]

319

macro_rules! assert_f32_biteq {

320

($left : expr, $right : expr) => {

321

let l: &f32 = &$left;

322

let r: &f32 = &$right;

323

let lb = l.to_bits();

324

let rb = r.to_bits();

325

assert_eq!(lb, rb, "float {} ({:#x}) is not equal to {} ({:#x})", *l, lb, *r, rb);

326

};

327

}

328

-

329

357

`// Ignore test on x87 floating point, these platforms do not guarantee NaN

330

358

`// payloads are preserved and flush denormals to zero, failing the tests.

331

359

`#[cfg(not(target_arch = "x86"))]

332

360

`#[test]

333

361

`fn test_next_up() {

334

let tiny = f32::from_bits(1);

335

let tiny_up = f32::from_bits(2);

336

let max_down = f32::from_bits(0x7f7f_fffe);

337

let largest_subnormal = f32::from_bits(0x007f_ffff);

338

let smallest_normal = f32::from_bits(0x0080_0000);

362

let tiny = f32::from_bits(TINY_BITS);

363

let tiny_up = f32::from_bits(TINY_UP_BITS);

364

let max_down = f32::from_bits(MAX_DOWN_BITS);

365

let largest_subnormal = f32::from_bits(LARGEST_SUBNORMAL_BITS);

366

let smallest_normal = f32::from_bits(SMALLEST_NORMAL_BITS);

339

367

`assert_f32_biteq!(f32::NEG_INFINITY.next_up(), f32::MIN);

340

368

`assert_f32_biteq!(f32::MIN.next_up(), -max_down);

341

369

`assert_f32_biteq!((-1.0 - f32::EPSILON).next_up(), -1.0);

`@@ -352,8 +380,8 @@ fn test_next_up() {

352

380

353

381

`// Check that NaNs roundtrip.

354

382

`let nan0 = f32::NAN;

355

let nan1 = f32::from_bits(f32::NAN.to_bits() ^ 0x002a_aaaa);

356

let nan2 = f32::from_bits(f32::NAN.to_bits() ^ 0x0055_5555);

383

let nan1 = f32::from_bits(f32::NAN.to_bits() ^ NAN_MASK1);

384

let nan2 = f32::from_bits(f32::NAN.to_bits() ^ NAN_MASK2);

357

385

`assert_f32_biteq!(nan0.next_up(), nan0);

358

386

`assert_f32_biteq!(nan1.next_up(), nan1);

359

387

`assert_f32_biteq!(nan2.next_up(), nan2);

`@@ -364,11 +392,11 @@ fn test_next_up() {

364

392

`#[cfg(not(target_arch = "x86"))]

365

393

`#[test]

366

394

`fn test_next_down() {

367

let tiny = f32::from_bits(1);

368

let tiny_up = f32::from_bits(2);

369

let max_down = f32::from_bits(0x7f7f_fffe);

370

let largest_subnormal = f32::from_bits(0x007f_ffff);

371

let smallest_normal = f32::from_bits(0x0080_0000);

395

let tiny = f32::from_bits(TINY_BITS);

396

let tiny_up = f32::from_bits(TINY_UP_BITS);

397

let max_down = f32::from_bits(MAX_DOWN_BITS);

398

let largest_subnormal = f32::from_bits(LARGEST_SUBNORMAL_BITS);

399

let smallest_normal = f32::from_bits(SMALLEST_NORMAL_BITS);

372

400

`assert_f32_biteq!(f32::NEG_INFINITY.next_down(), f32::NEG_INFINITY);

373

401

`assert_f32_biteq!(f32::MIN.next_down(), f32::NEG_INFINITY);

374

402

`assert_f32_biteq!((-max_down).next_down(), f32::MIN);

`@@ -386,8 +414,8 @@ fn test_next_down() {

386

414

387

415

`// Check that NaNs roundtrip.

388

416

`let nan0 = f32::NAN;

389

let nan1 = f32::from_bits(f32::NAN.to_bits() ^ 0x002a_aaaa);

390

let nan2 = f32::from_bits(f32::NAN.to_bits() ^ 0x0055_5555);

417

let nan1 = f32::from_bits(f32::NAN.to_bits() ^ NAN_MASK1);

418

let nan2 = f32::from_bits(f32::NAN.to_bits() ^ NAN_MASK2);

391

419

`assert_f32_biteq!(nan0.next_down(), nan0);

392

420

`assert_f32_biteq!(nan1.next_down(), nan1);

393

421

`assert_f32_biteq!(nan2.next_down(), nan2);

`@@ -734,8 +762,8 @@ fn test_float_bits_conv() {

734

762

735

763

`// Check that NaNs roundtrip their bits regardless of signaling-ness

736

764

`// 0xA is 0b1010; 0x5 is 0b0101 -- so these two together clobbers all the mantissa bits

737

let masked_nan1 = f32::NAN.to_bits() ^ 0x002A_AAAA;

738

let masked_nan2 = f32::NAN.to_bits() ^ 0x0055_5555;

765

let masked_nan1 = f32::NAN.to_bits() ^ NAN_MASK1;

766

let masked_nan2 = f32::NAN.to_bits() ^ NAN_MASK2;

739

767

`assert!(f32::from_bits(masked_nan1).is_nan());

740

768

`assert!(f32::from_bits(masked_nan2).is_nan());

741

769

Extract repeated constants from f32 and f64 source · model-checking/verify-rust-std@6839ec5 (original) (raw)

Extract repeated constants from `f32` and `f64` source · model-checking/verify-rust-std@6839ec5 (original) (raw)