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..0258d412ba9c --- /dev/null +++ b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic.rs @@ -0,0 +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 explicit copy_nonoverlapping on empty string + +#![feature(rustc_private)] + +extern crate libc; + +use std::mem::size_of; +use std::ptr::copy_nonoverlapping; +use std::slice::from_raw_parts; +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() { + 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 new file mode 100644 index 000000000000..cc56426c6c05 --- /dev/null +++ b/src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fixme.rs @@ -0,0 +1,44 @@ +// 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 + +// 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 +// [...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::mem::size_of; +use std::ptr::copy_nonoverlapping; +use std::slice::from_raw_parts; +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); + + // 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(); + assert!(dest_as_str.len() == l); + } +} + +fn main() { + // 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 new file mode 100644 index 000000000000..6df0193e54aa --- /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); +}