From deaa485e8ef3010da49b789b03bf47b689785bcb Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Mon, 16 May 2022 10:39:12 -0400 Subject: [PATCH] Audit for `copy` intrinsic (#1199) * Add/restore tests for copy intrinsics * Audit for `copy` intrinsic * More expected tests (readable/writable) --- .../codegen/intrinsic.rs | 98 ++++++++++++------- .../intrinsics/copy/copy-overflow/expected | 2 + .../intrinsics/copy/copy-overflow/main.rs | 18 ++++ .../copy/copy-unaligned-dst/expected | 2 + .../copy/copy-unaligned-dst/main.rs | 16 +++ .../copy/copy-unaligned-src/expected | 2 + .../copy/copy-unaligned-src/main.rs | 17 ++++ .../copy/copy-unreadable-src/expected | 2 + .../copy/copy-unreadable-src/main.rs | 16 +++ .../copy/copy-unwritable-dst/expected | 2 + .../copy/copy-unwritable-dst/main.rs | 15 +++ tests/kani/Intrinsics/Copy/copy.rs | 33 +++++++ .../Copy/copy_nonoverlapping.rs} | 15 +-- 13 files changed, 190 insertions(+), 48 deletions(-) create mode 100644 tests/expected/intrinsics/copy/copy-overflow/expected create mode 100644 tests/expected/intrinsics/copy/copy-overflow/main.rs create mode 100644 tests/expected/intrinsics/copy/copy-unaligned-dst/expected create mode 100644 tests/expected/intrinsics/copy/copy-unaligned-dst/main.rs create mode 100644 tests/expected/intrinsics/copy/copy-unaligned-src/expected create mode 100644 tests/expected/intrinsics/copy/copy-unaligned-src/main.rs create mode 100644 tests/expected/intrinsics/copy/copy-unreadable-src/expected create mode 100644 tests/expected/intrinsics/copy/copy-unreadable-src/main.rs create mode 100644 tests/expected/intrinsics/copy/copy-unwritable-dst/expected create mode 100644 tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs create mode 100644 tests/kani/Intrinsics/Copy/copy.rs rename tests/kani/{CopyIntrinsics/main_fixme.rs => Intrinsics/Copy/copy_nonoverlapping.rs} (85%) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 47cfe14335e28..ac8d805e2d803 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -146,39 +146,6 @@ impl<'tcx> GotocCtx<'tcx> { let farg_types = sig.inputs(); let cbmc_ret_ty = self.codegen_ty(ret_ty); - /// https://doc.rust-lang.org/core/intrinsics/fn.copy.html - /// https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html - /// An intrinsic that translates directly into either memmove (for copy) or memcpy (copy_nonoverlapping) - macro_rules! _codegen_intrinsic_copy { - ($f:ident) => {{ - let src = fargs.remove(0).cast_to(Type::void_pointer()); - let dst = fargs.remove(0).cast_to(Type::void_pointer()); - let count = fargs.remove(0); - let sz = { - match self.fn_sig_of_instance(instance).unwrap().skip_binder().inputs()[0] - .kind() - { - ty::RawPtr(t) => { - let layout = self.layout_of(t.ty); - Expr::int_constant(layout.size.bytes(), Type::size_t()) - } - _ => unreachable!(), - } - }; - let n = sz.mul(count); - let call_memcopy = BuiltinFn::$f.call(vec![dst.clone(), src, n.clone()], loc); - - // 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 - let copy_if_nontrivial = n.is_zero().ternary(dst, call_memcopy); - self.codegen_expr_to_place(p, copy_if_nontrivial) - }}; - } - // Codegens a simple intrinsic: ie. one which maps directly to a matching goto construct // We need to use this macro form because of a known limitation in rust // `codegen_simple_intrinsic!(self.get_sqrt(), Type::float())` gives the error message: @@ -500,8 +467,10 @@ impl<'tcx> GotocCtx<'tcx> { "ceilf64" => codegen_unimplemented_intrinsic!( "https://github.com/model-checking/kani/issues/1025" ), - "copy" => unstable_codegen!(_codegen_intrinsic_copy!(Memmove)), - "copy_nonoverlapping" => unstable_codegen!(_codegen_intrinsic_copy!(Memcpy)), + "copy" => self.codegen_copy_intrinsic(intrinsic, fargs, farg_types, p, loc), + "copy_nonoverlapping" => unreachable!( + "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`" + ), "copysignf32" => unstable_codegen!(codegen_simple_intrinsic!(Copysignf)), "copysignf64" => unstable_codegen!(codegen_simple_intrinsic!(Copysign)), "cosf32" => codegen_simple_intrinsic!(Cosf), @@ -928,6 +897,65 @@ 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 + /// + /// 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`) + /// 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( + &mut self, + intrinsic: &str, + mut fargs: Vec, + farg_types: &[Ty<'tcx>], + p: &Place<'tcx>, + loc: Location, + ) -> Stmt { + // The two first arguments are pointers. It's safe to cast them to void + // pointers or directly unwrap the `pointee_type` result as seen later. + let src = fargs.remove(0).cast_to(Type::void_pointer()); + let dst = fargs.remove(0).cast_to(Type::void_pointer()); + + // Generate alignment checks for both pointers + let src_align = self.is_ptr_aligned(farg_types[0], src.clone()); + let src_align_check = self.codegen_assert( + src_align, + PropertyClass::DefaultAssertion, + "`src` is 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", + loc, + ); + + // Compute the number of bytes to be copied + let count = fargs.remove(0); + let pointee_type = pointee_type(farg_types[0]).unwrap(); + 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); + + // 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. + // 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); + Stmt::block(vec![src_align_check, dst_align_check, overflow_check, copy_expr], loc) + } + /// Computes the offset from a pointer /// https://doc.rust-lang.org/std/intrinsics/fn.offset.html fn codegen_offset( diff --git a/tests/expected/intrinsics/copy/copy-overflow/expected b/tests/expected/intrinsics/copy/copy-overflow/expected new file mode 100644 index 0000000000000..040e3c6090bbe --- /dev/null +++ b/tests/expected/intrinsics/copy/copy-overflow/expected @@ -0,0 +1,2 @@ +FAILURE\ +copy: attempt to compute number in bytes which would overflow \ No newline at end of file diff --git a/tests/expected/intrinsics/copy/copy-overflow/main.rs b/tests/expected/intrinsics/copy/copy-overflow/main.rs new file mode 100644 index 0000000000000..2688d8cffa486 --- /dev/null +++ b/tests/expected/intrinsics/copy/copy-overflow/main.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `copy` triggers an overflow failure if the `count` argument can +// overflow a `usize` +#[kani::proof] +fn test_copy_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(src, dst, max_count); + } +} diff --git a/tests/expected/intrinsics/copy/copy-unaligned-dst/expected b/tests/expected/intrinsics/copy/copy-unaligned-dst/expected new file mode 100644 index 0000000000000..0fe63b4113d47 --- /dev/null +++ b/tests/expected/intrinsics/copy/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/copy-unaligned-dst/main.rs b/tests/expected/intrinsics/copy/copy-unaligned-dst/main.rs new file mode 100644 index 0000000000000..bc711e19a80aa --- /dev/null +++ b/tests/expected/intrinsics/copy/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/copy-unaligned-src/expected b/tests/expected/intrinsics/copy/copy-unaligned-src/expected new file mode 100644 index 0000000000000..047a4db37da17 --- /dev/null +++ b/tests/expected/intrinsics/copy/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/copy-unaligned-src/main.rs b/tests/expected/intrinsics/copy/copy-unaligned-src/main.rs new file mode 100644 index 0000000000000..8bbd6a10ec054 --- /dev/null +++ b/tests/expected/intrinsics/copy/copy-unaligned-src/main.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `copy` fails when `src` 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 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(src_unaligned, dst, 1); + } +} diff --git a/tests/expected/intrinsics/copy/copy-unreadable-src/expected b/tests/expected/intrinsics/copy/copy-unreadable-src/expected new file mode 100644 index 0000000000000..d050fc3af4e8e --- /dev/null +++ b/tests/expected/intrinsics/copy/copy-unreadable-src/expected @@ -0,0 +1,2 @@ +FAILURE\ +memmove source region readable \ No newline at end of file diff --git a/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs b/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs new file mode 100644 index 0000000000000..2b0e71cc16f36 --- /dev/null +++ b/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `copy` fails when `src` is not valid for reads. +#[kani::proof] +fn test_copy_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(src_invalid, dst, 1); + } +} diff --git a/tests/expected/intrinsics/copy/copy-unwritable-dst/expected b/tests/expected/intrinsics/copy/copy-unwritable-dst/expected new file mode 100644 index 0000000000000..5f190242aba67 --- /dev/null +++ b/tests/expected/intrinsics/copy/copy-unwritable-dst/expected @@ -0,0 +1,2 @@ +FAILURE\ +memmove destination region writeable \ No newline at end of file diff --git a/tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs b/tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs new file mode 100644 index 0000000000000..f68e9b2a807c1 --- /dev/null +++ b/tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `copy` fails when `dst` is not valid for writes. +#[kani::proof] +fn test_copy_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(src, dst_invalid, 1); + } +} diff --git a/tests/kani/Intrinsics/Copy/copy.rs b/tests/kani/Intrinsics/Copy/copy.rs new file mode 100644 index 0000000000000..9fb86b1304966 --- /dev/null +++ b/tests/kani/Intrinsics/Copy/copy.rs @@ -0,0 +1,33 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that `copy` works as expected: Copies a number `n` of elements from +// pointer `src` to pointer `dst`, even if their regions overlap. + +#[kani::proof] +fn test_copy_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 { + core::intrinsics::copy(src, dst, 1); + assert!(*dst == expected_val); + } +} + +#[kani::proof] +fn test_copy_with_overlap() { + let arr: [i32; 3] = [0, 1, 0]; + let src: *const i32 = arr.as_ptr(); + + unsafe { + let dst = src.add(1) as *mut i32; + core::intrinsics::copy(src, dst, 2); + // The first value does not change + assert!(arr[0] == 0); + // The next values are copied from `arr[0..=1]` + assert!(arr[1] == 0); + assert!(arr[2] == 1); + } +} diff --git a/tests/kani/CopyIntrinsics/main_fixme.rs b/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs similarity index 85% rename from tests/kani/CopyIntrinsics/main_fixme.rs rename to tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs index a450ab5c429a0..c0633fce4d0e1 100644 --- a/tests/kani/CopyIntrinsics/main_fixme.rs +++ b/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs @@ -5,18 +5,8 @@ use std::mem; use std::ptr; -fn test_copy() { - // TODO: make an overlapping set of locations, and check that it does the right thing for the overlapping region too. - // https://github.com/model-checking/kani/issues/12 - 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 { - ptr::copy(src, dst, 1); - assert!(*dst == expected_val); - } -} +// Note: Calls to `copy_nonoverlapping` are handled by `codegen_statement` +// and not `codegen_intrinsic`: https://github.com/model-checking/kani/issues/1198 /// https://doc.rust-lang.org/std/ptr/fn.copy_nonoverlapping.html /// Moves all the elements of `src` into `dst`, leaving `src` empty. @@ -89,7 +79,6 @@ fn test_swap() { #[kani::proof] fn main() { - test_copy(); test_swap(); test_append(); }