Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support to simd_bitmask intrinsic #2131

Closed
Tracked by #2107
celinval opened this issue Jan 17, 2023 · 10 comments · Fixed by #2677
Closed
Tracked by #2107

Add support to simd_bitmask intrinsic #2131

celinval opened this issue Jan 17, 2023 · 10 comments · Fixed by #2677
Assignees
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct Z-Kani Compiler Issues that require some changes to the compiler

Comments

@celinval
Copy link
Contributor

Requested feature: Add support to simd_bitmask intrinsic
Use case: This intrinsic is commonly found during the code generation of the top 100 crates. Harnesses that exercise this intrinsic will fail due to unimplemented feature.
Link to relevant documentation (Rust reference, Nomicon, RFC):

@celinval celinval added [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct Z-Kani Compiler Issues that require some changes to the compiler labels Jan 17, 2023
@tautschnig tautschnig removed their assignment Mar 1, 2023
@celinval
Copy link
Contributor Author

celinval commented Mar 1, 2023

Here is the definition from the intrinsics documentation:

    // truncate integer vector to bitmask
    // `fn simd_bitmask(vector) -> unsigned integer` takes a vector of integers and
    // returns either an unsigned integer or array of `u8`.
    // Every element in the vector becomes a single bit in the returned bitmask.
    // If the vector has less than 8 lanes, a u8 is returned with zeroed trailing bits.
    // The bit order of the result depends on the byte endianness. LSB-first for little
    // endian and MSB-first for big endian.
    //
    // UB if called on a vector with values other than 0 and -1.

From the actual Masks specification, the integer to mask operation is documented as:

Converts a vector of integers to a mask, where 0 represents false and -1 represents true.
Safety

All lanes must be either 0 or -1.

@tautschnig
Copy link
Member

Given this specification I believe that Kani should generate a "concatenation" expression where each operand will be an "if" with a condition of "lane notequal 0" and "1" and "0" as the two cases. (I still don't understand under which condition an array is to be produced as result.)

@celinval
Copy link
Contributor Author

celinval commented Jun 6, 2023

The array will be produced if the input vector has more than 128 lanes. You basically need one bit per lane.

@celinval
Copy link
Contributor Author

celinval commented Jun 6, 2023

Kani can do this, but it will be inefficient. CBMC can probably encode operations that result in a single bit, while Kani will have to generate the results for each lane first, then join them in different bytes.

@celinval celinval self-assigned this Jun 14, 2023
@celinval
Copy link
Contributor Author

This intrinsic seems to be used by string comparison and hash map / hash set functions such as insert.

@celinval
Copy link
Contributor Author

celinval commented Jul 6, 2023

After talking to @remi-delmas-3000, we decided to implement this on the Kani side since CBMC modeling happens before bitblasting. So we would still need to do this operation byte-wise.

@celinval
Copy link
Contributor Author

celinval commented Jul 7, 2023

I created a basic Rust implementation of simd_bitmask that we could potentially use as a stub for this. However, I bumped into an issue while trying to transmute a SIMD structure. I created rust-lang/rust#113465 to capture the issue.

It's not clear if this issue will affect the verification use flow since we will hook the implementation inside the kani-compiler. However, it would be really nice to be able to add tests to the library implementation itself.

@celinval
Copy link
Contributor Author

celinval commented Jul 8, 2023

This work is also blocked by #2590

@workingjubilee
Copy link
Contributor

You can't just use tuple access. You instead have to replicate our insane pattern for a legal read of a Simd type, sorry:

    /// Converts a SIMD vector to an array.
    #[inline]
    pub const fn to_array(self) -> [T; N] {
        let mut tmp = core::mem::MaybeUninit::uninit();
        // SAFETY: writing to `tmp` is safe and initializes it.
        //
        // FIXME: We currently use a pointer store instead of `transmute_copy` because `repr(simd)`
        // results in padding for non-power-of-2 vectors (so vectors are larger than arrays).
        //
        // NOTE: This deliberately doesn't just use `self.0`, see the comment
        // on the struct definition for details.
        unsafe {
            self.store(tmp.as_mut_ptr());
            tmp.assume_init()
        }
    }

@celinval celinval moved this to In Progress in Kani 2023-07-10 Jul 10, 2023
@celinval
Copy link
Contributor Author

Thanks @workingjubilee ! I think rust-lang/portable-simd#339 also has another workaround that seems to work:

https://github.com/rust-lang/portable-simd/blob/7c7dbe0c505ccbc02ff30c1e37381ab1d47bf46f/crates/core_simd/src/vector.rs#L162-L170

    pub const fn as_array(&self) -> &[T; N] {
        // SAFETY: `Simd<T, N>` is just an overaligned `[T; N]` with
        // potential padding at the end, so pointer casting to a
        // `&[T; N]` is safe.
        //
        // NOTE: This deliberately doesn't just use `&self.0`, see the comment
        // on the struct definition for details.
        unsafe { &*(self as *const Self as *const [T; N]) }
    }

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct Z-Kani Compiler Issues that require some changes to the compiler
Projects
No open projects
Status: No status
Status: In Progress
Status: In Progress
Status: No status
Development

Successfully merging a pull request may close this issue.

3 participants