Fix in erroneous implementation of _mm256_bsrli_epi128 #1823
Conversation
Fixing the issue mentioned in issue rust-lang#1822 of rust-lang/stdarch.
satiscugcat
changed the title
crates/core_arch/src/x86/avx2.rs
Outdated
| } | ||
|
|
||
| let r: i8x32 = match IMM8 % 16 { | ||
| let r: i8x32 = match IMM8 { |
There was a problem hiding this comment.
You have to also add a value to the default arm. It is currently unreachable_unchecked(), which makes IMM8 values > 15 UB.
Edit: Maybe you should change the IMM8 == 16 if above to be IMM8 >= 16? Also there is handling for IMM8 > 16 above already: (_mm256_setzero_si256(), a) which would become unreachable in that case.
There was a problem hiding this comment.
Oh right, I was mistaken. I think specifically values between 17-31 (inclusive) are UB without the %, which makes it not redundant. My mistake!
|
Did you try reverifying _mm256_alignr_epi8 with whatever tool you used to find the _mm256_bsrli_epi128 bug? And if so how did the |
The _mm256_bsrli_epi128 bug was found manually upon noticing a discrepancy in the intel specifications and the rust implementations in that case, and then testing it as it is tested in issue #1822 . Thus the other bug slipped past me too. My bad! |
satiscugcat
changed the title
|
Could you check pls if this bug is also there for |
Sure! We'll work on testing the variants from tomorrow. |
|
just checked, seems like the same bug is there for Actually, would you mind changing the impl of the |
I've made the appropriate changes. |
…fixing a bug in the process.
…mm_alignr_epi8 in ssse3.rs, also removed the import of the unreachable unchecked hint as it was no longer necessary
|
I don't understnd why the CI failed, running ci/run-docker.sh went through fine on my end. |
|
Ok, everything should be fine now. Let me know if there's anything else you think might need attention. |
Solution to challenge 15, resolves #173. This PR provides testable models for `core::arch` intrinsics, including abstractions to streamline the process of implementing these intrinsics and their tests. Currently there are 384 x86 intrinsics modelled, and 181 aarch64 intrinsics modelled. The methodology for writing the models is decribed in `testable-simd-models/README.md`. First, we model the SIMD types as bitvectors that can be converted to and from arrays of machine integers. Then, we model the raw operations on these types as functions over bitvectors, while keeping as much code as possible unchanged from the Rust code in `rust-lang/stdarch/crates/core_arch`. Finally, we write tests (using a generic macro) to compare the behaviour of our models with the corresponding intrinsic implementations in Rust core. Interestingly, in the process of modeling these intrinsivcs, we found bugs in the implementation of two intrinsics, `_mm256_bsrli_epi128` and `_mm512_bsrli_epi128`. These bugs were [fixed by our PR](rust-lang/stdarch#1823) in the 2025-06-30 version of the library. In a small way, this shows off the impact of writing testable models of the SIMD intrinsics. The model of intrinsics defined here is also used as the basis of formal proofs of Rust programs that use intrinsics. In particular, the `libcrux` cryptographic library uses these models in its [proofs of the post-quantum cryptographic algorithms](https://github.com/cryspen/libcrux/tree/main/fstar-helpers/core-models). As next steps, we intend to extend these testable models to a larger subset of core (beyond SIMD) and then translate these Rust models to models in F*, Rocq, and Lean, to enable proofs using our models in these backends. This work is being done as part of the [hax project](https://github.com/cryspen/hax). The work in this PR was primarily done by Aniket Mishra, under the supervision of Karthikeyan Bhargavan and Maxime Buyse at Cryspen. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: maximebuyse <[email protected]> Co-authored-by: Maxime Buyse <[email protected]>
5 participants
This fixes the error mentioned in issue #1822