From 898dd0b52d993c057f07e3d7d1834c4313ae3c9e Mon Sep 17 00:00:00 2001
From: Artem Agvanian <nartagva@amazon.com>
Date: Fri, 5 Jul 2024 15:29:02 -0700
Subject: [PATCH] Wrap `assert!(is_initialized(...))` into a separate function

---
 library/kani/src/mem.rs      | 25 +++++++++++--------------
 library/kani_core/src/mem.rs | 25 +++++++++++--------------
 2 files changed, 22 insertions(+), 28 deletions(-)

diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs
index f06bf36f7e38..201d027124d0 100644
--- a/library/kani/src/mem.rs
+++ b/library/kani/src/mem.rs
@@ -122,13 +122,7 @@ where
     // not make sense to use it inside assumption context.
     metadata.is_ptr_aligned(thin_ptr, Internal)
         && is_inbounds(&metadata, thin_ptr)
-        && {
-            crate::assert(
-                is_initialized(ptr, 1),
-                "Undefined Behavior: Reading from an uninitialized pointer",
-            );
-            true
-        }
+        && assert_is_initialized(ptr)
         && unsafe { has_valid_value(ptr) }
 }
 
@@ -159,13 +153,7 @@ where
     // Need to assert `is_initialized` because non-determinism is used under the hood, so it does
     // not make sense to use it inside assumption context.
     is_inbounds(&metadata, thin_ptr)
-        && {
-            crate::assert(
-                is_initialized(ptr, 1),
-                "Undefined Behavior: Reading from an uninitialized pointer",
-            );
-            true
-        }
+        && assert_is_initialized(ptr)
         && unsafe { has_valid_value(ptr) }
 }
 
@@ -316,6 +304,15 @@ pub fn is_initialized<T: ?Sized>(_ptr: *const T, _len: usize) -> bool {
     kani_intrinsic()
 }
 
+/// A helper to to assert `is_initialized` to use it as a part of other predicates.
+fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
+    crate::assert(
+        is_initialized(ptr, 1),
+        "Undefined Behavior: Reading from an uninitialized pointer",
+    );
+    true
+}
+
 /// Get the object ID of the given pointer.
 #[rustc_diagnostic_item = "KaniPointerObject"]
 #[inline(never)]
diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs
index e887e3f66642..de6c535be8dc 100644
--- a/library/kani_core/src/mem.rs
+++ b/library/kani_core/src/mem.rs
@@ -127,13 +127,7 @@ macro_rules! kani_mem {
             // does not make sense to use it inside assumption context.
             metadata.is_ptr_aligned(thin_ptr, Internal)
                 && is_inbounds(&metadata, thin_ptr)
-                && {
-                    assert!(
-                        is_initialized(ptr, 1),
-                        "Undefined Behavior: Reading from an uninitialized pointer",
-                    );
-                    true
-                }
+                && assert_is_initialized(ptr)
                 && unsafe { has_valid_value(ptr) }
         }
 
@@ -165,13 +159,7 @@ macro_rules! kani_mem {
             // Need to assert `is_initialized` because non-determinism is used under the hood, so it
             // does not make sense to use it inside assumption context.
             is_inbounds(&metadata, thin_ptr)
-                && {
-                    assert!(
-                        is_initialized(ptr, 1),
-                        "Undefined Behavior: Reading from an uninitialized pointer",
-                    );
-                    true
-                }
+                && assert_is_initialized(ptr)
                 && unsafe { has_valid_value(ptr) }
         }
 
@@ -322,6 +310,15 @@ macro_rules! kani_mem {
             kani_intrinsic()
         }
 
+        /// A helper to to assert `is_initialized` to use it as a part of other predicates.
+        fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
+            assert!(
+                is_initialized(ptr, 1),
+                "Undefined Behavior: Reading from an uninitialized pointer",
+            );
+            true
+        }
+
         /// Get the object ID of the given pointer.
         #[rustc_diagnostic_item = "KaniPointerObject"]
         #[inline(never)]