Add simple ensures, requires, predicates

  - I also added one proof-of-concept harness to ensure Kani can verify
    it.

.github/workflows/kani.yml

@@ -52,5 +52,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
           

.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/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::requires(attr, item)
+}

library/contracts/safety/src/runtime.rs

@@ -0,0 +1,17 @@
+use proc_macro::{TokenStream};
+use quote::{quote, format_ident};
+use syn::{ItemFn, parse_macro_input};
+
+/// 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,23 @@ 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 {
+    pub fn can_dereference<T>(ptr: *const T) -> bool { true }
+    pub fn can_write<T>(ptr: *mut T) -> bool { true }
+
+    pub fn can_read_unaligned<T>(ptr: *const T) -> bool { true }
+
+    pub fn can_write_unaligned<T>(ptr: *mut T) -> bool {true}
+}
+
+#[cfg(kani)]
+mod predicates {
+    pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned};
+}