Undo changes to stdarch

Author: Fedor Ryabinin

library/stdarch/crates/core_arch/src/x86/sse3.rs

@@ -1,14 +1,5 @@
 //! Streaming SIMD Extensions 3 (SSE3)
 
-#![feature(ub_checks)]
-use safety::{ensures,requires};
-#[cfg(kani)]
-#[unstable(feature="kani", issue="none")]
-use core::kani;
-#[allow(unused_imports)]
-#[unstable(feature = "ub_checks", issue = "none")]
-use core::ub_checks::*;
-
 use crate::core_arch::{simd::*, x86::*};
 use crate::intrinsics::simd::*;
 
@@ -108,7 +99,6 @@ pub fn _mm_hsub_ps(a: __m128, b: __m128) -> __m128 {
 #[target_feature(enable = "sse3")]
 #[cfg_attr(test, assert_instr(lddqu))]
 #[stable(feature = "simd_x86", since = "1.27.0")]
-#[requires(can_dereference(mem_addr))]
 pub unsafe fn _mm_lddqu_si128(mem_addr: *const __m128i) -> __m128i {
     transmute(lddqu(mem_addr as *const _))
 }
@@ -270,37 +260,3 @@ mod tests {
         assert_eq_m128d(r, _mm_setr_pd(d, d));
     }
 }
-#[cfg(kani)]
-mod verify {
-    use super::*;
-
-    #[cfg(kani)]
-    #[kani::proof_for_contract(unsafe fn _mm_lddqu_si128(mem_addr: *const __m128i) -> __m128i)]
-    fn proof_mm_lddqu_si128() {
-        // Create a valid __m128i value
-        let mut value = [0i32; 4];
-
-        // Get a pointer to the value
-        let ptr: *const __m128i = value.as_ptr() as *const __m128i;
-
-        // Call the function with the valid pointer
-        unsafe {
-            let _result = _mm_lddqu_si128(ptr);
-        }
-    }
-
-    #[cfg(kani)]
-    #[kani::proof_for_contract(unsafe fn _mm_loadddup_pd(mem_addr: *const f64) -> __m128d)]
-    fn proof_mm_loadddup_pd() {
-        // Create a valid f64 value
-        let value: f64 = 0.0;
-
-        // Get a pointer to the value
-        let ptr: *const f64 = &value;
-
-        // Call the function with the valid pointer
-        unsafe {
-            let _result = _mm_loadddup_pd(ptr);
-        }
-    }
-}

library/stdarch/crates/core_arch/src/x86/sse41.rs

@@ -1,14 +1,5 @@
 //! Streaming SIMD Extensions 4.1 (SSE4.1)
 
-#![feature(ub_checks)]
-use safety::{ensures,requires};
-#[cfg(kani)]
-#[unstable(feature="kani", issue="none")]
-use core::kani;
-#[allow(unused_imports)]
-#[unstable(feature = "ub_checks", issue = "none")]
-use core::ub_checks::*;
-
 use crate::core_arch::{simd::*, x86::*};
 use crate::intrinsics::simd::*;
 
@@ -1141,8 +1132,6 @@ pub fn _mm_test_mix_ones_zeros(a: __m128i, mask: __m128i) -> i32 {
 #[target_feature(enable = "sse4.1")]
 #[cfg_attr(test, assert_instr(movntdqa))]
 #[stable(feature = "simd_x86_updates", since = "1.82.0")]
-#[requires(can_dereference(mem_addr))]
-#[requires(mem_addr as usize % 16 == 0)]
 pub unsafe fn _mm_stream_load_si128(mem_addr: *const __m128i) -> __m128i {
     let dst: __m128i;
     crate::arch::asm!(
@@ -1950,26 +1939,3 @@ mod tests {
         assert_eq_m128i(a, r);
     }
 }
-#[cfg(kani)]
-mod verify {
-    use super::*;
-    #[cfg(kani)]
-    #[repr(align(16))]
-    struct Aligned16Bytes {
-        data: [u8; 16],
-    }
-
-    #[cfg(kani)]
-    #[kani::proof_for_contract(_mm_stream_load_si128)]
-    fn verify_mm_stream_load_si128() {
-        // Allocate memory for __m128i (16 bytes) with proper alignment
-        let mut aligned_data = Aligned16Bytes { data: [0u8; 16] };
-        let ptr = &aligned_data.data as *const _ as *const __m128i;
-
-        // Call the function with our properly aligned pointer
-        unsafe {
-            let _result = _mm_stream_load_si128(ptr);
-            // No postconditions to verify
-        }
-    }
-}