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