From c25e44531500488508de217ac9df2c96f51e81f9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 16 May 2022 20:45:02 +0000 Subject: [PATCH 1/6] Add new tests and split old ones --- .../copy-overflow/expected | 2 + .../copy-nonoverlapping/copy-overflow/main.rs | 18 ++++ .../copy-overlapping/expected | 1 + .../copy-overlapping/main.rs | 16 ++++ .../copy-unaligned-dst/expected | 2 + .../copy-unaligned-dst/main.rs | 16 ++++ .../copy-unaligned-src/expected | 2 + .../copy-unaligned-src/main.rs | 17 ++++ .../copy-unreadable-src/expected | 2 + .../copy-unreadable-src/main.rs | 16 ++++ .../copy-unwritable-dst/expected | 2 + .../copy-unwritable-dst/main.rs | 15 ++++ .../Intrinsics/Copy/copy_nonoverlapping.rs | 88 +++---------------- .../Copy/copy_nonoverlapping_append.rs | 45 ++++++++++ .../Copy/copy_nonoverlapping_swap.rs | 32 +++++++ 15 files changed, 197 insertions(+), 77 deletions(-) create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs create mode 100644 tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs create mode 100644 tests/kani/Intrinsics/Copy/copy_nonoverlapping_swap.rs diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/expected new file mode 100644 index 000000000000..ac218a7a2596 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/expected @@ -0,0 +1,2 @@ +FAILURE\ +copy_nonoverlapping: attempt to compute number in bytes which would overflow \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs new file mode 100644 index 000000000000..c1c655f3f1ed --- /dev/null +++ b/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); + } +} diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/expected new file mode 100644 index 000000000000..9ebadf73b291 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/expected @@ -0,0 +1 @@ +memcpy src/dst overlap \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs new file mode 100644 index 000000000000..bcfa5dae79a4 --- /dev/null +++ b/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); + } +} diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected new file mode 100644 index 000000000000..0fe63b4113d4 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected @@ -0,0 +1,2 @@ +FAILURE\ +`dst` is properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs new file mode 100644 index 000000000000..bc711e19a80a --- /dev/null +++ b/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` fails when `dst` is not aligned. +#[kani::proof] +fn test_copy_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(src, dst_unaligned, 1); + } +} diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected new file mode 100644 index 000000000000..047a4db37da1 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected @@ -0,0 +1,2 @@ +FAILURE\ +`src` is properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs new file mode 100644 index 000000000000..ad93c761df81 --- /dev/null +++ b/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); + } +} diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/expected new file mode 100644 index 000000000000..3fe1563c21c2 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/expected @@ -0,0 +1,2 @@ +FAILURE\ +memcpy source region readable \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs new file mode 100644 index 000000000000..ff2d54e7ca6b --- /dev/null +++ b/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); + } +} diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/expected new file mode 100644 index 000000000000..78e53fb3a882 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/expected @@ -0,0 +1,2 @@ +FAILURE\ +memcpy destination region writeable \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs new file mode 100644 index 000000000000..34c7832267e0 --- /dev/null +++ b/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); + } +} diff --git a/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs b/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs index c0633fce4d0e..bec748bfa7a3 100644 --- a/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs +++ b/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(dst: &mut Vec, src: &mut Vec) { - 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(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(); -} diff --git a/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs new file mode 100644 index 000000000000..a9c0d3a5eb9a --- /dev/null +++ b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs @@ -0,0 +1,45 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test the append example from +// https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html +use std::ptr; + +#[kani::proof] +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()); +} + +/// Moves all the elements of `src` into `dst`, leaving `src` empty. +fn append(dst: &mut Vec, src: &mut Vec) { + 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); + } +} diff --git a/tests/kani/Intrinsics/Copy/copy_nonoverlapping_swap.rs b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_swap.rs new file mode 100644 index 000000000000..6e36d4c297ff --- /dev/null +++ b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_swap.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test the swap example from +// https://doc.redox-os.org/std/std/intrinsics/fn.copy_nonoverlapping.html +use std::mem; +use std::ptr; + +#[kani::proof] +fn test_swap() { + let mut x = 12; + let mut y = 13; + swap(&mut x, &mut y); + assert!(x == 13); + assert!(y == 12); +} + +fn swap(x: &mut T, y: &mut T) { + unsafe { + // Give ourselves some scratch space to work with + let mut t: T = mem::uninitialized(); + + // 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); + } +} From 03d7f54b8ef9fe447938b8ee51060025a048ea79 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 16 May 2022 20:45:43 +0000 Subject: [PATCH 2/6] Handle `CopyNonOverlapping` statements from intrinsics code --- .../codegen/intrinsic.rs | 44 ++++++++++++------- .../codegen/statement.rs | 35 ++++++++------- 2 files changed, 48 insertions(+), 31 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index ac8d805e2d80..a6d35d91a358 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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::()` bytes (done by calls to `memmove`) + /// * (Exclusive to `copy_nonoverlapping`) The region of memory beginning + /// at `src` with a size of `count * size_of::()` 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, 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) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index f8b8ee4323f7..e143582da79b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/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(_, _) From 26e8b3379ec0d67b5199195c657118cd52ae8c39 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 16 May 2022 21:09:35 +0000 Subject: [PATCH 3/6] Add missed changes on one test --- .../copy-nonoverlapping/copy-unaligned-dst/main.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs index bc711e19a80a..82c33d60c0c0 100644 --- a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs @@ -1,9 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Checks that `copy` fails when `dst` is not aligned. +// Checks that `copy_nonoverlapping` fails when `dst` is not aligned. #[kani::proof] -fn test_copy_unaligned() { +fn test_copy_nonoverlapping_unaligned() { let arr: [i32; 3] = [0, 1, 0]; let src: *const i32 = arr.as_ptr(); @@ -11,6 +11,6 @@ fn test_copy_unaligned() { // 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(src, dst_unaligned, 1); + core::intrinsics::copy_nonoverlapping(src, dst_unaligned, 1); } } From 8e4e0f1b0ca7287bdb12a98fe8ee71bf45238ca1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 May 2022 19:07:03 +0000 Subject: [PATCH 4/6] Rename and add comments in `codegen_copy` --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 13 ++++++++----- .../src/codegen_cprover_gotoc/codegen/statement.rs | 7 ++----- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index a6d35d91a358..744f49820ef0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -468,7 +468,7 @@ impl<'tcx> GotocCtx<'tcx> { "https://github.com/model-checking/kani/issues/1025" ), "copy" => { - self.codegen_copy_intrinsic(intrinsic, false, fargs, farg_types, Some(p), loc) + self.codegen_copy(intrinsic, false, fargs, farg_types, Some(p), loc) } "copy_nonoverlapping" => unreachable!( "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`" @@ -899,22 +899,25 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::atomic_block(vec![skip_stmt], loc) } - /// An intrinsic that translates directly into `memmove` (for `copy`) - /// or `memcpy` (for `copy_nonoverlapping`) + /// Copies `count * size_of::()` 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::()` bytes (done by calls to `memmove`) - /// * (Exclusive to `copy_nonoverlapping`) The region of memory beginning + /// * (Exclusive to nonoverlapping copy) The region of memory beginning /// at `src` with a size of `count * size_of::()` 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 of the copy built-in call) would not overflow. - pub fn codegen_copy_intrinsic( + pub fn codegen_copy( &mut self, intrinsic: &str, is_non_overlapping: bool, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index e143582da79b..5579073a3e32 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -731,10 +731,7 @@ impl<'tcx> GotocCtx<'tcx> { ref dst, ref count, }) => { - // 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. + // Pack the operands and their types, then call `codegen_copy` let fargs = vec![ self.codegen_operand(src), self.codegen_operand(dst), @@ -742,7 +739,7 @@ impl<'tcx> GotocCtx<'tcx> { ]; let farg_types = &[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)]; - self.codegen_copy_intrinsic( + self.codegen_copy( "copy_nonoverlapping", true, fargs, From ee200b123946fa8b5c293e4364aea416f3cab8af Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 May 2022 19:10:43 +0000 Subject: [PATCH 5/6] Slight rewording for alignment checks --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 10 +++++----- .../copy-nonoverlapping/copy-unaligned-dst/expected | 2 +- .../copy-nonoverlapping/copy-unaligned-src/expected | 2 +- .../intrinsics/copy/copy-unaligned-dst/expected | 2 +- .../intrinsics/copy/copy-unaligned-src/expected | 2 +- .../expected/intrinsics/write_bytes/unaligned/expected | 2 +- 6 files changed, 10 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 744f49820ef0..70572af5163b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -936,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, ); @@ -1291,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); @@ -1316,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, ); diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected index 0fe63b4113d4..1c1e00c0cb0a 100644 --- a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected @@ -1,2 +1,2 @@ FAILURE\ -`dst` is properly aligned \ No newline at end of file +`dst` must be properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected index 047a4db37da1..485accebd53c 100644 --- a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected @@ -1,2 +1,2 @@ FAILURE\ -`src` is properly aligned \ No newline at end of file +`src` must be properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/copy/copy-unaligned-dst/expected b/tests/expected/intrinsics/copy/copy-unaligned-dst/expected index 0fe63b4113d4..1c1e00c0cb0a 100644 --- a/tests/expected/intrinsics/copy/copy-unaligned-dst/expected +++ b/tests/expected/intrinsics/copy/copy-unaligned-dst/expected @@ -1,2 +1,2 @@ FAILURE\ -`dst` is properly aligned \ No newline at end of file +`dst` must be properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/copy/copy-unaligned-src/expected b/tests/expected/intrinsics/copy/copy-unaligned-src/expected index 047a4db37da1..485accebd53c 100644 --- a/tests/expected/intrinsics/copy/copy-unaligned-src/expected +++ b/tests/expected/intrinsics/copy/copy-unaligned-src/expected @@ -1,2 +1,2 @@ FAILURE\ -`src` is properly aligned \ No newline at end of file +`src` must be properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/write_bytes/unaligned/expected b/tests/expected/intrinsics/write_bytes/unaligned/expected index 0fe63b4113d4..1c1e00c0cb0a 100644 --- a/tests/expected/intrinsics/write_bytes/unaligned/expected +++ b/tests/expected/intrinsics/write_bytes/unaligned/expected @@ -1,2 +1,2 @@ FAILURE\ -`dst` is properly aligned \ No newline at end of file +`dst` must be properly aligned \ No newline at end of file From 67ffffbf80ac8191ceed353edf672a57c9e058a9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 May 2022 19:20:01 +0000 Subject: [PATCH 6/6] Fix format + suggestion --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 8 +++----- .../src/codegen_cprover_gotoc/codegen/statement.rs | 9 +-------- 2 files changed, 4 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 70572af5163b..bca3a9ad1b1a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -467,9 +467,7 @@ impl<'tcx> GotocCtx<'tcx> { "ceilf64" => codegen_unimplemented_intrinsic!( "https://github.com/model-checking/kani/issues/1025" ), - "copy" => { - self.codegen_copy(intrinsic, false, fargs, farg_types, Some(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`" ), @@ -900,12 +898,12 @@ impl<'tcx> GotocCtx<'tcx> { } /// Copies `count * size_of::()` 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. + /// 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) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 5579073a3e32..8a5ba1370d7a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -739,14 +739,7 @@ impl<'tcx> GotocCtx<'tcx> { ]; 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, - ) + self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location) } StatementKind::FakeRead(_) | StatementKind::Retag(_, _)