Handle copy on empty str/length zero data

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());

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)
             }};
         }
 

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(_, _)

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::<u8>();
+        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);
+}

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::<u8>();
+        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);
+}

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);
+}