Squashed 'library/' changes from a2cf636..3e6b1c26cd5

3e6b1c26cd5 Merge commit 'cee9f0879743983a0924f94d37e0abd6d464bb4f' into sync-2024-07-20
496b81c004b Merge commit 'dd0d2657eb2c8466bbd9fa6ea4bf2b094565c680' into sync-2024-07-17
e3a5cb88602 Merge commit 'dd0d2657eb2c8466bbd9fa6ea4bf2b094565c680' into sync-2024-07-17
2f83451ef02 Reapply repository changes to library files
7b3d8ba5d15 Reapply repository changes to library files
c0a2240a2e7 Move contracts back to library/contracts
9d2c65282fd Move contracts back to library/contracts
586d10f1860 Merge commit '0cd155fda0d5b0b3ba666cd9df978d380f6c7067' as 'library'
9cab9f2bf44 Merge commit '0cd155fda0d5b0b3ba666cd9df978d380f6c7067' as 'library'
47a29de Delete library folder so we can recreate subtree
eea60ef Record library patch and delete library/
af85a10 Move contracts out of library for now
fd1c9c2 Add contracts for Layout and Alignment (#33)
5d8ee62 Add permissions needed to modify PR (#34)
bbfbb19 Add PR approval check for specific directories (#31)
5f2798e Add a challenge for `linked_list` (#30)
5a7327e Propose a new challenge about pointer arithmetic ops (#23)
c7dd281 Add committee application guideline and committee TOML file (#32)
df109da Add tracking issue for challenges template (#27)
52bea58 Remove copyright strings (#24)
e15993a Fix challenge numbers and move to challenges/ dir (#22)
ebb5c7f Add copyright file (#13)
df8da5a Add a few more contract and harness examples (#18)
5b70960 Run CI checks on all PRs against to main (#20)
a7c6d00 refined core transmutation challenge. (#11)
614eb77 Add simple ensures, requires, safety predicates (#15)
3a164b0 Add Challenge 2: Verify the memory safery of core intrinsics using raw pointers (#14)
8931064 Add Kani usage and verify-std section to verification book (#12)
5a369ec Add initial challenge template (#10)
b8464d4 Add Rust tests and Kani workflow (#9)
6f793b3 Update text and book
ec8c25c Fix text
4a6eb06 Add disclaimer, and fix links (#5)
dc3222b Fix the book script (#8)
c9653b7 Add copyright check file (#7)
05dca8f Add contest book (#6)
838f888 Adding std library as a subtree
6efb19b Merge commit '2faab3154fb126423ccf8e56c10577a3cd3f9457' as 'library'
2faab31 Squashed 'library/' content from commit f461edda8cb
104c14e Update README.md (#3)
7c30a94 Add README.md file (#2)
f24a233 Create initial commit with the license files

git-subtree-dir: library
git-subtree-split: 3e6b1c26cd58a676a339261c5e190fa29b903833

Author: jaisnan

contracts/safety/Cargo.toml

@@ -0,0 +1,14 @@
+[package]
+name = "safety"
+version = "0.1.0"
+edition = "2021"
+license = "MIT OR Apache-2.0"
+
+[lib]
+proc-macro = true
+
+[dependencies]
+proc-macro2 = "1.0"
+proc-macro-error = "1.0.4"
+quote = "1.0.20"
+syn = { version = "2.0.18", features = ["full"] }

contracts/safety/build.rs

@@ -0,0 +1,4 @@
+fn main() {
+    // We add the configurations here to be checked.
+    println!("cargo:rustc-check-cfg=cfg(kani_host)");
+}

contracts/safety/src/kani.rs

@@ -0,0 +1,21 @@
+use proc_macro::{TokenStream};
+use quote::{quote, format_ident};
+use syn::{ItemFn, parse_macro_input};
+
+pub(crate) fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
+    rewrite_attr(attr, item, "requires")
+}
+
+pub(crate) fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
+    rewrite_attr(attr, item, "ensures")
+}
+
+fn rewrite_attr(attr: TokenStream, item: TokenStream, name: &str) -> TokenStream {
+    let args = proc_macro2::TokenStream::from(attr);
+    let fn_item = parse_macro_input!(item as ItemFn);
+    let attribute = format_ident!("{}", name);
+    quote!(
+        #[kani_core::#attribute(#args)]
+        #fn_item
+    ).into()
+}

contracts/safety/src/lib.rs

@@ -0,0 +1,25 @@
+//! Implement a few placeholders for contract attributes until they get implemented upstream.
+//! Each tool should implement their own version in a separate module of this crate.
+
+use proc_macro::TokenStream;
+use proc_macro_error::proc_macro_error;
+
+#[cfg(kani_host)]
+#[path = "kani.rs"]
+mod tool;
+
+#[cfg(not(kani_host))]
+#[path = "runtime.rs"]
+mod tool;
+
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
+    tool::requires(attr, item)
+}
+
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
+    tool::ensures(attr, item)
+}

contracts/safety/src/runtime.rs

@@ -0,0 +1,15 @@
+use proc_macro::TokenStream;
+
+/// For now, runtime requires is a no-op.
+///
+/// TODO: At runtime the `requires` should become an assert unsafe precondition.
+pub(crate) fn requires(_attr: TokenStream, item: TokenStream) -> TokenStream {
+    item
+}
+
+/// For now, runtime requires is a no-op.
+///
+/// TODO: At runtime the `ensures` should become an assert as well.
+pub(crate) fn ensures(_attr: TokenStream, item: TokenStream) -> TokenStream {
+    item
+}

core/Cargo.toml

@@ -24,6 +24,9 @@ name = "corebenches"
 path = "benches/lib.rs"
 test = true
 
+[dependencies]
+safety = {path = "../contracts/safety" }
+
 [dev-dependencies]
 rand = { version = "0.8.5", default-features = false }
 rand_xorshift = { version = "0.3.0", default-features = false }

core/src/alloc/layout.rs

@@ -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:
@@ -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) } }
@@ -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);
+        }
+    }
+}

core/src/intrinsics.rs

@@ -63,11 +63,15 @@
 )]
 #![allow(missing_docs)]
 
+use safety::requires;
 use crate::marker::DiscriminantKind;
 use crate::marker::Tuple;
 use crate::ptr;
 use crate::ub_checks;
 
+#[cfg(kani)]
+use crate::kani;
+
 pub mod mir;
 pub mod simd;
 
@@ -2708,6 +2712,12 @@ pub const fn is_val_statically_known<T: Copy>(_arg: T) -> bool {
 #[rustc_intrinsic]
 // This has fallback `const fn` MIR, so shouldn't need stability, see #122652
 #[rustc_const_unstable(feature = "const_typed_swap", issue = "none")]
+#[cfg_attr(kani, kani::modifies(x))]
+#[cfg_attr(kani, kani::modifies(y))]
+#[requires(ub_checks::can_dereference(x) && ub_checks::can_write(x))]
+#[requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))]
+#[requires(x.addr() != y.addr() || core::mem::size_of::<T>() == 0)]
+#[requires((x.addr() >= y.addr() + core::mem::size_of::<T>()) || (y.addr() >= x.addr() + core::mem::size_of::<T>()))]
 pub const unsafe fn typed_swap<T>(x: *mut T, y: *mut T) {
     // SAFETY: The caller provided single non-overlapping items behind
     // pointers, so swapping them with `count: 1` is fine.
@@ -3154,3 +3164,37 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize
 
     const_eval_select((ptr, align), compiletime, runtime);
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use core::{cmp, fmt};
+    use super::*;
+    use crate::kani;
+
+    #[kani::proof_for_contract(typed_swap)]
+    pub fn check_typed_swap_u8() {
+        check_swap::<u8>()
+    }
+
+    #[kani::proof_for_contract(typed_swap)]
+    pub fn check_typed_swap_char() {
+        check_swap::<char>()
+    }
+
+    #[kani::proof_for_contract(typed_swap)]
+    pub fn check_typed_swap_non_zero() {
+        check_swap::<core::num::NonZeroI32>()
+    }
+
+    pub fn check_swap<T: kani::Arbitrary + Copy + cmp::PartialEq + fmt::Debug>() {
+        let mut x = kani::any::<T>();
+        let old_x = x;
+        let mut y = kani::any::<T>();
+        let old_y = y;
+
+        unsafe { typed_swap(&mut x, &mut y) };
+        assert_eq!(y, old_x);
+        assert_eq!(x, old_y);
+    }
+}

core/src/lib.rs

@@ -424,6 +424,9 @@ mod unit;
 #[stable(feature = "core_primitive", since = "1.43.0")]
 pub mod primitive;
 
+#[cfg(kani)]
+kani_core::kani_lib!(core);
+
 // Pull in the `core_arch` crate directly into core. The contents of
 // `core_arch` are in a different repository: rust-lang/stdarch.
 //

core/src/mem/mod.rs

@@ -13,6 +13,9 @@ use crate::intrinsics;
 use crate::marker::DiscriminantKind;
 use crate::ptr;
 
+#[cfg(kani)]
+use crate::kani;
+
 mod manually_drop;
 #[stable(feature = "manually_drop", since = "1.20.0")]
 pub use manually_drop::ManuallyDrop;
@@ -725,6 +728,8 @@ pub unsafe fn uninitialized<T>() -> T {
 #[stable(feature = "rust1", since = "1.0.0")]
 #[rustc_const_unstable(feature = "const_swap", issue = "83163")]
 #[rustc_diagnostic_item = "mem_swap"]
+#[cfg_attr(kani, crate::kani::modifies(x))]
+#[cfg_attr(kani, crate::kani::modifies(y))]
 pub const fn swap<T>(x: &mut T, y: &mut T) {
     // SAFETY: `&mut` guarantees these are typed readable and writable
     // as well as non-overlapping.
@@ -1359,3 +1364,38 @@ pub macro offset_of($Container:ty, $($fields:expr)+ $(,)?) {
     // The `{}` is for better error messages
     {builtin # offset_of($Container, $($fields)+)}
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    /// Use this type to ensure that mem swap does not drop the value.
+    #[derive(kani::Arbitrary)]
+    struct CannotDrop<T: kani::Arbitrary> {
+        inner: T,
+    }
+
+    impl<T: kani::Arbitrary> Drop for CannotDrop<T> {
+        fn drop(&mut self) {
+            unreachable!("Cannot drop")
+        }
+    }
+
+    #[kani::proof_for_contract(swap)]
+    pub fn check_swap_primitive() {
+        let mut x: u8 = kani::any();
+        let mut y: u8 = kani::any();
+        swap(&mut x, &mut y)
+    }
+
+    #[kani::proof_for_contract(swap)]
+    pub fn check_swap_adt_no_drop() {
+        let mut x: CannotDrop<char> = kani::any();
+        let mut y: CannotDrop<char> = kani::any();
+        swap(&mut x, &mut y);
+        forget(x);
+        forget(y);
+    }
+}

core/src/ptr/alignment.rs

@@ -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.
 ///
@@ -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)]
+    #[requires((align & (align - 1)) == 0)]
     pub const unsafe fn new_unchecked(align: usize) -> Self {
         #[cfg(debug_assertions)]
         assert_unsafe_precondition!(

core/src/ptr/mod.rs

@@ -415,7 +415,9 @@ use crate::intrinsics;
 use crate::marker::FnPtr;
 use crate::ub_checks;
 
-use crate::mem::{self, MaybeUninit};
+use crate::mem::{self, align_of, size_of, MaybeUninit};
+#[cfg(kani)]
+use crate::kani;
 
 mod alignment;
 #[unstable(feature = "ptr_alignment_type", issue = "102070")]
@@ -1692,6 +1694,7 @@ pub const unsafe fn write_unaligned<T>(dst: *mut T, src: T) {
 #[stable(feature = "volatile", since = "1.9.0")]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_diagnostic_item = "ptr_read_volatile"]
+#[safety::requires(ub_checks::can_dereference(src))]
 pub unsafe fn read_volatile<T>(src: *const T) -> T {
     // SAFETY: the caller must uphold the safety contract for `volatile_load`.
     unsafe {
@@ -1771,6 +1774,7 @@ pub unsafe fn read_volatile<T>(src: *const T) -> T {
 #[stable(feature = "volatile", since = "1.9.0")]
 #[rustc_diagnostic_item = "ptr_write_volatile"]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[safety::requires(ub_checks::can_write(dst))]
 pub unsafe fn write_volatile<T>(dst: *mut T, src: T) {
     // SAFETY: the caller must uphold the safety contract for `volatile_store`.
     unsafe {
@@ -2294,3 +2298,19 @@ pub macro addr_of($place:expr) {
 pub macro addr_of_mut($place:expr) {
     &raw mut $place
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use crate::fmt::Debug;
+    use super::*;
+    use crate::kani;
+
+    #[kani::proof_for_contract(read_volatile)]
+    pub fn check_read_u128() {
+        let val = kani::any::<u16>();
+        let ptr = &val as *const _;
+        let copy = unsafe { read_volatile(ptr) };
+        assert_eq!(val, copy);
+    }
+}

core/src/ub_checks.rs

@@ -160,3 +160,51 @@ pub(crate) const fn is_nonoverlapping(
     // This is just for safety checks so we can const_eval_select.
     const_eval_select((src, dst, size, count), comptime, runtime)
 }
+
+pub use predicates::*;
+
+/// Provide a few predicates to be used in safety contracts.
+///
+/// At runtime, they are no-op, and always return true.
+#[cfg(not(kani))]
+mod predicates {
+    /// Checks if a pointer can be dereferenced, ensuring:
+    ///   * `src` is valid for reads (see [`crate::ptr`] documentation).
+    ///   * `src` is properly aligned (use `read_unaligned` if not).
+    ///   * `src` points to a properly initialized value of type `T`.
+    ///
+    /// [`crate::ptr`]: https://doc.rust-lang.org/std/ptr/index.html
+    pub fn can_dereference<T>(src: *const T) -> bool {
+        let _ = src;
+        true
+    }
+
+    /// Check if a pointer can be written to:
+    /// * `dst` must be valid for writes.
+    /// * `dst` must be properly aligned. Use `write_unaligned` if this is not the
+    ///    case.
+    pub fn can_write<T>(dst: *mut T) -> bool {
+        let _ = dst;
+        true
+    }
+
+    /// Check if a pointer can be the target of unaligned reads.
+    /// * `src` must be valid for reads.
+    /// * `src` must point to a properly initialized value of type `T`.
+    pub fn can_read_unaligned<T>(src: *const T) -> bool {
+        let _ = src;
+        true
+    }
+
+    /// Check if a pointer can be the target of unaligned writes.
+    /// * `dst` must be valid for writes.
+    pub fn can_write_unaligned<T>(dst: *mut T) -> bool {
+        let _ = dst;
+        true
+    }
+}
+
+#[cfg(kani)]
+mod predicates {
+    pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned};
+}