Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Audit copy_nonoverlapping intrinsic #1201

Merged
merged 7 commits into from
May 20, 2022
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 29 additions & 15 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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`"
),
Expand Down Expand Up @@ -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`)
adpaco-aws marked this conversation as resolved.
Show resolved Hide resolved
/// or `memcpy` (for `copy_nonoverlapping`)
/// https://doc.rust-lang.org/core/intrinsics/fn.copy.html
adpaco-aws marked this conversation as resolved.
Show resolved Hide resolved
/// 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
Expand Down Expand Up @@ -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)
}

Expand Down
35 changes: 19 additions & 16 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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(
adpaco-aws marked this conversation as resolved.
Show resolved Hide resolved
"copy_nonoverlapping",
true,
fargs,
farg_types,
None,
location,
)
}
StatementKind::FakeRead(_)
| StatementKind::Retag(_, _)
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
FAILURE\
copy_nonoverlapping: attempt to compute number in bytes which would overflow
Original file line number Diff line number Diff line change
@@ -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);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
memcpy src/dst overlap
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this a CBMC message? I was wondering if we change it to say copy_nonoverlap here. Do we use memcpy anywhere else?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, this is a CBMC message so there's not much we can do. We use memcpy in our __rust_realloc C implementation but we don't generate calls to memcpy anywhere else.

Original file line number Diff line number Diff line change
@@ -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);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
FAILURE\
`dst` is properly aligned
adpaco-aws marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
@@ -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);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
FAILURE\
`src` is properly aligned
Original file line number Diff line number Diff line change
@@ -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);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
FAILURE\
memcpy source region readable
Original file line number Diff line number Diff line change
@@ -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);
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
FAILURE\
memcpy destination region writeable
Original file line number Diff line number Diff line change
@@ -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);
}
}
88 changes: 11 additions & 77 deletions tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs
Original file line number Diff line number Diff line change
@@ -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();
}
45 changes: 45 additions & 0 deletions tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs
Original file line number Diff line number Diff line change
@@ -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<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);
}
}
Loading