Update raw_eq documentation and tests (rust-lang#1091)

* Update `raw_eq` documentation

* Updates test and adds two more

* Comment from review

Author: adpaco-aws

docs/src/rust-feature-support.md

@@ -192,6 +192,16 @@ ensure there is no resource leak or persistent data inconsistency. Check out
 [this issue](https://github.com/model-checking/kani/issues/692) for updates on
 stack unwinding support.
 
+### Uninitialized memory
+
+Reading uninitialized memory is
+[considered undefined behavior](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#behavior-considered-undefined) in Rust.
+At the moment, Kani cannot detect if memory is uninitialized, but in practice
+this is mitigated by the fact that all memory is initialized with
+nondeterministic values.
+Therefore, any code that depends on uninitialized data will exhibit nondeterministic behavior.
+See [this issue](https://github.com/model-checking/kani/issues/920) for more details.
+
 ### Destructors
 
 At present, we are aware of some issues with destructors, in particular those
@@ -374,7 +384,7 @@ prefetch_write_instruction | No | |
 ptr_guaranteed_eq | Partial | |
 ptr_guaranteed_ne | Partial | |
 ptr_offset_from | Partial | Missing undefined behavior checks |
-raw_eq | Partial | Missing undefined behavior checks |
+raw_eq | Partial | Cannot detect [uninitialized memory](#uninitialized-memory) |
 rintf32 | No | |
 rintf64 | No | |
 rotate_left | Yes | |

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -933,13 +933,15 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     // `raw_eq` determines whether the raw bytes of two values are equal.
-    // https://stdrs.dev/nightly/x86_64-pc-windows-gnu/std/intrinsics/fn.raw_eq.html
+    // https://doc.rust-lang.org/core/intrinsics/fn.raw_eq.html
     //
     // The implementation below calls `memcmp` and returns equal if the result is zero.
     //
-    // TODO: Handle more cases in this intrinsic by looking into the parameters' layouts.
-    // TODO: Fix soundness issues in this intrinsic. It's UB to call `raw_eq` if any of
-    // the bytes in the first or second arguments are uninitialized.
+    // TODO: It's UB to call `raw_eq` if any of the bytes in the first or second
+    // arguments are uninitialized. At present, we cannot detect if there is
+    // uninitialized memory, but `raw_eq` would basically return a nondet. value
+    // when one of the arguments is uninitialized.
+    // https://github.com/model-checking/kani/issues/920
     fn codegen_intrinsic_raw_eq(
         &mut self,
         instance: Instance<'tcx>,

tests/kani/Intrinsics/raw_eq.rs renamed to tests/kani/Intrinsics/RawEq/main.rs

@@ -1,14 +1,12 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we get the expected results for the `raw_eq` intrinsic
 #![feature(core_intrinsics)]
-#![feature(const_intrinsic_raw_eq)]
-#![deny(const_err)]
+use std::intrinsics::raw_eq;
 
 #[kani::proof]
 fn main() {
-    // Check that we get the expected results for the `raw_eq` intrinsic
-    use std::intrinsics::raw_eq;
-
     let raw_eq_i32_true: bool = unsafe { raw_eq(&42_i32, &42) };
     assert!(raw_eq_i32_true);
 
@@ -24,6 +22,6 @@ fn main() {
     let raw_eq_array_true: bool = unsafe { raw_eq(&[13_u8, 42], &[13, 42]) };
     assert!(raw_eq_array_true);
 
-    const raw_eq_array_false: bool = unsafe { raw_eq(&[13_u8, 42], &[42, 13]) };
+    let raw_eq_array_false: bool = unsafe { raw_eq(&[13_u8, 42], &[42, 13]) };
     assert!(!raw_eq_array_false);
 }

tests/kani/Intrinsics/RawEq/uninit_eq.rs

@@ -0,0 +1,18 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Checks that `raw_eq` cannot determine equality when one of the arguments is
+// uninitialized
+#![feature(core_intrinsics)]
+use std::intrinsics::raw_eq;
+use std::mem::{zeroed, MaybeUninit};
+
+#[kani::proof]
+fn main() {
+    let zeroed_arr: [u8; 8] = unsafe { zeroed() };
+    let uninit_arr: [u8; 8] = unsafe { MaybeUninit::uninit().assume_init() };
+
+    let arr_are_eq = unsafe { raw_eq(&zeroed_arr, &uninit_arr) };
+    assert!(arr_are_eq);
+}

tests/kani/Intrinsics/RawEq/uninit_ne.rs

@@ -0,0 +1,18 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Checks that `raw_eq` cannot determine inequality when one of the arguments
+// is uninitialized
+#![feature(core_intrinsics)]
+use std::intrinsics::raw_eq;
+use std::mem::{zeroed, MaybeUninit};
+
+#[kani::proof]
+fn main() {
+    let zeroed_arr: [u8; 8] = unsafe { zeroed() };
+    let uninit_arr: [u8; 8] = unsafe { MaybeUninit::uninit().assume_init() };
+
+    let arr_are_eq = unsafe { raw_eq(&zeroed_arr, &uninit_arr) };
+    assert!(!arr_are_eq);
+}