Add simple ensures, requires, safety predicates

.github/workflows/kani.yml

@@ -26,6 +26,11 @@ jobs:
       matrix:
         # Kani does not support windows.
         os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
     steps:
       - name: Checkout Library
         uses: actions/checkout@v4
@@ -41,6 +46,11 @@ jobs:
           path: kani
           ref: features/verify-rust-std
 
+      - name: Setup Dependencies
+        working-directory: kani
+        run: |
+          ./scripts/setup/${{ matrix.base }}/install_deps.sh
+
       - name: Build `Kani`
         working-directory: kani
         run: |
@@ -52,5 +62,6 @@ jobs:
         env:
           RUST_BACKTRACE: 1
         run: |
-          kani verify-std -Z unstable-options ./library --target-dir "target"
+          kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
+            -Z mem-predicates -Z ptr-to-ref-cast-checks
 

.github/workflows/rustc.yml

@@ -61,6 +61,9 @@ jobs:
 
       - name: Run tests
         working-directory: upstream
+        env:
+          # Avoid error due to unexpected `cfg`.
+          RUSTFLAGS: "--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))"
         run: |
           ./configure --set=llvm.download-ci-llvm=true
           ./x test --stage 0 library/std

.gitignore

@@ -26,6 +26,7 @@ Session.vim
 *.rlib
 *.rmeta
 *.mir
+Cargo.lock
 
 ## Temporary files
 *~

library/contracts/safety/Cargo.toml

@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[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"] }

library/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)");
+}

library/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()
+}

library/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)
+}

library/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
+}

library/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 }

library/core/src/lib.rs

@@ -431,6 +431,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.
 //

library/core/src/ptr/mod.rs

@@ -416,6 +416,8 @@ use crate::marker::FnPtr;
 use crate::ub_checks;
 
 use crate::mem::{self, align_of, size_of, MaybeUninit};
+#[cfg(kani)]
+use crate::kani;
 
 mod alignment;
 #[unstable(feature = "ptr_alignment_type", issue = "102070")]
@@ -1687,6 +1689,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 {
@@ -1766,6 +1769,8 @@ 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
+// What happens to the value that was replaced? No drop?
+#[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 {
@@ -2290,3 +2295,20 @@ 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);
+    }
+}
+

library/core/src/ub_checks.rs

@@ -160,3 +160,49 @@ 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 {
+    /// Check if a pointer can be dereferenced. I.e.:
+    ///   * `src` must be valid for reads. See [crate::ptr] documentation.
+    ///   * `src` must be properly aligned. Use read_unaligned if this is not the case.
+    ///   * `src` must point to a properly initialized value of type T.
+    ///
+    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
+    }
+
+    /// * `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};
+}