Skip to content

Add safety preconditions to std/src/alloc.rs #330

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Add safety preconditions to std/src/alloc.rs #330

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e503889
Add safety preconditions to std/src/alloc.rs
tautschnig Apr 18, 2025
d97b770
Fix format
tautschnig Apr 18, 2025
8fef60f
Add autoharness to run-kani script and use in CI
tautschnig Apr 18, 2025
0c569a7
Merge remote-tracking branch 'origin/main' into alloc-rs-contracts
tautschnig Apr 29, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .github/workflows/kani.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,7 @@ jobs:
- name: Run Kani Verification
run: |
scripts/run-kani.sh --run autoharness --kani-args \
--include-pattern alloc::__default_lib_allocator:: \
--include-pattern alloc::layout::Layout::from_size_align \
--include-pattern ascii::ascii_char::AsciiChar::from_u8 \
--include-pattern char::convert::from_u32_unchecked \
Expand Down
20 changes: 20 additions & 0 deletions library/std/src/alloc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,13 +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};

#[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.
///
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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<u8>, layout: Layout) {
if layout.size() != 0 {
Expand All @@ -221,6 +229,7 @@ unsafe impl Allocator for System {
}
}

#[requires(new_layout.size() >= old_layout.size())]
#[inline]
unsafe fn grow(
&self,
Expand All @@ -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,
Expand All @@ -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,
Expand Down Expand Up @@ -382,6 +393,11 @@ 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
Expand All @@ -393,6 +409,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
Expand All @@ -403,13 +420,15 @@ 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
// `GlobalAlloc::dealloc`.
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,
Expand All @@ -425,6 +444,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
Expand Down
Loading