Audit for ptr_guaranteed_<cmp> (rust-lang#1090)

* Audit for `ptr_guaranteed_<cmp>`

* Update docs

* Add two tests

Author: adpaco-aws

docs/src/rust-feature-support.md

@@ -381,8 +381,8 @@ prefetch_read_data | No | |
 prefetch_read_instruction | No | |
 prefetch_write_data | No | |
 prefetch_write_instruction | No | |
-ptr_guaranteed_eq | Partial | |
-ptr_guaranteed_ne | Partial | |
+ptr_guaranteed_eq | Yes | |
+ptr_guaranteed_ne | Yes | |
 ptr_offset_from | Partial | Missing undefined behavior checks |
 raw_eq | Partial | Cannot detect [uninitialized memory](#uninitialized-memory) |
 rintf32 | No | |

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

@@ -246,8 +246,10 @@ impl<'tcx> GotocCtx<'tcx> {
             ($f:ident) => {{ codegen_intrinsic_binop!($f) }};
         }
 
-        // Intrinsics which encode a simple binary operation
-        macro_rules! codegen_intrinsic_boolean_binop {
+        // Intrinsics which encode a pointer comparison (e.g., `ptr_guaranteed_eq`).
+        // These behave as regular pointer comparison at runtime:
+        // https://doc.rust-lang.org/beta/std/primitive.pointer.html#method.guaranteed_eq
+        macro_rules! codegen_ptr_guaranteed_cmp {
             ($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b).cast_to(Type::c_bool())) }};
         }
 
@@ -519,8 +521,8 @@ impl<'tcx> GotocCtx<'tcx> {
             "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)),
             "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)),
             "pref_align_of" => codegen_intrinsic_const!(),
-            "ptr_guaranteed_eq" => codegen_intrinsic_boolean_binop!(eq),
-            "ptr_guaranteed_ne" => codegen_intrinsic_boolean_binop!(neq),
+            "ptr_guaranteed_eq" => codegen_ptr_guaranteed_cmp!(eq),
+            "ptr_guaranteed_ne" => codegen_ptr_guaranteed_cmp!(neq),
             "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc),
             "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc),
             "rintf32" => codegen_unimplemented_intrinsic!(

tests/kani/Intrinsics/PtrGuaranteedCmp/eq.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `ptr_guaranteed_eq` returns true if the pointers are equal, false
+// otherwise.
+#![feature(core_intrinsics)]
+use std::intrinsics::ptr_guaranteed_eq;
+
+#[kani::proof]
+fn test_ptr_eq_eq(ptr1: *const u8, ptr2: *const u8) {
+    kani::assume(ptr1 == ptr2);
+    assert!(ptr_guaranteed_eq(ptr1, ptr2));
+}
+
+#[kani::proof]
+fn test_ptr_eq_ne(ptr1: *const u8, ptr2: *const u8) {
+    kani::assume(ptr1 != ptr2);
+    assert!(!ptr_guaranteed_eq(ptr1, ptr2));
+}

tests/kani/Intrinsics/PtrGuaranteedCmp/ne.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `ptr_guaranteed_ne` returns true if the pointers are different,
+// false otherwise.
+#![feature(core_intrinsics)]
+use std::intrinsics::ptr_guaranteed_ne;
+
+#[kani::proof]
+fn test_ptr_ne_ne(ptr1: *const u8, ptr2: *const u8) {
+    kani::assume(ptr1 != ptr2);
+    assert!(ptr_guaranteed_ne(ptr1, ptr2));
+}
+
+#[kani::proof]
+fn test_ptr_ne_eq(ptr1: *const u8, ptr2: *const u8) {
+    kani::assume(ptr1 == ptr2);
+    assert!(!ptr_guaranteed_ne(ptr1, ptr2));
+}