From f7269e2bbc8ab812239a69a6a00a9ec2459c521d Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 11 Jun 2024 13:40:21 -0700
Subject: [PATCH 1/5] Add simple ensures, requires, predicates

  - I also added one proof-of-concept harness to ensure Kani can verify
    it.
---
 .github/workflows/kani.yml              |  3 ++-
 .gitignore                              |  1 +
 library/contracts/safety/Cargo.toml     | 17 +++++++++++++++++
 library/contracts/safety/src/kani.rs    | 21 +++++++++++++++++++++
 library/contracts/safety/src/lib.rs     | 25 +++++++++++++++++++++++++
 library/contracts/safety/src/runtime.rs | 17 +++++++++++++++++
 library/core/Cargo.toml                 |  3 +++
 library/core/src/lib.rs                 |  3 +++
 library/core/src/ptr/mod.rs             | 22 ++++++++++++++++++++++
 library/core/src/ub_checks.rs           | 20 ++++++++++++++++++++
 10 files changed, 131 insertions(+), 1 deletion(-)
 create mode 100644 library/contracts/safety/Cargo.toml
 create mode 100644 library/contracts/safety/src/kani.rs
 create mode 100644 library/contracts/safety/src/lib.rs
 create mode 100644 library/contracts/safety/src/runtime.rs

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 03365bd9cdbf1..68dabd130b86f 100644
--- a/.github/workflows/kani.yml
+++ b/.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
           
diff --git a/.gitignore b/.gitignore
index fa490af4c013e..f9fe675ebbe11 100644
--- a/.gitignore
+++ b/.gitignore
@@ -26,6 +26,7 @@ Session.vim
 *.rlib
 *.rmeta
 *.mir
+Cargo.lock
 
 ## Temporary files
 *~
diff --git a/library/contracts/safety/Cargo.toml b/library/contracts/safety/Cargo.toml
new file mode 100644
index 0000000000000..e51487e7266e9
--- /dev/null
+++ b/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"] }
diff --git a/library/contracts/safety/src/kani.rs b/library/contracts/safety/src/kani.rs
new file mode 100644
index 0000000000000..a8b4ab360dc8e
--- /dev/null
+++ b/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()
+}
diff --git a/library/contracts/safety/src/lib.rs b/library/contracts/safety/src/lib.rs
new file mode 100644
index 0000000000000..4b6f4528a56f1
--- /dev/null
+++ b/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)
+}
diff --git a/library/contracts/safety/src/runtime.rs b/library/contracts/safety/src/runtime.rs
new file mode 100644
index 0000000000000..f3f439ce726a6
--- /dev/null
+++ b/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
+}
diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml
index 0c2642341235b..e9fb39f19966c 100644
--- a/library/core/Cargo.toml
+++ b/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 }
diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs
index 206d1ab885291..7626d6d4a3cc8 100644
--- a/library/core/src/lib.rs
+++ b/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.
 //
diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index d2bbdc84d4dd1..a6706c389752d 100644
--- a/library/core/src/ptr/mod.rs
+++ b/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);
+    }
+}
+
diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs
index 1aa6a288e7082..e8404badda9fb 100644
--- a/library/core/src/ub_checks.rs
+++ b/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};
+}

From bfefeffe1661131500c832674d5054941d6b3419 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 11 Jun 2024 14:43:22 -0700
Subject: [PATCH 2/5] Install Kani's runtime dependencies and fix Rust CI

---
 .github/workflows/kani.yml              | 10 ++++++++++
 .github/workflows/rustc.yml             |  3 +++
 library/contracts/safety/src/runtime.rs |  4 +---
 3 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 68dabd130b86f..2b950b3e097b8 100644
--- a/.github/workflows/kani.yml
+++ b/.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: |
diff --git a/.github/workflows/rustc.yml b/.github/workflows/rustc.yml
index 2b8eb1a56dec8..f0f92d542b67d 100644
--- a/.github/workflows/rustc.yml
+++ b/.github/workflows/rustc.yml
@@ -61,6 +61,9 @@ jobs:
 
       - name: Run tests
         working-directory: upstream
+        env:
+          # Avoid error due to unexpected `cfg`
+          RUSTFLAGS: "-A unexpected_cfgs"
         run: |
           ./configure --set=llvm.download-ci-llvm=true
           ./x test --stage 0 library/std
diff --git a/library/contracts/safety/src/runtime.rs b/library/contracts/safety/src/runtime.rs
index f3f439ce726a6..78e8b1dc354d2 100644
--- a/library/contracts/safety/src/runtime.rs
+++ b/library/contracts/safety/src/runtime.rs
@@ -1,6 +1,4 @@
-use proc_macro::{TokenStream};
-use quote::{quote, format_ident};
-use syn::{ItemFn, parse_macro_input};
+use proc_macro::TokenStream;
 
 /// For now, runtime requires is a no-op.
 ///

From bced939434762b4487bcf2d473fe0e8ff21f0d87 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 11 Jun 2024 16:03:08 -0700
Subject: [PATCH 3/5] Try to remove host warnings and fix ensures

---
 library/contracts/safety/Cargo.toml | 4 ++++
 library/contracts/safety/src/lib.rs | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/library/contracts/safety/Cargo.toml b/library/contracts/safety/Cargo.toml
index e51487e7266e9..5e912e117224d 100644
--- a/library/contracts/safety/Cargo.toml
+++ b/library/contracts/safety/Cargo.toml
@@ -15,3 +15,7 @@ proc-macro2 = "1.0"
 proc-macro-error = "1.0.4"
 quote = "1.0.20"
 syn = { version = "2.0.18", features = ["full"] }
+
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani_host)'] }
\ No newline at end of file
diff --git a/library/contracts/safety/src/lib.rs b/library/contracts/safety/src/lib.rs
index 4b6f4528a56f1..9fe852a622de3 100644
--- a/library/contracts/safety/src/lib.rs
+++ b/library/contracts/safety/src/lib.rs
@@ -21,5 +21,5 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
 #[proc_macro_error]
 #[proc_macro_attribute]
 pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
-    tool::requires(attr, item)
+    tool::ensures(attr, item)
 }

From 250948010e4642868476ad94704d1996891cfe27 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 11 Jun 2024 16:58:53 -0700
Subject: [PATCH 4/5] Add comments and --check-cfg

---
 .github/workflows/rustc.yml         |  4 ++--
 library/contracts/safety/Cargo.toml |  4 ----
 library/contracts/safety/build.rs   |  4 ++++
 library/core/src/ub_checks.rs       | 34 +++++++++++++++++++++++++----
 4 files changed, 36 insertions(+), 10 deletions(-)
 create mode 100644 library/contracts/safety/build.rs

diff --git a/.github/workflows/rustc.yml b/.github/workflows/rustc.yml
index f0f92d542b67d..c971d223ff331 100644
--- a/.github/workflows/rustc.yml
+++ b/.github/workflows/rustc.yml
@@ -62,8 +62,8 @@ jobs:
       - name: Run tests
         working-directory: upstream
         env:
-          # Avoid error due to unexpected `cfg`
-          RUSTFLAGS: "-A unexpected_cfgs"
+          # 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
diff --git a/library/contracts/safety/Cargo.toml b/library/contracts/safety/Cargo.toml
index 5e912e117224d..e51487e7266e9 100644
--- a/library/contracts/safety/Cargo.toml
+++ b/library/contracts/safety/Cargo.toml
@@ -15,7 +15,3 @@ proc-macro2 = "1.0"
 proc-macro-error = "1.0.4"
 quote = "1.0.20"
 syn = { version = "2.0.18", features = ["full"] }
-
-
-[lints.rust]
-unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani_host)'] }
\ No newline at end of file
diff --git a/library/contracts/safety/build.rs b/library/contracts/safety/build.rs
new file mode 100644
index 0000000000000..32258fb328eec
--- /dev/null
+++ b/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)");
+}
\ No newline at end of file
diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs
index e8404badda9fb..a6e890023bfeb 100644
--- a/library/core/src/ub_checks.rs
+++ b/library/core/src/ub_checks.rs
@@ -168,12 +168,38 @@ pub use predicates::*;
 /// 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 }
+    /// 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
+    }
 
-    pub fn can_read_unaligned<T>(ptr: *const T) -> bool { 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
+    }
 
-    pub fn can_write_unaligned<T>(ptr: *mut T) -> bool {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)]

From c4b9c199c24c24a0ccb5093e69a47bb5d20337c5 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 11 Jun 2024 19:18:45 -0700
Subject: [PATCH 5/5] Apply suggestions from code review

Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
---
 library/contracts/safety/build.rs |  2 +-
 library/core/src/ptr/mod.rs       |  1 -
 library/core/src/ub_checks.rs     | 12 +++++++-----
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/library/contracts/safety/build.rs b/library/contracts/safety/build.rs
index 32258fb328eec..e74a4c9e57d6e 100644
--- a/library/contracts/safety/build.rs
+++ b/library/contracts/safety/build.rs
@@ -1,4 +1,4 @@
 fn main() {
     // We add the configurations here to be checked.
     println!("cargo:rustc-check-cfg=cfg(kani_host)");
-}
\ No newline at end of file
+}
diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index a6706c389752d..61d101c766f49 100644
--- a/library/core/src/ptr/mod.rs
+++ b/library/core/src/ptr/mod.rs
@@ -1769,7 +1769,6 @@ 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`.
diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs
index a6e890023bfeb..b864b63c5c661 100644
--- a/library/core/src/ub_checks.rs
+++ b/library/core/src/ub_checks.rs
@@ -168,11 +168,12 @@ pub use predicates::*;
 /// 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.
+    /// 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
@@ -180,7 +181,7 @@ mod predicates {
 
     /// 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
+    /// * `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;
@@ -195,6 +196,7 @@ mod predicates {
         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;