simd_bitmask intrinsic: add a non-power-of-2 multi-byte example · model-checking/verify-rust-std@3edb521 (original) (raw)

`@@ -463,7 +463,7 @@ extern "rust-intrinsic" {

463

`` /// T must be an integer vector.

464

`///

465

`` /// U must be either the smallest unsigned integer with at least as many bits as the length

466

`` -

/// of T, or the smallest array of u8 with as many bits as the length of T.

466

`` +

/// of T, or the smallest array of u8 with at least as many bits as the length of T.

467

`///

468

`/// Each element is truncated to a single bit and packed into the result.

469

`///

`@@ -475,12 +475,19 @@ extern "rust-intrinsic" {

475

`/// * On little endian, the least significant bit corresponds to the first vector element.

476

`/// * On big endian, the least significant bit corresponds to the last vector element.

477

`///

478

`` -

/// For example, [!0, 0, !0, !0] packs to 0b1101 on little endian and 0b1011 on big

479

/// endian.

478

`` +

/// For example, [!0, 0, !0, !0] packs to

479

`` +

/// - 0b1101u8 or [0b1101] on little endian, and

480

`` +

/// - 0b1011u8 or [0b1011] on big endian.

480

481

`///

481

`` -

/// To consider a larger example, [!0, 0, 0, 0, 0, 0, 0, 0, !0, !0, 0, 0, 0, 0, !0, 0] packs

482

`` -

/// to [0b00000001, 0b01000011] or 0b0100001100000001 on little endian, and `[0b10000000,

483

`` -

/// 0b11000010]or0b1000000011000010` on big endian.

482

/// To consider a larger example,

483

`` +

/// [!0, 0, 0, 0, 0, 0, 0, 0, !0, !0, 0, 0, 0, 0, !0, 0] packs to

484

`` +

/// - 0b0100001100000001u16 or [0b00000001, 0b01000011] on little endian, and

485

`` +

/// - 0b1000000011000010u16 or [0b10000000, 0b11000010] on big endian.

486

///

487

/// And finally, a non-power-of-2 example with multiple bytes:

488

`` +

/// [!0, !0, 0, !0, 0, 0, !0, 0, !0, 0] packs to

489

`` +

/// - 0b0101001011u16 or [0b01001011, 0b01] on little endian, and

490

`` +

/// - 0b1101001010u16 or [0b11, 0b01001010] on big endian.

484

491

`///

485

492

`/// # Safety

486

493

`` /// x must contain only 0 and !0.