Do not assume that ZST-typed symbols refer to unique objects (model-c…

…hecking#3134)

The Rust specification does not guarantee that ZST-typed symbols are
backed by unique objects, and `rustc` appears to make use of this as can
be demonstrated for both locals and statics. For parameters no such
example has been found, but as there remains a lack of a guarantee we
err on the safe side.

Resolves: model-checking#3129

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -1221,7 +1221,9 @@ impl<'tcx> GotocCtx<'tcx> {
     // `raw_eq` determines whether the raw bytes of two values are equal.
     // https://doc.rust-lang.org/core/intrinsics/fn.raw_eq.html
     //
-    // The implementation below calls `memcmp` and returns equal if the result is zero.
+    // The implementation below calls `memcmp` and returns equal if the result is zero, and
+    // immediately returns zero when ZSTs are compared to mimic what compare_bytes and our memcmp
+    // hook do.
     //
     // TODO: It's UB to call `raw_eq` if any of the bytes in the first or second
     // arguments are uninitialized. At present, we cannot detect if there is
@@ -1240,13 +1242,17 @@ impl<'tcx> GotocCtx<'tcx> {
         let dst = fargs.remove(0).cast_to(Type::void_pointer());
         let val = fargs.remove(0).cast_to(Type::void_pointer());
         let layout = self.layout_of_stable(ty);
-        let sz = Expr::int_constant(layout.size.bytes(), Type::size_t())
-            .with_size_of_annotation(self.codegen_ty_stable(ty));
-        let e = BuiltinFn::Memcmp
-            .call(vec![dst, val, sz], loc)
-            .eq(Type::c_int().zero())
-            .cast_to(Type::c_bool());
-        self.codegen_expr_to_place_stable(p, e)
+        if layout.size.bytes() == 0 {
+            self.codegen_expr_to_place_stable(p, Expr::int_constant(1, Type::c_bool()))
+        } else {
+            let sz = Expr::int_constant(layout.size.bytes(), Type::size_t())
+                .with_size_of_annotation(self.codegen_ty_stable(ty));
+            let e = BuiltinFn::Memcmp
+                .call(vec![dst, val, sz], loc)
+                .eq(Type::c_int().zero())
+                .cast_to(Type::c_bool());
+            self.codegen_expr_to_place_stable(p, e)
+        }
     }
 
     // This is an operation that is primarily relevant for stacked borrow
@@ -1856,8 +1862,14 @@ impl<'tcx> GotocCtx<'tcx> {
             "`dst` must be properly aligned",
             loc,
         );
-        let expr = dst.dereference().assign(src, loc);
-        Stmt::block(vec![align_check, expr], loc)
+        let deref = dst.dereference();
+        if deref.typ().sizeof(&self.symbol_table) == 0 {
+            // do not attempt to dereference (and assign) a ZST
+            align_check
+        } else {
+            let expr = deref.assign(src, loc);
+            Stmt::block(vec![align_check, expr], loc)
+        }
     }
 
     /// Sets `count * size_of::<T>()` bytes of memory starting at `dst` to `val`

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -11,7 +11,7 @@ use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented;
-use cbmc::goto_program::{Expr, Location, Type};
+use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{TagEncoding, Variants};
@@ -636,6 +636,14 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    fn is_zst_object(&self, expr: &Expr) -> bool {
+        match expr.value() {
+            ExprValue::Symbol { .. } => expr.typ().sizeof(&self.symbol_table) == 0,
+            ExprValue::Member { lhs, .. } => self.is_zst_object(lhs),
+            _ => false,
+        }
+    }
+
     /// Codegen the reference to a given place.
     /// We currently have a somewhat weird way of handling ZST.
     /// - For `*(&T)` where `T: Unsized`, the projection's `goto_expr` is a thin pointer, so we
@@ -647,8 +655,33 @@ impl<'tcx> GotocCtx<'tcx> {
         let projection =
             unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place));
         if self.use_thin_pointer_stable(place_ty) {
-            // Just return the address of the place dereferenced.
-            projection.goto_expr.address_of()
+            // For ZST objects rustc does not necessarily generate any actual objects.
+            let need_not_be_an_object = self.is_zst_object(&projection.goto_expr);
+            let address_of = projection.goto_expr.clone().address_of();
+            if need_not_be_an_object {
+                // Create a non-deterministic numeric value, assume it is non-zero and (when
+                // interpreted as an address) of proper alignment for the type, and cast that
+                // numeric value to a pointer type.
+                let loc = projection.goto_expr.location();
+                let (var, decl) =
+                    self.decl_temp_variable(Type::size_t(), Some(Type::size_t().nondet()), *loc);
+                let assume_non_zero =
+                    Stmt::assume(var.clone().neq(Expr::int_constant(0, var.typ().clone())), *loc);
+                let layout = self.layout_of_stable(place_ty);
+                let alignment = Expr::int_constant(layout.align.abi.bytes(), var.typ().clone());
+                let assume_aligned = Stmt::assume(
+                    var.clone().rem(alignment).eq(Expr::int_constant(0, var.typ().clone())),
+                    *loc,
+                );
+                let cast_to_pointer_type = var.cast_to(address_of.typ().clone()).as_stmt(*loc);
+                Expr::statement_expression(
+                    vec![decl, assume_non_zero, assume_aligned, cast_to_pointer_type],
+                    address_of.typ().clone(),
+                )
+            } else {
+                // Just return the address of the place dereferenced.
+                address_of
+            }
         } else if place_ty == pointee_type(self.local_ty_stable(place.local)).unwrap() {
             // Just return the fat pointer if this is a simple &(*local).
             projection.fat_ptr_goto_expr.unwrap()

library/kani/src/mem.rs

@@ -61,25 +61,18 @@ where
     crate::assert(!ptr.is_null(), "Expected valid pointer, but found `null`");
 
     let (thin_ptr, metadata) = ptr.to_raw_parts();
-    can_read(&metadata, thin_ptr)
-}
-
-fn can_read<M, T>(metadata: &M, data_ptr: *const ()) -> bool
-where
-    M: PtrProperties<T>,
-    T: ?Sized,
-{
-    let marker = Internal;
-    let sz = metadata.pointee_size(marker);
-    if metadata.dangling(marker) as *const _ == data_ptr {
-        crate::assert(sz == 0, "Dangling pointer is only valid for zero-sized access")
+    let sz = metadata.pointee_size(Internal);
+    if sz == 0 {
+        true // ZST pointers are always valid
     } else {
+        // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be
+        // stubbed.
         crate::assert(
-            is_read_ok(data_ptr, sz),
+            is_read_ok(thin_ptr, sz),
             "Expected valid pointer, but found dangling pointer",
         );
+        true
     }
-    true
 }
 
 mod private {
@@ -256,18 +249,6 @@ mod tests {
         assert_valid_ptr(vec_ptr);
     }
 
-    #[test]
-    #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")]
-    fn test_dangling_char() {
-        test_dangling_of_t::<char>();
-    }
-
-    #[test]
-    #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")]
-    fn test_dangling_slice() {
-        test_dangling_of_t::<&str>();
-    }
-
     #[test]
     #[should_panic(expected = "Expected valid pointer, but found `null`")]
     fn test_null_fat_ptr() {

tests/expected/function-contract/valid_ptr.expected

@@ -1,5 +1,5 @@
 Checking harness pre_condition::harness_invalid_ptr...
-Failed Checks: Dangling pointer is only valid for zero-sized access
+Failed Checks: Expected valid pointer, but found dangling pointer
 
 Checking harness pre_condition::harness_stack_ptr...
 VERIFICATION:- SUCCESSFUL

tests/expected/zst/expected

@@ -0,0 +1,4 @@
+Status: FAILURE\
+Description: "dereference failure: pointer NULL"
+
+VERIFICATION:- FAILED

tests/expected/zst/main.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This example demonstrates that rustc may choose not to allocate unique locations to ZST objects.
+#[repr(C)]
+#[derive(Copy, Clone)]
+struct Z(i8, i64);
+
+struct Y;
+
+#[kani::proof]
+fn test_z() -> Z {
+    let m = Y;
+    let n = Y;
+    let zz = Z(1, -1);
+
+    let ptr: *const Z = if &n as *const _ == &m as *const _ { std::ptr::null() } else { &zz };
+    unsafe { *ptr }
+}

tests/kani/Closure/zst_param.rs

@@ -17,7 +17,8 @@ fn check_zst_param() {
     let input = kani::any();
     let closure = |a: Void, out: usize, b: Void| {
         kani::cover!();
-        assert!(&a as *const Void != &b as *const Void, "Should succeed");
+        assert!(&a as *const Void != std::ptr::null(), "Should succeed");
+        assert!(&b as *const Void != std::ptr::null(), "Should succeed");
         out
     };
     let output = invoke(input, closure);

tests/kani/MemPredicates/thin_ptr_validity.rs

@@ -46,10 +46,10 @@ mod invalid_access {
     }
 
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_zst() {
         let raw_ptr: *const [char; 0] =
             unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) } as *const _;
+        // ZST pointer are always valid
         assert_valid_ptr(raw_ptr);
     }