Derive Arbitrary for various core_arch::x86 types (#348)

This enables autoharness to generate an additional 4067 harnesses (and
successfully prove 363 of them).

Using a patch instead of directly modifying the source code here for
`library/stdarch` is a git submodule. Modifying the source code directly
would require forking that other repository, tweaking our submodule
pointer, and thereby causing additional challenges for our fork update
automation.

The long-term solution should be automated derive-arbitrary support in
autoharness.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

.github/workflows/goto-transcoder.yml

@@ -27,6 +27,8 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: true
+      - name: Apply stdarch patch
+        run: cd library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Generate contracts programs
       - name: Generate contracts

.github/workflows/kani-metrics.yml

@@ -18,7 +18,9 @@ jobs:
       uses: actions/checkout@v4
       with:
         submodules: true
-    
+    - name: Apply stdarch patch
+      run: cd library/stdarch && patch -p1 < ../../stdarch.patch
+
     # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
     - name: Set up Python
       uses: actions/setup-python@v4

.github/workflows/kani.yml

@@ -43,7 +43,9 @@ jobs:
         with:
           path: head
           submodules: true
-      
+      - name: Apply stdarch patch
+        run: cd head/library/stdarch && patch -p1 < ../../stdarch.patch
+
       # Step 2: Install jq
       - name: Install jq
         if: matrix.os == 'ubuntu-latest'
@@ -72,6 +74,8 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: true
+      - name: Apply stdarch patch
+        run: cd library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Run Kani autoharness on the std library for selected functions.
       # Uses "--include-pattern" to make sure we do not try to run across all
@@ -82,6 +86,8 @@ jobs:
       # - We use >::disjoint_bitor (and >::unchecked_disjoint_bitor) as pattern
       #   as whitespace is not supported, cf.
       #   https://github.com/model-checking/kani/issues/4046
+      # - core_arch::x86::__m128d::as_f64x2 is just one example of hundreds of
+      #   core_arch::x86:: functions that are known to verify successfully.
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
@@ -91,6 +97,7 @@ jobs:
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
+            --include-pattern core_arch::x86::__m128d::as_f64x2 \
             --include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
             --include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
             --include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
@@ -257,6 +264,8 @@ jobs:
         with:
           path: head
           submodules: true
+      - name: Apply stdarch patch
+        run: cd head/library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Run list on the std library
       - name: Run Kani List
@@ -289,6 +298,8 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: true
+      - name: Apply stdarch patch
+        run: cd library/stdarch && patch -p1 < ../../stdarch.patch
 
       # Step 2: Run autoharness analyzer on the std library
       - name: Run Autoharness Analyzer

stdarch.patch

@@ -0,0 +1,51 @@
+--- a/crates/core_arch/src/aarch64/neon/mod.rs
++++ b/crates/core_arch/src/aarch64/neon/mod.rs
+@@ -2,6 +2,9 @@
+ 
+ #![allow(non_camel_case_types)]
+ 
++#[cfg(kani)]
++use crate::kani;
++
+ #[rustfmt::skip]
+ mod generated;
+ #[rustfmt::skip]
+--- a/crates/core_arch/src/arm_shared/neon/mod.rs
++++ b/crates/core_arch/src/arm_shared/neon/mod.rs
+@@ -1,5 +1,8 @@
+ //! ARMv7 NEON intrinsics
+ 
++#[cfg(kani)]
++use crate::kani;
++
+ #[rustfmt::skip]
+ mod generated;
+ #[rustfmt::skip]
+--- a/crates/core_arch/src/macros.rs
++++ b/crates/core_arch/src/macros.rs
+@@ -128,6 +128,15 @@ macro_rules! types {
+             }
+         }
+ 
++        #[cfg(kani)]
++        $(#[$stability])+
++        impl kani::Arbitrary for $name {
++            fn any() -> Self {
++                let data: [$elem_type; $len] = kani::any();
++                Self { 0: data }
++            }
++        }
++
+         $(#[$stability])+
+         impl crate::fmt::Debug for $name {
+             #[inline]
+--- a/crates/core_arch/src/x86/mod.rs
++++ b/crates/core_arch/src/x86/mod.rs
+@@ -1,5 +1,7 @@
+ //! `x86` and `x86_64` intrinsics.
+ 
++#[cfg(kani)]
++use crate::kani;
+ use crate::mem::transmute;
+ 
+ #[macro_use]