Auto merge of #126171 - RalfJung:simd_bitmask_multibyte, r=workingjub… · model-checking/verify-rust-std@03d11c2 (original) (raw)

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

460

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

461

`///

462

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

463

`` -

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

463

`` +

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

464

`///

465

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

466

`///

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

472

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

473

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

474

`///

475

`` -

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

476

/// endian.

475

`` +

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

476

`` +

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

477

`` +

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

477

478

`///

478

`` -

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

479

`` -

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

480

`` -

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

479

/// To consider a larger example,

480

`` +

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

481

`` +

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

482

`` +

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

483

///

484

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

485

`` +

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

486

`` +

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

487

`` +

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

481

488

`///

482

489

`/// # Safety

483

490

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