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] 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)]