Handle CopyNonOverlapping statements from intrinsics code

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

@@ -467,7 +467,9 @@ impl<'tcx> GotocCtx<'tcx> {
             "ceilf64" => codegen_unimplemented_intrinsic!(
                 "https://github.com/model-checking/kani/issues/1025"
             ),
-            "copy" => self.codegen_copy_intrinsic(intrinsic, fargs, farg_types, p, loc),
+            "copy" => {
+                self.codegen_copy_intrinsic(intrinsic, false, fargs, farg_types, Some(p), loc)
+            }
             "copy_nonoverlapping" => unreachable!(
                 "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`"
             ),
@@ -897,21 +899,28 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::atomic_block(vec![skip_stmt], loc)
     }
 
-    /// An intrinsic that translates directly into `memmove`
+    /// An intrinsic that translates directly into `memmove` (for `copy`)
+    /// or `memcpy` (for `copy_nonoverlapping`)
     /// https://doc.rust-lang.org/core/intrinsics/fn.copy.html
+    /// https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html
     ///
     /// Undefined behavior if any of these conditions are violated:
     ///  * Both `src`/`dst` must be properly aligned (done by alignment checks)
     ///  * Both `src`/`dst` must be valid for reads/writes of `count *
     ///      size_of::<T>()` bytes (done by calls to `memmove`)
+    ///  * (Exclusive to `copy_nonoverlapping`) The region of memory beginning
+    ///      at `src` with a size of `count * size_of::<T>()` bytes must *not*
+    ///      overlap with the region of memory beginning at `dst` with the same
+    ///      size.
     /// In addition, we check that computing `count` in bytes (i.e., the third
-    /// argument for the `memmove` call) would not overflow.
-    fn codegen_copy_intrinsic(
+    /// argument of the copy built-in call) would not overflow.
+    pub fn codegen_copy_intrinsic(
         &mut self,
         intrinsic: &str,
+        is_non_overlapping: bool,
         mut fargs: Vec<Expr>,
         farg_types: &[Ty<'tcx>],
-        p: &Place<'tcx>,
+        p: Option<&Place<'tcx>>,
         loc: Location,
     ) -> Stmt {
         // The two first arguments are pointers. It's safe to cast them to void
@@ -941,18 +950,23 @@ impl<'tcx> GotocCtx<'tcx> {
         let (count_bytes, overflow_check) =
             self.count_in_bytes(count, pointee_type, Type::size_t(), intrinsic, loc);
 
-        // Build the call to `memmove`
-        let call_memmove =
-            BuiltinFn::Memmove.call(vec![dst.clone(), src, count_bytes.clone()], loc);
+        // Build the call to the copy built-in (`memmove` or `memcpy`)
+        let copy_builtin = if is_non_overlapping { BuiltinFn::Memcpy } else { BuiltinFn::Memmove };
+        let copy_call = copy_builtin.call(vec![dst.clone(), src, count_bytes.clone()], loc);
 
-        // The C implementation of `memmove` does not allow an invalid pointer for
-        // `src` nor `dst`, but the LLVM implementation specifies that a copy with
-        // length zero is a no-op. This comes up specifically when handling
-        // the empty string; CBMC will fail on passing a reference to empty
-        // string unless we codegen this zero check.
+        // The C implementations of `memmove` and `memcpy` do not allow an
+        // invalid pointer for `src` nor `dst`, but the LLVM implementations
+        // specify that a zero-length copy is a no-op:
         // https://llvm.org/docs/LangRef.html#llvm-memmove-intrinsic
-        let copy_if_nontrivial = count_bytes.is_zero().ternary(dst, call_memmove);
-        let copy_expr = self.codegen_expr_to_place(p, copy_if_nontrivial);
+        // https://llvm.org/docs/LangRef.html#llvm-memcpy-intrinsic
+        // This comes up specifically when handling the empty string; CBMC will
+        // fail on passing a reference to it unless we codegen this zero check.
+        let copy_if_nontrivial = count_bytes.is_zero().ternary(dst, copy_call);
+        let copy_expr = if p.is_some() {
+            self.codegen_expr_to_place(p.unwrap(), copy_if_nontrivial)
+        } else {
+            copy_if_nontrivial.as_stmt(loc)
+        };
         Stmt::block(vec![src_align_check, dst_align_check, overflow_check, copy_expr], loc)
     }
 

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

@@ -731,22 +731,25 @@ impl<'tcx> GotocCtx<'tcx> {
                 ref dst,
                 ref count,
             }) => {
-                let src = self.codegen_operand(src).cast_to(Type::void_pointer());
-                let dst = self.codegen_operand(dst);
-                let count = self.codegen_operand(count);
-                let sz = dst.typ().base_type().unwrap().sizeof(&self.symbol_table);
-                let sz = Expr::int_constant(sz, Type::size_t());
-                let n = sz.mul(count);
-                let dst = dst.cast_to(Type::void_pointer());
-                let e = BuiltinFn::Memcpy.call(vec![dst, src, n.clone()], location.clone());
-
-                // The C implementation of memcpy does not allow an invalid pointer for
-                // the src/dst, but the LLVM implementation specifies that a copy with
-                // length zero is a no-op. This comes up specifically when handling
-                // the empty string; CBMC will fail on passing a reference to empty
-                // string unless we codegen this zero check.
-                // https://llvm.org/docs/LangRef.html#llvm-memcpy-intrinsic
-                Stmt::if_then_else(n.is_zero().not(), e.as_stmt(location.clone()), None, location)
+                // It's surprising that calls to the intrinsic
+                // `copy_nonoverlapping` are not handled in `codegen_intrinsic`.
+                // We pack the operands and their types, and then call
+                // `codegen_copy_intrinsic` as if it was an intrinsic.
+                let fargs = vec![
+                    self.codegen_operand(src),
+                    self.codegen_operand(dst),
+                    self.codegen_operand(count),
+                ];
+                let farg_types =
+                    &[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)];
+                self.codegen_copy_intrinsic(
+                    "copy_nonoverlapping",
+                    true,
+                    fargs,
+                    farg_types,
+                    None,
+                    location,
+                )
             }
             StatementKind::FakeRead(_)
             | StatementKind::Retag(_, _)