From e5038896f1bb18de099c53130944c3610950af68 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Apr 2025 14:47:46 +0000 Subject: [PATCH 1/3] Add safety preconditions to std/src/alloc.rs These contracts formalize the safety requirements that were previously only documented in comments. --- library/std/src/alloc.rs | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/library/std/src/alloc.rs b/library/std/src/alloc.rs index 5d2a304b41c5a..441a7632f5422 100644 --- a/library/std/src/alloc.rs +++ b/library/std/src/alloc.rs @@ -59,6 +59,9 @@ use core::ptr::NonNull; use core::sync::atomic::{AtomicPtr, Ordering}; use core::{hint, mem, ptr}; +#[cfg(kani)] +use core::kani; +use safety::requires; #[stable(feature = "alloc_module", since = "1.28.0")] #[doc(inline)] @@ -150,6 +153,10 @@ impl System { } // SAFETY: Same as `Allocator::grow` + #[requires(new_layout.size() >= old_layout.size())] + #[requires(ptr.as_ptr().is_aligned_to(old_layout.align()))] + #[requires(old_layout.size() == 0 || old_layout.align() != 0)] + #[requires(new_layout.size() == 0 || new_layout.align() != 0)] #[inline] unsafe fn grow_impl( &self, @@ -212,6 +219,7 @@ unsafe impl Allocator for System { self.alloc_impl(layout, true) } + #[requires(layout.size() != 0)] #[inline] unsafe fn deallocate(&self, ptr: NonNull, layout: Layout) { if layout.size() != 0 { @@ -221,6 +229,7 @@ unsafe impl Allocator for System { } } + #[requires(new_layout.size() >= old_layout.size())] #[inline] unsafe fn grow( &self, @@ -232,6 +241,7 @@ unsafe impl Allocator for System { unsafe { self.grow_impl(ptr, old_layout, new_layout, false) } } + #[requires(new_layout.size() >= old_layout.size())] #[inline] unsafe fn grow_zeroed( &self, @@ -243,6 +253,7 @@ unsafe impl Allocator for System { unsafe { self.grow_impl(ptr, old_layout, new_layout, true) } } + #[requires(new_layout.size() <= old_layout.size())] #[inline] unsafe fn shrink( &self, @@ -382,6 +393,10 @@ pub fn rust_oom(layout: Layout) -> ! { #[allow(unused_attributes)] #[unstable(feature = "alloc_internals", issue = "none")] pub mod __default_lib_allocator { + #[cfg(kani)] + use core::kani; + use safety::requires; + use super::{GlobalAlloc, Layout, System}; // These magic symbol names are used as a fallback for implementing the // `__rust_alloc` etc symbols (see `src/liballoc/alloc.rs`) when there is @@ -393,6 +408,7 @@ pub mod __default_lib_allocator { // linkage directives are provided as part of the current compiler allocator // ABI + #[requires(align.is_power_of_two())] #[rustc_std_internal_symbol] pub unsafe extern "C" fn __rdl_alloc(size: usize, align: usize) -> *mut u8 { // SAFETY: see the guarantees expected by `Layout::from_size_align` and @@ -403,6 +419,7 @@ pub mod __default_lib_allocator { } } + #[requires(align.is_power_of_two())] #[rustc_std_internal_symbol] pub unsafe extern "C" fn __rdl_dealloc(ptr: *mut u8, size: usize, align: usize) { // SAFETY: see the guarantees expected by `Layout::from_size_align` and @@ -410,6 +427,7 @@ pub mod __default_lib_allocator { unsafe { System.dealloc(ptr, Layout::from_size_align_unchecked(size, align)) } } + #[requires(align.is_power_of_two())] #[rustc_std_internal_symbol] pub unsafe extern "C" fn __rdl_realloc( ptr: *mut u8, @@ -425,6 +443,7 @@ pub mod __default_lib_allocator { } } + #[requires(align.is_power_of_two())] #[rustc_std_internal_symbol] pub unsafe extern "C" fn __rdl_alloc_zeroed(size: usize, align: usize) -> *mut u8 { // SAFETY: see the guarantees expected by `Layout::from_size_align` and From d97b7707aa4df8f77c35d9c81b7c8cac51606890 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Apr 2025 14:57:21 +0000 Subject: [PATCH 2/3] Fix format --- library/std/src/alloc.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/library/std/src/alloc.rs b/library/std/src/alloc.rs index 441a7632f5422..1e11a3329a3d6 100644 --- a/library/std/src/alloc.rs +++ b/library/std/src/alloc.rs @@ -56,16 +56,16 @@ #![deny(unsafe_op_in_unsafe_fn)] #![stable(feature = "alloc_module", since = "1.28.0")] +#[cfg(kani)] +use core::kani; use core::ptr::NonNull; use core::sync::atomic::{AtomicPtr, Ordering}; use core::{hint, mem, ptr}; -#[cfg(kani)] -use core::kani; -use safety::requires; #[stable(feature = "alloc_module", since = "1.28.0")] #[doc(inline)] pub use alloc_crate::alloc::*; +use safety::requires; /// The default memory allocator provided by the operating system. /// @@ -395,6 +395,7 @@ pub fn rust_oom(layout: Layout) -> ! { pub mod __default_lib_allocator { #[cfg(kani)] use core::kani; + use safety::requires; use super::{GlobalAlloc, Layout, System}; From 8fef60ff67660a838ac22e5a570fba4b1a84ae0a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Apr 2025 18:38:25 +0000 Subject: [PATCH 3/3] Add autoharness to run-kani script and use in CI --- .github/workflows/kani.yml | 27 +++++++++++++++++++++++++++ scripts/run-kani.sh | 9 +++++++++ 2 files changed, 36 insertions(+) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 90463ec8574c6..f8ff363f0feb9 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -53,6 +53,33 @@ jobs: - name: Run Kani Verification run: head/scripts/run-kani.sh --path ${{github.workspace}}/head + kani-autoharness: + name: Verify std library using autoharness + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest, macos-latest] + include: + - os: ubuntu-latest + base: ubuntu + - os: macos-latest + base: macos + fail-fast: false + + steps: + # Step 1: Check out the repository + - name: Checkout Repository + uses: actions/checkout@v4 + with: + submodules: true + + # Step 2: Run Kani on the std library for selected functions + - name: Run Kani Verification + run: | + scripts/run-kani.sh --kani-args \ + --include-pattern alloc::__default_lib_allocator:: \ + --jobs=3 --output-format=terse + run-kani-list: name: Kani List runs-on: ubuntu-latest diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 200bd957180d6..6bf815b8605db 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -297,6 +297,15 @@ main() { --enable-unstable \ --cbmc-args --object-bits 12 fi + elif [[ "$run_command" == "autoharness" ]]; then + # Run verification for all automatically generated harnesses (not in parallel) + echo "Running Kani autoharness command..." + "$kani_path" autoharness -Z autoharness -Z unstable-options --std ./library \ + $unstable_args \ + --no-assert-contracts \ + $command_args \ + --enable-unstable \ + --cbmc-args --object-bits 12 elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." "$kani_path" list -Z list $unstable_args ./library --std --format markdown