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