diff --git a/.github/workflows/goto-transcoder.yml b/.github/workflows/goto-transcoder.yml index 7272f2d657a0f..0d72ea82e2de9 100644 --- a/.github/workflows/goto-transcoder.yml +++ b/.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 diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml index 106ed3e160b4b..4595a7697b52f 100644 --- a/.github/workflows/kani-metrics.yml +++ b/.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 diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 79e556ff282b7..ffb0ff73d4bde 100644 --- a/.github/workflows/kani.yml +++ b/.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,18 +74,24 @@ 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 # possible functions as that may take a lot longer than expected. Instead, # explicitly list all functions (or prefixes thereof) the proofs of which # are known to pass. + # Notes: + # - 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 \ --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::::count_ones" \ --include-pattern "num::nonzero::NonZero::::count_ones" \ --include-pattern "num::nonzero::NonZero::::count_ones" \ @@ -136,6 +144,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 @@ -168,6 +178,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 diff --git a/stdarch.patch b/stdarch.patch new file mode 100644 index 0000000000000..341ff64fa9426 --- /dev/null +++ b/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]