Skip to content

Commit

Permalink
Audit for write_bytes (#1102)
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws authored and tedinski committed Apr 26, 2022
1 parent b8369e5 commit 49253b3
Show file tree
Hide file tree
Showing 8 changed files with 132 additions and 9 deletions.
55 changes: 46 additions & 9 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -622,16 +622,9 @@ impl<'tcx> GotocCtx<'tcx> {
"wrapping_mul" => codegen_wrapping_op!(mul),
"wrapping_sub" => codegen_wrapping_op!(sub),
"write_bytes" => {
let dst = fargs.remove(0).cast_to(Type::void_pointer());
let val = fargs.remove(0).cast_to(Type::c_int());
let count = fargs.remove(0);
let ty = self.monomorphize(instance.substs.type_at(0));
let layout = self.layout_of(ty);
let sz = Expr::int_constant(layout.size.bytes(), Type::size_t());
let e = BuiltinFn::Memset.call(vec![dst, val, count.mul(sz)], loc);
self.codegen_expr_to_place(p, e)
assert!(self.place_ty(p).is_unit());
self.codegen_write_bytes(instance, intrinsic, fargs, loc)
}

// Unimplemented
_ => codegen_unimplemented_intrinsic!(
"https://github.com/model-checking/kani/issues/new/choose"
Expand Down Expand Up @@ -1188,4 +1181,48 @@ impl<'tcx> GotocCtx<'tcx> {
let expr = dst.dereference().assign(src, loc.clone());
Stmt::block(vec![align_check, expr], loc)
}

/// Sets `count * size_of::<T>()` bytes of memory starting at `dst` to `val`
/// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
///
/// Undefined behavior if any of these conditions are violated:
/// * `dst` must be valid for writes (done by memset writable check)
/// * `dst` must be properly aligned (done by `align_check` below)
/// In addition, we check that computing `bytes` (i.e., the third argument
/// for the `memset` call) would not overflow
fn codegen_write_bytes(
&mut self,
instance: Instance<'tcx>,
intrinsic: &str,
mut fargs: Vec<Expr>,
loc: Location,
) -> Stmt {
let dst = fargs.remove(0).cast_to(Type::void_pointer());
let val = fargs.remove(0).cast_to(Type::c_int());
let count = fargs.remove(0);

// Check that `dst` is properly aligned
let ty = self.monomorphize(instance.substs.type_at(0));
let align = self.is_aligned(ty, dst.clone());
let align_check = self.codegen_assert(
align,
PropertyClass::DefaultAssertion,
"`dst` is properly aligned",
loc,
);

// Check that computing `bytes` would not overflow
let layout = self.layout_of(ty);
let size = Expr::int_constant(layout.size.bytes(), Type::size_t());
let bytes = count.mul_overflow(size);
let overflow_check = self.codegen_assert(
bytes.overflowed.not(),
PropertyClass::ArithmeticOverflow,
format!("{}: attempt to compute `bytes` which would overflow", intrinsic).as_str(),
loc,
);

let memset_call = BuiltinFn::Memset.call(vec![dst, val, bytes.result], loc);
Stmt::block(vec![align_check, overflow_check, memset_call.as_stmt(loc)], loc)
}
}
2 changes: 2 additions & 0 deletions tests/expected/intrinsics/write_bytes/out-of-bounds/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
FAILURE\
memset destination region writeable
19 changes: 19 additions & 0 deletions tests/expected/intrinsics/write_bytes/out-of-bounds/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Checks that `write_bytes` fails if an out-of-bounds write is made.

// This test is a modified version of the example in
// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
#![feature(core_intrinsics)]
use std::intrinsics::write_bytes;

#[kani::proof]
fn main() {
let mut vec = vec![0u32; 4];
unsafe {
let vec_ptr = vec.as_mut_ptr().add(4);
write_bytes(vec_ptr, 0xfe, 1);
}
assert_eq!(vec, [0, 0, 0, 0]);
}
2 changes: 2 additions & 0 deletions tests/expected/intrinsics/write_bytes/overflow/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
FAILURE\
write_bytes: attempt to compute `bytes` which would overflow
20 changes: 20 additions & 0 deletions tests/expected/intrinsics/write_bytes/overflow/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Checks that `write_bytes` triggers the overflow check.

// This test is a modified version of the example in
// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
#![feature(core_intrinsics)]
use std::intrinsics::write_bytes;

#[kani::proof]
fn main() {
let mut vec = vec![0u32; 4];
unsafe {
let vec_ptr = vec.as_mut_ptr();
// Passing `usize::MAX + 1` is guaranteed to
// overflow when computing the number of bytes
write_bytes(vec_ptr, 0xfe, usize::MAX / 4 + 1);
}
}
2 changes: 2 additions & 0 deletions tests/expected/intrinsics/write_bytes/unaligned/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
FAILURE\
`dst` is properly aligned
22 changes: 22 additions & 0 deletions tests/expected/intrinsics/write_bytes/unaligned/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Checks that `write_bytes` fails when `dst` is not aligned.

// This test is a modified version of the example in
// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
use std::intrinsics::write_bytes;

#[kani::proof]
fn main() {
let mut vec = vec![0u32; 4];
unsafe {
let vec_ptr = vec.as_mut_ptr();
// Obtain an unaligned pointer by casting into `*mut u8`,
// adding an offset of 1 and casting back into `*mut u32`
let vec_ptr_u8: *mut u8 = vec_ptr as *mut u8;
let unaligned_ptr = vec_ptr_u8.add(1) as *mut u32;
write_bytes(unaligned_ptr, 0xfe, 2);
}
assert_eq!(vec, [0xfefefe00, 0xfefefefe, 0x000000fe, 0]);
}
19 changes: 19 additions & 0 deletions tests/kani/Intrinsics/WriteBytes/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Checks that `write_bytes` works as expected.

// This test is a modified version of the example in
// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
#![feature(core_intrinsics)]
use std::intrinsics::write_bytes;

#[kani::proof]
fn main() {
let mut vec = vec![0u32; 4];
unsafe {
let vec_ptr = vec.as_mut_ptr();
write_bytes(vec_ptr, 0xfe, 2);
}
assert_eq!(vec, [0xfefefefe, 0xfefefefe, 0, 0]);
}

0 comments on commit 49253b3

Please sign in to comment.