Skip to content
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

Add safety preconditions to alloc/src/alloc.rs #118

Draft
wants to merge 12 commits into
base: main
Choose a base branch
from
+104 −0
Draft

Add safety preconditions to alloc/src/alloc.rs #118

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
9822a02
Add safety preconditions to alloc/src/alloc.rs
tautschnig Oct 17, 2024
80a8886
Add safety dependency to alloc and std crates
tautschnig Oct 17, 2024
f685389
Fix placement of use directives
tautschnig Oct 17, 2024
f529e5d
Fix placement of requires clause
tautschnig Oct 17, 2024
71061d3
fixup! Add safety dependency to alloc and std crates
tautschnig Oct 17, 2024
247d3be
Fix harnesses
tautschnig Oct 17, 2024
90fbc0e
Merge remote-tracking branch 'origin/main' into bedrock-library/alloc…
tautschnig Oct 17, 2024
f17509e
fixup! Add safety dependency to alloc and std crates
tautschnig Oct 17, 2024
cb4b650
Disable unsupported harnesses of trait contracts
tautschnig Oct 18, 2024
b1bad7a
Global::alloc_impl isn't unsafe, so we should only have post-conditions
tautschnig Oct 18, 2024
d28ca19
fixup! Disable unsupported harnesses of trait contracts
tautschnig Oct 18, 2024
d640ef6
Disable check_grow_impl as we cannot currently express the necessary …
tautschnig Oct 18, 2024
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 library/alloc/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ edition = "2021"
[dependencies]
core = { path = "../core" }
compiler_builtins = { version = "0.1.123", features = ['rustc-dep-of-std'] }
safety = { path = "../contracts/safety" }

[dev-dependencies]
rand = { version = "0.8.5", default-features = false, features = ["alloc"] }
Expand Down
100 changes: 100 additions & 0 deletions library/alloc/src/alloc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,11 @@ use core::hint;
#[cfg(not(test))]
use core::ptr::{self, NonNull};

use safety::{ensures,requires};
#[cfg(kani)]
#[unstable(feature="kani", issue="none")]
use core::kani;

#[cfg(test)]
mod tests;

Expand Down Expand Up @@ -173,6 +178,7 @@ pub unsafe fn alloc_zeroed(layout: Layout) -> *mut u8 {
#[cfg(not(test))]
impl Global {
#[inline]
#[ensures(|ret| layout.size() != 0 || ret.is_ok())]
fn alloc_impl(&self, layout: Layout, zeroed: bool) -> Result<NonNull<[u8]>, AllocError> {
match layout.size() {
0 => Ok(NonNull::slice_from_raw_parts(layout.dangling(), 0)),
Expand All @@ -186,6 +192,10 @@ impl Global {
}

// SAFETY: Same as `Allocator::grow`
#[requires(new_layout.size() >= old_layout.size())]
#[requires(old_layout.size() == 0 || old_layout.align() != 0)]
#[requires(new_layout.size() == 0 || new_layout.align() != 0)]
#[requires(ptr.as_ptr() as usize % old_layout.align() == 0)]
#[inline]
unsafe fn grow_impl(
&self,
Expand Down Expand Up @@ -247,6 +257,8 @@ unsafe impl Allocator for Global {
}

#[inline]
#[requires(layout.size() == 0 || layout.align() != 0)]
#[requires(ptr.as_ptr() as usize % layout.align() == 0)]
Comment on lines +260 to +261
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

don't we need to require that the pointer is actually allocated?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We actually need an even stronger precondition (and Kani correctly detects this via the grow_impl harness): we'd need to express that ptr either points to a ZST (that's doable) or is a valid heap allocation (I don't know how we could currently express this).

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We would need ghost state. 😄

unsafe fn deallocate(&self, ptr: NonNull<u8>, layout: Layout) {
if layout.size() != 0 {
// SAFETY: `layout` is non-zero in size,
Expand All @@ -256,6 +268,10 @@ unsafe impl Allocator for Global {
}

#[inline]
#[requires(new_layout.size() >= old_layout.size())]
#[requires(old_layout.size() == 0 || old_layout.align() != 0)]
#[requires(new_layout.size() == 0 || new_layout.align() != 0)]
#[requires(ptr.as_ptr() as usize % old_layout.align() == 0)]
unsafe fn grow(
&self,
ptr: NonNull<u8>,
Expand All @@ -267,6 +283,10 @@ unsafe impl Allocator for Global {
}

#[inline]
#[requires(new_layout.size() >= old_layout.size())]
#[requires(old_layout.size() == 0 || old_layout.align() != 0)]
#[requires(new_layout.size() == 0 || new_layout.align() != 0)]
#[requires(ptr.as_ptr() as usize % old_layout.align() == 0)]
unsafe fn grow_zeroed(
&self,
ptr: NonNull<u8>,
Expand All @@ -278,6 +298,10 @@ unsafe impl Allocator for Global {
}

#[inline]
#[requires(new_layout.size() <= old_layout.size())]
#[requires(old_layout.size() == 0 || old_layout.align() != 0)]
#[requires(new_layout.size() == 0 || new_layout.align() != 0)]
#[requires(ptr.as_ptr() as usize % old_layout.align() == 0)]
unsafe fn shrink(
&self,
ptr: NonNull<u8>,
Expand Down Expand Up @@ -423,3 +447,79 @@ pub mod __alloc_error_handler {
}
}
}

#[cfg(kani)]
#[unstable(feature="kani", issue="none")]
mod verify {
use super::*;

// fn alloc_impl(&self, layout: Layout, zeroed: bool) -> Result<NonNull<[u8]>, AllocError>
#[kani::proof_for_contract(Global::alloc_impl)]
pub fn check_alloc_impl() {
let _ = Global.alloc_impl(kani::any(), kani::any());
}

// TODO: Kani correctly detects that the precondition is too weak. We'd need a way to express
// that ptr either points to a ZST (we can do this), or else is heap-allocated (we cannot).
// // unsafe fn grow_impl(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout, zeroed: bool) -> Result<NonNull<[u8]>, AllocError>
// #[kani::proof_for_contract(Global::grow_impl)]
// pub fn check_grow_impl() {
// let raw_ptr = kani::any::<usize>() as *mut u8;
// unsafe {
// let n = NonNull::new_unchecked(raw_ptr);
// let _ = Global.grow_impl(n, kani::any(), kani::any(), kani::any());
// }
// }

// TODO: disabled as Kani does not currently support contracts on traits. See
// https://github.com/model-checking/kani/issues/1997
// // unsafe fn deallocate(&self, ptr: NonNull<u8>, layout: Layout)
// #[kani::proof_for_contract(Allocator::deallocate)]
// pub fn check_deallocate() {
// let obj : &dyn Allocator = &Global;
// let raw_ptr = kani::any::<usize>() as *mut u8;
// unsafe {
// let n = NonNull::new_unchecked(raw_ptr);
// let _ = obj.deallocate(n, kani::any());
// }
// }

// TODO: disabled as Kani does not currently support contracts on traits. See
// https://github.com/model-checking/kani/issues/1997
// // unsafe fn grow(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout) -> Result<NonNull<[u8]>, AllocError>
// #[kani::proof_for_contract(Allocator::grow)]
// pub fn check_grow() {
// let obj : &dyn Allocator = &Global;
// let raw_ptr = kani::any::<usize>() as *mut u8;
// unsafe {
// let n = NonNull::new_unchecked(raw_ptr);
// let _ = obj.grow(n, kani::any(), kani::any());
// }
// }

// TODO: disabled as Kani does not currently support contracts on traits. See
// https://github.com/model-checking/kani/issues/1997
// // unsafe fn grow_zeroed(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout) -> Result<NonNull<[u8]>, AllocError>
// #[kani::proof_for_contract(Allocator::grow_zeroed)]
// pub fn check_grow_zeroed() {
// let obj : &dyn Allocator = &Global;
// let raw_ptr = kani::any::<usize>() as *mut u8;
// unsafe {
// let n = NonNull::new_unchecked(raw_ptr);
// let _ = obj.grow_zeroed(n, kani::any(), kani::any());
// }
// }

// TODO: disabled as Kani does not currently support contracts on traits. See
// https://github.com/model-checking/kani/issues/1997
// // unsafe fn shrink(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout) -> Result<NonNull<[u8]>, AllocError>
// #[kani::proof_for_contract(Allocator::shrink)]
// pub fn check_shrink() {
// let obj : &dyn Allocator = &Global;
// let raw_ptr = kani::any::<usize>() as *mut u8;
// unsafe {
// let n = NonNull::new_unchecked(raw_ptr);
// let _ = obj.shrink(n, kani::any(), kani::any());
// }
// }
}
1 change: 1 addition & 0 deletions library/alloc/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@
//
// Library features:
// tidy-alphabetical-start
#![cfg_attr(kani, feature(kani))]
#![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))]
#![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))]
#![feature(alloc_layout_extra)]
Expand Down
1 change: 1 addition & 0 deletions library/std/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ hashbrown = { version = "0.14", default-features = false, features = [
std_detect = { path = "../stdarch/crates/std_detect", default-features = false, features = [
'rustc-dep-of-std',
] }
safety = { path = "../contracts/safety" }

# Dependencies of the `backtrace` crate
rustc-demangle = { version = "0.1.24", features = ['rustc-dep-of-std'] }
Expand Down
1 change: 1 addition & 0 deletions library/std/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -269,6 +269,7 @@
#![cfg_attr(any(windows, target_os = "uefi"), feature(round_char_boundary))]
#![cfg_attr(target_family = "wasm", feature(stdarch_wasm_atomic_wait))]
#![cfg_attr(target_arch = "wasm64", feature(simd_wasm64))]
#![cfg_attr(kani, feature(kani))]
//
// Language features:
// tidy-alphabetical-start
Expand Down
Loading