Do not assume that ZST-typed symbols refer to unique objects

It seems that rustc does not necessarily create unique objects for
ZST-typed symbols, unless they are parameters.

Resolves: model-checking#3129

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

@@ -34,11 +34,10 @@ impl<'tcx> GotocCtx<'tcx> {
  let var_type = self.codegen_ty_stable(ldata.ty);
  let loc = self.codegen_span_stable(ldata.span);
  // Indices [1, N] represent the function parameters where N is the number of parameters.
- // Except that ZST fields are not included as parameters.
  let sym =
  Symbol::variable(name, base_name, var_type, self.codegen_span_stable(ldata.span))
  .with_is_hidden(!self.is_user_variable(&lc))
- .with_is_parameter((lc > 0 && lc <= num_args) && !self.is_zst_stable(ldata.ty));
+ .with_is_parameter(lc > 0 && lc <= num_args);
  let sym_e = sym.to_expr();
  self.symbol_table.insert(sym);
 
@@ -176,7 +175,7 @@ impl<'tcx> GotocCtx<'tcx> {
  let (name, base_name) = self.codegen_spread_arg_name(&lc);
  let sym = Symbol::variable(name, base_name, self.codegen_ty_stable(*arg_t), loc)
  .with_is_hidden(false)
- .with_is_parameter(!self.is_zst_stable(*arg_t));
+ .with_is_parameter(true);
  // The spread arguments are additional function paramaters that are patched in
  // They are to the function signature added in the `fn_typ` function.
  // But they were never added to the symbol table, which we currently do here.

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, Type};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{TagEncoding, Variants};
@@ -642,8 +642,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 non-parameter objects with ZST rustc does not necessarily generate
+ // individual objects.
+ let need_not_be_unique = match projection.goto_expr.value() {
+ ExprValue::Symbol { identifier } => {
+ !self.symbol_table.lookup(*identifier).unwrap().is_parameter
+ }
+ _ => false,
+ };
+ let address_of = projection.goto_expr.address_of();
+ if need_not_be_unique && self.is_zst_stable(place_ty) {
+ let global_zst_name = "__kani_zst_object";
+ let zst_typ = self.codegen_ty_stable(place_ty);
+ let global_zst_object = self.ensure_global_var(
+ global_zst_name,
+ false,
+ zst_typ,
+ Location::none(),
+ |_, _| None, // zero-sized, so no initialization necessary
+ );
+ Type::bool().nondet().ternary(
+ address_of.clone(),
+ global_zst_object.address_of().cast_to(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()

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -137,7 +137,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
  // Generate a Symbol Expression representing a function variable from the MIR
  pub fn gen_function_local_variable(&mut self, c: u64, fname: &str, t: Type) -> Symbol {
- self.gen_stack_variable(c, fname, "var", t, Location::none(), false)
+ self.gen_stack_variable(c, fname, "var", t, Location::none())
  }
 
  /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable
@@ -149,11 +149,10 @@ impl<'tcx> GotocCtx<'tcx> {
  prefix: &str,
  t: Type,
  loc: Location,
- is_param: bool,
  ) -> Symbol {
  let base_name = format!("{prefix}_{c}");
  let name = format!("{fname}::1::{base_name}");
- let symbol = Symbol::variable(name, base_name, t, loc).with_is_parameter(is_param);
+ let symbol = Symbol::variable(name, base_name, t, loc);
  self.symbol_table.insert(symbol.clone());
  symbol
  }
@@ -167,8 +166,7 @@ impl<'tcx> GotocCtx<'tcx> {
  loc: Location,
  ) -> (Expr, Stmt) {
  let c = self.current_fn_mut().get_and_incr_counter();
- let var =
- self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc, false).to_expr();
+ let var = self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc).to_expr();
  let value = value.or_else(|| self.codegen_default_initializer(&var));
  let decl = Stmt::decl(var.clone(), value, loc);
  (var, decl)

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,15 @@
+#[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 }
+}