From a85b1189e8b0b469d3bc1684ea39d9f419178610 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 10:27:39 +0000 Subject: [PATCH 1/3] Derive `Arbitrary` for various `core_arch::x86` types 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. --- .github/workflows/goto-transcoder.yml | 2 ++ .github/workflows/kani-metrics.yml | 4 +++- .github/workflows/kani.yml | 14 +++++++++++- stdarch.patch | 32 +++++++++++++++++++++++++++ 4 files changed, 50 insertions(+), 2 deletions(-) create mode 100644 stdarch.patch 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 fd949f8eef552..3a7aff4f5bfc1 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 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..56a8ff6884f1c --- /dev/null +++ b/stdarch.patch @@ -0,0 +1,32 @@ +diff --git a/crates/core_arch/src/macros.rs b/crates/core_arch/src/macros.rs +index f59e278b..f3d33636 100644 +--- 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] +diff --git a/crates/core_arch/src/x86/mod.rs b/crates/core_arch/src/x86/mod.rs +index 0404b194..d57d1fc8 100644 +--- 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] From fda0919fd5c50d4b366b8f79d412e8904011383a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 10:51:38 +0000 Subject: [PATCH 2/3] Fix path, add macOS support --- .github/workflows/kani.yml | 2 +- stdarch.patch | 15 +++++++++++---- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 3a7aff4f5bfc1..7959a88c1f0e0 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -44,7 +44,7 @@ jobs: path: head submodules: true - name: Apply stdarch patch - run: cd library/stdarch && patch -p1 < ../../stdarch.patch + run: cd head/library/stdarch && patch -p1 < ../../stdarch.patch # Step 2: Install jq - name: Install jq diff --git a/stdarch.patch b/stdarch.patch index 56a8ff6884f1c..61b8e5925155c 100644 --- a/stdarch.patch +++ b/stdarch.patch @@ -1,5 +1,14 @@ -diff --git a/crates/core_arch/src/macros.rs b/crates/core_arch/src/macros.rs -index f59e278b..f3d33636 100644 +--- 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 { @@ -18,8 +27,6 @@ index f59e278b..f3d33636 100644 $(#[$stability])+ impl crate::fmt::Debug for $name { #[inline] -diff --git a/crates/core_arch/src/x86/mod.rs b/crates/core_arch/src/x86/mod.rs -index 0404b194..d57d1fc8 100644 --- a/crates/core_arch/src/x86/mod.rs +++ b/crates/core_arch/src/x86/mod.rs @@ -1,5 +1,7 @@ From 142ed502ac20d202761763a965ece76a9a58c09b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 11:04:18 +0000 Subject: [PATCH 3/3] Further ARM fix --- stdarch.patch | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/stdarch.patch b/stdarch.patch index 61b8e5925155c..341ff64fa9426 100644 --- a/stdarch.patch +++ b/stdarch.patch @@ -1,3 +1,15 @@ +--- 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 @@