Remove assigns clause for ZST pointers (#3417)

This PR filters out ZST pointee types when generating CMBC assigns
clauses for contracts. This prevents CMBC from complaining that the
pointer doesn't point to a valid allocation.

Resolves #3181

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: carolynzech

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

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::codegen_cprover_gotoc::{codegen::ty_stable::pointee_type_stable, GotocCtx};
 use crate::kani_middle::attributes::KaniAttributes;
 use cbmc::goto_program::FunctionContract;
 use cbmc::goto_program::{Expr, Lambda, Location, Type};
@@ -160,11 +160,17 @@ impl<'tcx> GotocCtx<'tcx> {
         let TyKind::RigidTy(RigidTy::Tuple(modifies_tys)) = modifies_ty.kind() else {
             unreachable!("found {:?}", modifies_ty.kind())
         };
+
+        for ty in &modifies_tys {
+            assert!(ty.kind().is_any_ptr(), "Expected pointer, but found {}", ty);
+        }
+
         let assigns: Vec<_> = modifies_tys
             .into_iter()
+            // do not attempt to dereference (and assign) a ZST
+            .filter(|ty| !self.is_zst_stable(pointee_type_stable(*ty).unwrap()))
             .enumerate()
             .map(|(idx, ty)| {
-                assert!(ty.kind().is_any_ptr(), "Expected pointer, but found {}", ty);
                 let ptr = modifies_args.clone().member(idx.to_string(), &self.symbol_table);
                 if self.is_fat_pointer_stable(ty) {
                     let unref = match ty.kind() {

tests/expected/function-contract/modifies/zst_pass.expected

@@ -0,0 +1,5 @@
+.assertion\
+- Status: SUCCESS\
+- Description: "ptr NULL or writable up to size"\
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/modifies/zst_pass.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::modifies(dst)]
+pub unsafe fn replace<T>(dst: *mut T, src: T) -> T {
+    std::ptr::replace(dst, src)
+}
+
+#[kani::proof_for_contract(replace)]
+pub fn check_replace_unit() {
+    check_replace_impl::<()>();
+}
+
+fn check_replace_impl<T: kani::Arbitrary + Eq + Clone>() {
+    let mut dst = T::any();
+    let orig = dst.clone();
+    let src = T::any();
+    let ret = unsafe { replace(&mut dst, src.clone()) };
+    assert_eq!(ret, orig);
+    assert_eq!(dst, src);
+}

tests/std-checks/core/mem.expected

@@ -1,7 +1,3 @@
 Checking harness mem::verify::check_swap_unit...
 
-Failed Checks: ptr NULL or writable up to size
-
-Summary:
-Verification failed for - mem::verify::check_swap_unit
-Complete - 6 successfully verified harnesses, 1 failures, 7 total.
+Complete - 7 successfully verified harnesses, 0 failures, 7 total.

tests/std-checks/core/ptr.expected

@@ -1,4 +1,3 @@
 Summary:
-Verification failed for - ptr::verify::check_replace_unit
 Verification failed for - ptr::verify::check_as_ref_dangling
-Complete - 4 successfully verified harnesses, 2 failures, 6 total.
+Complete - 5 successfully verified harnesses, 1 failures, 6 total.

tests/std-checks/core/src/mem.rs

@@ -48,8 +48,6 @@ mod verify {
         contracts::swap(&mut x, &mut y)
     }
 
-    /// FIX-ME: Modifies clause fail with pointer to ZST.
-    /// <https://github.com/model-checking/kani/issues/3181>
     #[kani::proof_for_contract(contracts::swap)]
     pub fn check_swap_unit() {
         let mut x: () = kani::any();

tests/std-checks/core/src/ptr.rs

@@ -89,8 +89,6 @@ mod verify {
         let _rf = unsafe { contracts::as_ref(&non_null) };
     }
 
-    /// FIX-ME: Modifies clause fail with pointer to ZST.
-    /// <https://github.com/model-checking/kani/issues/3181>
     #[kani::proof_for_contract(contracts::replace)]
     pub fn check_replace_unit() {
         check_replace_impl::<()>();