From 5b73cc5d4837662ff6d04b9e4e132459c312582b Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Fri, 18 Jun 2021 16:28:27 -0400 Subject: [PATCH 1/4] Don't call memcpy when len is 0 --- .../src/gotoc/cbmc/goto_program/expr.rs | 7 +++++++ .../rustc_codegen_llvm/src/gotoc/intrinsic.rs | 12 ++++++++++-- .../rustc_codegen_llvm/src/gotoc/statement.rs | 16 ++++++++++++++-- .../Strings/copy_empty_string_by_intrinsic.rs | 13 +++++++++++++ .../cbmc/Strings/copy_empty_string_by_ref.rs | 13 +++++++++++++ 5 files changed, 57 insertions(+), 4 deletions(-) create mode 100644 src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs create mode 100644 src/test/cbmc/Strings/copy_empty_string_by_ref.rs diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs index 645c29afef8e..4bbf5f8849fc 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs @@ -1105,6 +1105,13 @@ impl Expr { self.lt(typ.zero()) } + /// `self == 0` + pub fn is_zero(self) -> Self { + assert!(self.typ.is_numeric()); + let typ = self.typ.clone(); + self.eq(typ.zero()) + } + /// `self != NULL` pub fn is_nonnull(self) -> Self { assert!(self.typ.is_pointer()); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs index 3d0f47f35fbe..37c3c93e79a5 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs @@ -61,8 +61,16 @@ impl<'tcx> GotocCtx<'tcx> { } }; let n = sz.mul(count); - let e = BuiltinFn::$f.call(vec![dst, src, n], loc); - self.codegen_expr_to_place(p, e) + 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) }}; } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs index 57e5698c4ed9..e41e5ea59759 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -507,8 +507,20 @@ impl<'tcx> GotocCtx<'tcx> { 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], Location::none()); - e.as_stmt(Location::none()) + let e = BuiltinFn::Memcpy.call(vec![dst, src, n.clone()], Location::none()); + + // 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::none()), + None, + Location::none(), + ) } StatementKind::FakeRead(_) | StatementKind::Retag(_, _) diff --git a/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs new file mode 100644 index 000000000000..43d6c810b8b7 --- /dev/null +++ b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs @@ -0,0 +1,13 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Make sure we can handle implicit memcpy on the empty string + +fn take_string_ref(s: &str, l: usize) { + assert!(s.len() == l) +} + +fn main() { + take_string_ref(&"x".to_string(), 1); + take_string_ref(&"".to_string(), 0); +} \ No newline at end of file diff --git a/src/test/cbmc/Strings/copy_empty_string_by_ref.rs b/src/test/cbmc/Strings/copy_empty_string_by_ref.rs new file mode 100644 index 000000000000..43d6c810b8b7 --- /dev/null +++ b/src/test/cbmc/Strings/copy_empty_string_by_ref.rs @@ -0,0 +1,13 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Make sure we can handle implicit memcpy on the empty string + +fn take_string_ref(s: &str, l: usize) { + assert!(s.len() == l) +} + +fn main() { + take_string_ref(&"x".to_string(), 1); + take_string_ref(&"".to_string(), 0); +} \ No newline at end of file From 9b3d31e34b993d42516a7023b5e8b0361073f89f Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Fri, 18 Jun 2021 17:07:32 -0400 Subject: [PATCH 2/4] Add more tests --- .../Strings/copy_empty_string_by_intrinsic.rs | 27 +++++++++--- .../copy_empty_string_by_intrinsic_fail.rs | 42 +++++++++++++++++++ 2 files changed, 64 insertions(+), 5 deletions(-) create mode 100644 src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fail.rs diff --git a/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs index 43d6c810b8b7..86657a4552b9 100644 --- a/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs +++ b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs @@ -1,13 +1,30 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// Make sure we can handle implicit memcpy on the empty string +// Make sure we can handle explicit copy_nonoverlapping on empty string -fn take_string_ref(s: &str, l: usize) { - assert!(s.len() == l) +#![feature(rustc_private)] + +extern crate libc; + +use std::ptr::copy_nonoverlapping; +use std::slice::from_raw_parts; +use std::mem::{size_of}; +use std::str; + +fn copy_string(s: &str, l: usize) { + unsafe { + // Unsafe buffer + let size: libc::size_t = size_of::(); + let dest: *mut u8 = libc::malloc(size * l) as *mut u8; + + // Copy + let src = from_raw_parts(s.as_ptr(), l).as_ptr(); + copy_nonoverlapping(src, dest, l); + } } fn main() { - take_string_ref(&"x".to_string(), 1); - take_string_ref(&"".to_string(), 0); + copy_string("x", 1); + copy_string("", 0); } \ No newline at end of file diff --git a/src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fail.rs b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fail.rs new file mode 100644 index 000000000000..5b39d9f5d259 --- /dev/null +++ b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fail.rs @@ -0,0 +1,42 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Make sure we can handle explicit copy_nonoverlapping on empty string + +// The copy_nonoverlapping succeeds, but the final copy back to a slice +// fails: +// [...copy_empty_string_by_intrinsic.assertion.2] line 1035 unreachable code: FAILURE +// [...copy_empty_string_by_intrinsic.assertion.1] line 1037 a panicking function std::result::unwrap_failed is invoked: FAILURE +// [...copy_string.assertion.2] line 28 assertion failed: dest_as_str.len() == l: FAILURE + +#![feature(rustc_private)] + +extern crate libc; + +use std::ptr::copy_nonoverlapping; +use std::slice::from_raw_parts; +use std::mem::{size_of}; +use std::str; + +fn copy_string(s: &str, l: usize) { + unsafe { + // Unsafe buffer + let size: libc::size_t = size_of::(); + let dest: *mut u8 = libc::malloc(size * l) as *mut u8; + + // Copy + let src = from_raw_parts(s.as_ptr(), l).as_ptr(); + copy_nonoverlapping(src, dest, l); + + // THIS CHUNK causes 3 failures + // Back to str, check length + let dest_slice : &[u8] = from_raw_parts(dest, l); + let dest_as_str : &str= str::from_utf8(dest_slice).unwrap(); + assert!(dest_as_str.len() == l); + } +} + +fn main() { + copy_string("x", 1); + copy_string("", 0); +} \ No newline at end of file From df010663fe19a51f7c20959070ce7d7694d432a3 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Fri, 18 Jun 2021 17:18:58 -0400 Subject: [PATCH 3/4] Test name --- ..._intrinsic_fail.rs => copy_empty_string_by_intrinsic_fixme.rs} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/test/cbmc/Strings/{copy_empty_string_by_intrinsic_fail.rs => copy_empty_string_by_intrinsic_fixme.rs} (100%) diff --git a/src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fail.rs b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fixme.rs similarity index 100% rename from src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fail.rs rename to src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fixme.rs From 8b10ce233ffecd657f6432228df454f28dd01ee2 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 22 Jun 2021 09:15:26 -0400 Subject: [PATCH 4/4] Adrian comments, rustfmt --- .../Strings/copy_empty_string_by_intrinsic.rs | 10 +++++----- .../copy_empty_string_by_intrinsic_fixme.rs | 20 ++++++++++--------- .../cbmc/Strings/copy_empty_string_by_ref.rs | 8 ++++---- 3 files changed, 20 insertions(+), 18 deletions(-) diff --git a/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs index 86657a4552b9..0258d412ba9c 100644 --- a/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs +++ b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs @@ -7,9 +7,9 @@ extern crate libc; +use std::mem::size_of; use std::ptr::copy_nonoverlapping; use std::slice::from_raw_parts; -use std::mem::{size_of}; use std::str; fn copy_string(s: &str, l: usize) { @@ -17,7 +17,7 @@ fn copy_string(s: &str, l: usize) { // Unsafe buffer let size: libc::size_t = size_of::(); let dest: *mut u8 = libc::malloc(size * l) as *mut u8; - + // Copy let src = from_raw_parts(s.as_ptr(), l).as_ptr(); copy_nonoverlapping(src, dest, l); @@ -25,6 +25,6 @@ fn copy_string(s: &str, l: usize) { } fn main() { - copy_string("x", 1); - copy_string("", 0); -} \ No newline at end of file + copy_string("x", 1); + copy_string("", 0); +} diff --git a/src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fixme.rs b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fixme.rs index 5b39d9f5d259..cc56426c6c05 100644 --- a/src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fixme.rs +++ b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fixme.rs @@ -3,6 +3,7 @@ // Make sure we can handle explicit copy_nonoverlapping on empty string +// TODO: https://github.com/model-checking/rmc/issues/241 // The copy_nonoverlapping succeeds, but the final copy back to a slice // fails: // [...copy_empty_string_by_intrinsic.assertion.2] line 1035 unreachable code: FAILURE @@ -13,9 +14,9 @@ extern crate libc; +use std::mem::size_of; use std::ptr::copy_nonoverlapping; use std::slice::from_raw_parts; -use std::mem::{size_of}; use std::str; fn copy_string(s: &str, l: usize) { @@ -23,20 +24,21 @@ fn copy_string(s: &str, l: usize) { // Unsafe buffer let size: libc::size_t = size_of::(); let dest: *mut u8 = libc::malloc(size * l) as *mut u8; - + // Copy let src = from_raw_parts(s.as_ptr(), l).as_ptr(); copy_nonoverlapping(src, dest, l); - - // THIS CHUNK causes 3 failures + + // The chunk below causes the 3 failures at the top of the file // Back to str, check length - let dest_slice : &[u8] = from_raw_parts(dest, l); - let dest_as_str : &str= str::from_utf8(dest_slice).unwrap(); + let dest_slice: &[u8] = from_raw_parts(dest, l); + let dest_as_str: &str = str::from_utf8(dest_slice).unwrap(); assert!(dest_as_str.len() == l); } } fn main() { - copy_string("x", 1); - copy_string("", 0); -} \ No newline at end of file + // Verification fails for both of these cases. + copy_string("x", 1); + copy_string("", 0); +} diff --git a/src/test/cbmc/Strings/copy_empty_string_by_ref.rs b/src/test/cbmc/Strings/copy_empty_string_by_ref.rs index 43d6c810b8b7..6df0193e54aa 100644 --- a/src/test/cbmc/Strings/copy_empty_string_by_ref.rs +++ b/src/test/cbmc/Strings/copy_empty_string_by_ref.rs @@ -1,13 +1,13 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// Make sure we can handle implicit memcpy on the empty string +// Make sure we can handle implicit memcpy on the empty string fn take_string_ref(s: &str, l: usize) { assert!(s.len() == l) } fn main() { - take_string_ref(&"x".to_string(), 1); - take_string_ref(&"".to_string(), 0); -} \ No newline at end of file + take_string_ref(&"x".to_string(), 1); + take_string_ref(&"".to_string(), 0); +}