From d588c011c88b82bb1a3bee2d4a17a0be89d7ce19 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 12 Jun 2024 14:27:21 +0200
Subject: [PATCH] Fix typed_swap for ZSTs (#3256)

typed_swap needs to be a no-op on ZSTs as pointers to those have an
arbitrary value in Kani.

Resolves: #3182
---
 .../codegen/intrinsic.rs                      | 61 +++++++++++--------
 tests/kani/Intrinsics/typed_swap.rs           |  7 +++
 tests/std-checks/core/src/mem.rs              |  2 -
 3 files changed, 43 insertions(+), 27 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 4e965b4105ef..942c39203083 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -1880,12 +1880,11 @@ impl<'tcx> GotocCtx<'tcx> {
             "`dst` must be properly aligned",
             loc,
         );
-        let deref = dst.dereference();
-        if deref.typ().sizeof(&self.symbol_table) == 0 {
+        if self.is_zst_stable(pointee_type_stable(dst_typ).unwrap()) {
             // do not attempt to dereference (and assign) a ZST
             align_check
         } else {
-            let expr = deref.assign(src, loc);
+            let expr = dst.dereference().assign(src, loc);
             Stmt::block(vec![align_check, expr], loc)
         }
     }
@@ -1991,30 +1990,42 @@ impl<'tcx> GotocCtx<'tcx> {
         let x = fargs.remove(0);
         let y = fargs.remove(0);
 
-        // if(same_object(x, y)) {
-        //   assert(x + 1 <= y || y + 1 <= x);
-        //   assume(x + 1 <= y || y + 1 <= x);
-        // }
-        let one = Expr::int_constant(1, Type::c_int());
-        let non_overlapping =
-            x.clone().plus(one.clone()).le(y.clone()).or(y.clone().plus(one.clone()).le(x.clone()));
-        let non_overlapping_check = self.codegen_assert_assume(
-            non_overlapping,
-            PropertyClass::SafetyCheck,
-            "memory regions pointed to by `x` and `y` must not overlap",
-            loc,
-        );
-        let non_overlapping_stmt =
-            Stmt::if_then_else(x.clone().same_object(y.clone()), non_overlapping_check, None, loc);
+        if self.is_zst_stable(pointee_type_stable(farg_types[0]).unwrap()) {
+            // do not attempt to dereference (and assign) a ZST
+            Stmt::skip(loc)
+        } else {
+            // if(same_object(x, y)) {
+            //   assert(x + 1 <= y || y + 1 <= x);
+            //   assume(x + 1 <= y || y + 1 <= x);
+            // }
+            let one = Expr::int_constant(1, Type::c_int());
+            let non_overlapping = x
+                .clone()
+                .plus(one.clone())
+                .le(y.clone())
+                .or(y.clone().plus(one.clone()).le(x.clone()));
+            let non_overlapping_check = self.codegen_assert_assume(
+                non_overlapping,
+                PropertyClass::SafetyCheck,
+                "memory regions pointed to by `x` and `y` must not overlap",
+                loc,
+            );
+            let non_overlapping_stmt = Stmt::if_then_else(
+                x.clone().same_object(y.clone()),
+                non_overlapping_check,
+                None,
+                loc,
+            );
 
-        // T t = *y; *y = *x; *x = t;
-        let deref_y = y.clone().dereference();
-        let (temp_var, assign_to_t) =
-            self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc);
-        let assign_to_y = y.dereference().assign(x.clone().dereference(), loc);
-        let assign_to_x = x.dereference().assign(temp_var, loc);
+            // T t = *y; *y = *x; *x = t;
+            let deref_y = y.clone().dereference();
+            let (temp_var, assign_to_t) =
+                self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc);
+            let assign_to_y = y.dereference().assign(x.clone().dereference(), loc);
+            let assign_to_x = x.dereference().assign(temp_var, loc);
 
-        Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc)
+            Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc)
+        }
     }
 }
 
diff --git a/tests/kani/Intrinsics/typed_swap.rs b/tests/kani/Intrinsics/typed_swap.rs
index 4279bb713ece..996784b5181d 100644
--- a/tests/kani/Intrinsics/typed_swap.rs
+++ b/tests/kani/Intrinsics/typed_swap.rs
@@ -19,3 +19,10 @@ fn test_typed_swap_u32() {
     assert!(b == a_before);
     assert!(a == b_before);
 }
+
+#[kani::proof]
+pub fn check_swap_unit() {
+    let mut x: () = kani::any();
+    let mut y: () = kani::any();
+    std::mem::swap(&mut x, &mut y)
+}
diff --git a/tests/std-checks/core/src/mem.rs b/tests/std-checks/core/src/mem.rs
index 5ca439a18e1c..4f41d176a73a 100644
--- a/tests/std-checks/core/src/mem.rs
+++ b/tests/std-checks/core/src/mem.rs
@@ -45,8 +45,6 @@ mod verify {
 
     /// FIX-ME: Modifies clause fail with pointer to ZST.
     /// <https://github.com/model-checking/kani/issues/3181>
-    /// FIX-ME: `typed_swap` intrisic fails for ZST.
-    /// <https://github.com/model-checking/kani/issues/3182>
     #[kani::proof_for_contract(contracts::swap)]
     pub fn check_swap_unit() {
         let mut x: () = kani::any();