Audit copy_nonoverlapping intrinsic

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

@@ -467,7 +467,7 @@ 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 +897,31 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::atomic_block(vec![skip_stmt], loc)
     }
 
-    /// An intrinsic that translates directly into `memmove`
-    /// https://doc.rust-lang.org/core/intrinsics/fn.copy.html
+    /// Copies `count * size_of::<T>()` bytes from `src` to `dst`.
+    ///
+    /// Note that this function handles code generation for:
+    ///  1. The `copy` intrinsic.
+    ///     https://doc.rust-lang.org/core/intrinsics/fn.copy.html
+    ///  2. The `CopyNonOverlapping` statement.
+    ///     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 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 +934,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 +951,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 +1289,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 +1314,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,15 @@ 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

tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs

@@ -1,84 +1,18 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-#![feature(core_intrinsics)]
-/// kani main.rs -- --default-unwind 20 --unwinding-assertions
-use std::mem;
-use std::ptr;
 
-// Note: Calls to `copy_nonoverlapping` are handled by `codegen_statement`
-// and not `codegen_intrinsic`: https://github.com/model-checking/kani/issues/1198
+// Check that `copy_nonoverlapping` works as expected: Copies a number `n` of elements from
+// pointer `src` to pointer `dst`. Their regions of memory do not overlap, otherwise the
+// call to `copy_nonoverlapping` would fail (a separate test checks for this).
 
-/// https://doc.rust-lang.org/std/ptr/fn.copy_nonoverlapping.html
-/// Moves all the elements of `src` into `dst`, leaving `src` empty.
-fn append<T>(dst: &mut Vec<T>, src: &mut Vec<T>) {
-    let src_len = src.len();
-    let dst_len = dst.len();
-
-    // Ensure that `dst` has enough capacity to hold all of `src`.
-    dst.reserve(src_len);
-
-    unsafe {
-        // The call to offset is always safe because `Vec` will never
-        // allocate more than `isize::MAX` bytes.
-        let dst_ptr = dst.as_mut_ptr().offset(dst_len as isize);
-        let src_ptr = src.as_ptr();
-
-        // Truncate `src` without dropping its contents. We do this first,
-        // to avoid problems in case something further down panics.
-        src.set_len(0);
-
-        // The two regions cannot overlap because mutable references do
-        // not alias, and two different vectors cannot own the same
-        // memory.
-        ptr::copy_nonoverlapping(src_ptr, dst_ptr, src_len);
-
-        // Notify `dst` that it now holds the contents of `src`.
-        dst.set_len(dst_len + src_len);
-    }
-}
-
-fn test_append() {
-    let mut a = vec!['r'];
-    let mut b = vec!['u', 's', 't'];
-
-    append(&mut a, &mut b);
-
-    assert!(a == &['r', 'u', 's', 't']);
-    assert!(b.is_empty());
-}
-
-/// Test the swap example from https://doc.redox-os.org/std/std/intrinsics/fn.copy_nonoverlapping.html
-/// Using T as uninitialized as in the example gives other errors, which we will solve later.
-/// For this test, passing in a default value that gets overridden is sufficient.
-fn swap_with_default<T>(x: &mut T, y: &mut T, default: T) {
+#[kani::proof]
+fn test_copy_nonoverlapping_simple() {
+    let mut expected_val = 42;
+    let src: *mut i32 = &mut expected_val as *mut i32;
+    let mut old_val = 99;
+    let dst: *mut i32 = &mut old_val;
     unsafe {
-        // Give ourselves some scratch space to work with
-        //         let mut t: T = mem::uninitialized();
-        let mut t: T = default;
-
-        // Perform the swap, `&mut` pointers never alias
-        ptr::copy_nonoverlapping(x, &mut t, 1);
-        ptr::copy_nonoverlapping(y, x, 1);
-        ptr::copy_nonoverlapping(&t, y, 1);
-
-        // y and t now point to the same thing, but we need to completely forget `tmp`
-        // because it's no longer relevant.
-        mem::forget(t);
+        core::intrinsics::copy_nonoverlapping(src, dst, 1);
+        assert!(*dst == expected_val);
     }
 }
-
-/// another test for copy_nonoverlapping, from
-/// https://doc.redox-os.org/std/std/intrinsics/fn.copy_nonoverlapping.html
-fn test_swap() {
-    let mut x = 12;
-    let mut y = 13;
-    swap_with_default(&mut x, &mut y, 3);
-    assert!(x == 13);
-    assert!(y == 12);
-}
-
-#[kani::proof]
-fn main() {
-    test_swap();
-    test_append();
-}