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.

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 contracts for Layout and Alignment #33

Merged
merged 2 commits into from
Jul 11, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
23 changes: 23 additions & 0 deletions library/core/src/alloc/layout.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,16 @@
// collections, resulting in having to optimize down excess IR multiple times.
// Your performance intuition is useless. Run perf.

use safety::requires;
use crate::cmp;
use crate::error::Error;
use crate::fmt;
use crate::mem;
use crate::ptr::{Alignment, NonNull};

#[cfg(kani)]
use crate::kani;

// While this function is used in one place and its implementation
// could be inlined, the previous attempts to do so made rustc
// slower:
Expand Down Expand Up @@ -117,6 +121,7 @@ impl Layout {
#[must_use]
#[inline]
#[rustc_allow_const_fn_unstable(ptr_alignment_type)]
#[requires(Layout::from_size_align(size, align).is_ok())]
pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
// SAFETY: the caller is required to uphold the preconditions.
unsafe { Layout { size, align: Alignment::new_unchecked(align) } }
Expand Down Expand Up @@ -492,3 +497,21 @@ impl fmt::Display for LayoutError {
f.write_str("invalid parameters to Layout::from_size_align")
}
}

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

#[kani::proof_for_contract(Layout::from_size_align_unchecked)]
pub fn check_from_size_align_unchecked() {
let s = kani::any::<usize>();
let a = kani::any::<usize>();

unsafe {
let layout = Layout::from_size_align_unchecked(s, a);
assert_eq!(layout.size(), s);
assert_eq!(layout.align(), a);
}
}
}
6 changes: 6 additions & 0 deletions library/core/src/ptr/alignment.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,12 @@
use safety::requires;
use crate::num::NonZero;
#[cfg(debug_assertions)]
use crate::ub_checks::assert_unsafe_precondition;
use crate::{cmp, fmt, hash, mem, num};

#[cfg(kani)]
use crate::kani;

/// A type storing a `usize` which is a power of two, and thus
/// represents a possible alignment in the Rust abstract machine.
///
Expand Down Expand Up @@ -76,6 +80,8 @@ impl Alignment {
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
#[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
#[inline]
#[requires(align > 0)]
tautschnig marked this conversation as resolved.
Show resolved Hide resolved
#[requires((align & (align - 1)) == 0)]
pub const unsafe fn new_unchecked(align: usize) -> Self {
#[cfg(debug_assertions)]
assert_unsafe_precondition!(
Expand Down
Loading