From 9a5463be5b0e39ebe8b99c1c0e775575b8aa901e Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Sat, 23 Apr 2022 21:22:56 +0000 Subject: [PATCH 1/7] Audit for `write_bytes` --- .../codegen/intrinsic.rs | 41 +++++++++++++++---- 1 file changed, 32 insertions(+), 9 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 35a5217aaede..51f551ec1db7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -628,16 +628,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" @@ -1156,4 +1149,34 @@ impl<'tcx> GotocCtx<'tcx> { let expr = dst.dereference().assign(src, loc.clone()); Stmt::block(vec![align_check, expr], loc) } + + /// Sets `count * size_of::()` 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 `--pointer-check`) + /// * `dst` must be properly aligned (done by `align_check` below) + fn codegen_write_bytes( + &mut self, + instance: Instance<'tcx>, + _intrinsic: &str, + mut fargs: Vec, + 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); + 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.clone(), + ); + let layout = self.layout_of(ty); + let sz = Expr::int_constant(layout.size.bytes(), Type::size_t()); + let memset_call = BuiltinFn::Memset.call(vec![dst, val, count.mul(sz)], loc); + Stmt::block(vec![align_check, memset_call.as_stmt(loc)], loc) + } } From a67180df312c35ac8728e8642928113c00c14322 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Sat, 23 Apr 2022 21:48:52 +0000 Subject: [PATCH 2/7] Add tests for `write_bytes` --- .../write_bytes/out-of-bounds/expected | 2 ++ .../write_bytes/out-of-bounds/main.rs | 19 ++++++++++++++++ .../intrinsics/write_bytes/unaligned/expected | 2 ++ .../intrinsics/write_bytes/unaligned/main.rs | 22 +++++++++++++++++++ tests/kani/Intrinsics/WriteBytes/main.rs | 19 ++++++++++++++++ 5 files changed, 64 insertions(+) create mode 100644 tests/expected/intrinsics/write_bytes/out-of-bounds/expected create mode 100644 tests/expected/intrinsics/write_bytes/out-of-bounds/main.rs create mode 100644 tests/expected/intrinsics/write_bytes/unaligned/expected create mode 100644 tests/expected/intrinsics/write_bytes/unaligned/main.rs create mode 100644 tests/kani/Intrinsics/WriteBytes/main.rs diff --git a/tests/expected/intrinsics/write_bytes/out-of-bounds/expected b/tests/expected/intrinsics/write_bytes/out-of-bounds/expected new file mode 100644 index 000000000000..d69010f53d0c --- /dev/null +++ b/tests/expected/intrinsics/write_bytes/out-of-bounds/expected @@ -0,0 +1,2 @@ +FAILURE\ +memset destination region writeable \ No newline at end of file diff --git a/tests/expected/intrinsics/write_bytes/out-of-bounds/main.rs b/tests/expected/intrinsics/write_bytes/out-of-bounds/main.rs new file mode 100644 index 000000000000..7bd5ea7ea0ea --- /dev/null +++ b/tests/expected/intrinsics/write_bytes/out-of-bounds/main.rs @@ -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]); +} diff --git a/tests/expected/intrinsics/write_bytes/unaligned/expected b/tests/expected/intrinsics/write_bytes/unaligned/expected new file mode 100644 index 000000000000..0fe63b4113d4 --- /dev/null +++ b/tests/expected/intrinsics/write_bytes/unaligned/expected @@ -0,0 +1,2 @@ +FAILURE\ +`dst` is properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/write_bytes/unaligned/main.rs b/tests/expected/intrinsics/write_bytes/unaligned/main.rs new file mode 100644 index 000000000000..4a941a56c39d --- /dev/null +++ b/tests/expected/intrinsics/write_bytes/unaligned/main.rs @@ -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]); +} diff --git a/tests/kani/Intrinsics/WriteBytes/main.rs b/tests/kani/Intrinsics/WriteBytes/main.rs new file mode 100644 index 000000000000..395c1c03c355 --- /dev/null +++ b/tests/kani/Intrinsics/WriteBytes/main.rs @@ -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]); +} From bc20e54311536d5afdcb19beed703a95eb099f0f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Sat, 23 Apr 2022 21:49:46 +0000 Subject: [PATCH 3/7] Update comment --- kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 51f551ec1db7..462244ccb92b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1154,7 +1154,7 @@ impl<'tcx> GotocCtx<'tcx> { /// 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 `--pointer-check`) + /// * `dst` must be valid for writes (done by memset writable check) /// * `dst` must be properly aligned (done by `align_check` below) fn codegen_write_bytes( &mut self, From 4bba9555bff603615807c43478ec0772dbf502e7 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 25 Apr 2022 22:59:13 +0000 Subject: [PATCH 4/7] Remove loc clone --- kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 462244ccb92b..3d6bca08387d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1172,7 +1172,7 @@ impl<'tcx> GotocCtx<'tcx> { align, PropertyClass::DefaultAssertion, "`dst` is properly aligned", - loc.clone(), + loc, ); let layout = self.layout_of(ty); let sz = Expr::int_constant(layout.size.bytes(), Type::size_t()); From 3c33ffe047c48d10c60f13c89bb02aa0b92a5a73 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 26 Apr 2022 13:41:56 +0000 Subject: [PATCH 5/7] Check overflows when computing `bytes` --- .../codegen/intrinsic.rs | 22 +++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 3d6bca08387d..4a74c5426890 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1156,16 +1156,20 @@ impl<'tcx> GotocCtx<'tcx> { /// 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, + intrinsic: &str, mut fargs: Vec, 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( @@ -1174,9 +1178,19 @@ impl<'tcx> GotocCtx<'tcx> { "`dst` is properly aligned", loc, ); + + // Check that computing `bytes` would not overflow let layout = self.layout_of(ty); - let sz = Expr::int_constant(layout.size.bytes(), Type::size_t()); - let memset_call = BuiltinFn::Memset.call(vec![dst, val, count.mul(sz)], loc); - Stmt::block(vec![align_check, memset_call.as_stmt(loc)], loc) + 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.clone(), + ); + + 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) } } From 7bbc16b57951e74da735705bc12b4b2ef01c305a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 26 Apr 2022 13:42:20 +0000 Subject: [PATCH 6/7] Add test for expected overflows --- .../intrinsics/write_bytes/overflow/expected | 2 ++ .../intrinsics/write_bytes/overflow/main.rs | 20 +++++++++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 tests/expected/intrinsics/write_bytes/overflow/expected create mode 100644 tests/expected/intrinsics/write_bytes/overflow/main.rs diff --git a/tests/expected/intrinsics/write_bytes/overflow/expected b/tests/expected/intrinsics/write_bytes/overflow/expected new file mode 100644 index 000000000000..4fb5bfd4c9ee --- /dev/null +++ b/tests/expected/intrinsics/write_bytes/overflow/expected @@ -0,0 +1,2 @@ +FAILURE\ +write_bytes: attempt to compute `bytes` which would overflow \ No newline at end of file diff --git a/tests/expected/intrinsics/write_bytes/overflow/main.rs b/tests/expected/intrinsics/write_bytes/overflow/main.rs new file mode 100644 index 000000000000..0e2ff04a90b9 --- /dev/null +++ b/tests/expected/intrinsics/write_bytes/overflow/main.rs @@ -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); + } +} From e448686a08065febd64b1e698a257f02eec9fe1b Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 26 Apr 2022 13:43:17 +0000 Subject: [PATCH 7/7] Remove `loc` cloning --- kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 4a74c5426890..6343318d4172 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1187,7 +1187,7 @@ impl<'tcx> GotocCtx<'tcx> { bytes.overflowed.not(), PropertyClass::ArithmeticOverflow, format!("{}: attempt to compute `bytes` which would overflow", intrinsic).as_str(), - loc.clone(), + loc, ); let memset_call = BuiltinFn::Memset.call(vec![dst, val, bytes.result], loc);