Audit copy_nonoverlapping intrinsic

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, false, fargs, farg_types, Some(p), loc)
+            }
             "copy_nonoverlapping" => unreachable!(
                 "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`"
             ),
@@ -897,21 +899,31 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::atomic_block(vec![skip_stmt], loc)
     }
 
-    /// An intrinsic that translates directly into `memmove`
+    /// Copies `count * size_of::<T>()` bytes from `src` to `dst`.
     /// https://doc.rust-lang.org/core/intrinsics/fn.copy.html
+    /// https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html
+    ///
+    /// Note that this function handles code generation for:
+    ///  1. The `copy` intrinsic.
+    ///  2. The `CopyNonOverlapping` statement.
     ///
     /// 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 nonoverlapping copy) 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(
         &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
@@ -924,14 +936,14 @@ impl<'tcx> GotocCtx<'tcx> {
         let src_align_check = self.codegen_assert(
             src_align,
             PropertyClass::DefaultAssertion,
-            "`src` is properly aligned",
+            "`src` must be properly aligned",
             loc,
         );
         let dst_align = self.is_ptr_aligned(farg_types[1], dst.clone());
         let dst_align_check = self.codegen_assert(
             dst_align,
             PropertyClass::DefaultAssertion,
-            "`dst` is properly aligned",
+            "`dst` must be properly aligned",
             loc,
         );
 
@@ -941,18 +953,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)
     }
 
@@ -1274,7 +1291,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let align_check = self.codegen_assert(
             align,
             PropertyClass::DefaultAssertion,
-            "`dst` is properly aligned",
+            "`dst` must be properly aligned",
             loc,
         );
         let expr = dst.dereference().assign(src, loc);
@@ -1299,13 +1316,13 @@ impl<'tcx> GotocCtx<'tcx> {
         let val = fargs.remove(0).cast_to(Type::c_int());
         let count = fargs.remove(0);
 
-        // Check that `dst` is properly aligned
+        // Check that `dst` must be properly aligned
         let dst_typ = farg_types[0];
         let align = self.is_ptr_aligned(dst_typ, dst.clone());
         let align_check = self.codegen_assert(
             align,
             PropertyClass::DefaultAssertion,
-            "`dst` is properly aligned",
+            "`dst` must be properly aligned",
             loc,
         );
 

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

@@ -731,22 +731,22 @@ 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)
+                // Pack the operands and their types, then call `codegen_copy`
+                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(
+                    "copy_nonoverlapping",
+                    true,
+                    fargs,
+                    farg_types,
+                    None,
+                    location,
+                )
             }
             StatementKind::FakeRead(_)
             | StatementKind::Retag(_, _)

tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/expected

@@ -0,0 +1,2 @@
+FAILURE\
+copy_nonoverlapping: attempt to compute number in bytes which would overflow

tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `copy_nonoverlapping` triggers an overflow failure if the `count`
+// argument can overflow a `usize`
+#[kani::proof]
+fn test_copy_nonoverlapping_unaligned() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+    // Passing `max_count` is guaranteed to overflow
+    // the count in bytes for `i32` pointers
+    let max_count = usize::MAX / 4 + 1;
+
+    unsafe {
+        let dst = src.add(1) as *mut i32;
+        core::intrinsics::copy_nonoverlapping(src, dst, max_count);
+    }
+}

tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/expected

@@ -0,0 +1 @@
+memcpy src/dst overlap

tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `copy_nonoverlapping` fails if the `src`/`dst` regions overlap.
+#[kani::proof]
+fn test_copy_nonoverlapping_with_overlap() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // The call to `copy_nonoverlapping` is expected to fail because
+        // the `src` region and the `dst` region overlap in `arr[1]`
+        let dst = src.add(1) as *mut i32;
+        core::intrinsics::copy_nonoverlapping(src, dst, 2);
+    }
+}

tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected

@@ -0,0 +1,2 @@
+FAILURE\
+`dst` must be properly aligned

tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `copy_nonoverlapping` fails when `dst` is not aligned.
+#[kani::proof]
+fn test_copy_nonoverlapping_unaligned() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // Get an unaligned pointer with a single-byte offset
+        let dst_i8: *const i8 = src.add(1) as *mut i8;
+        let dst_unaligned = unsafe { dst_i8.add(1) as *mut i32 };
+        core::intrinsics::copy_nonoverlapping(src, dst_unaligned, 1);
+    }
+}

tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected

@@ -0,0 +1,2 @@
+FAILURE\
+`src` must be properly aligned

tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `copy_nonoverlapping` fails when `src` is not aligned.
+#[kani::proof]
+fn test_copy_nonoverlapping_unaligned() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // Get an unaligned pointer with a single-byte offset
+        let src_i8: *const i8 = src as *const i8;
+        let src_unaligned = unsafe { src_i8.add(1) as *const i32 };
+        let dst = src.add(1) as *mut i32;
+        core::intrinsics::copy_nonoverlapping(src_unaligned, dst, 1);
+    }
+}

tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/expected

@@ -0,0 +1,2 @@
+FAILURE\
+memcpy source region readable

tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `copy_nonoverlapping` fails when `src` is not valid for reads.
+#[kani::proof]
+fn test_copy_nonoverlapping_invalid() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // Get an invalid pointer with a negative offset
+        let src_invalid = unsafe { src.sub(1) as *const i32 };
+        let dst = src.add(1) as *mut i32;
+        core::intrinsics::copy_nonoverlapping(src_invalid, dst, 1);
+    }
+}

tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/expected

@@ -0,0 +1,2 @@
+FAILURE\
+memcpy destination region writeable

tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `copy_nonoverlapping` fails when `dst` is not valid for writes.
+#[kani::proof]
+fn test_copy_nonoverlapping_invalid() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // Get an invalid pointer with an out-of-bounds offset
+        let dst_invalid = src.add(3) as *mut i32;
+        core::intrinsics::copy_nonoverlapping(src, dst_invalid, 1);
+    }
+}

tests/expected/intrinsics/copy/copy-unaligned-dst/expected

@@ -1,2 +1,2 @@
 FAILURE\
-`dst` is properly aligned
+`dst` must be properly aligned

tests/expected/intrinsics/copy/copy-unaligned-src/expected

@@ -1,2 +1,2 @@
 FAILURE\
-`src` is properly aligned
+`src` must be properly aligned

tests/expected/intrinsics/write_bytes/unaligned/expected

@@ -1,2 +1,2 @@
 FAILURE\
-`dst` is properly aligned
+`dst` must be properly aligned