Parameters are not to be treated different

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

@@ -34,10 +34,11 @@ 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);
+ .with_is_parameter((lc > 0 && lc <= num_args) && !self.is_zst_stable(ldata.ty));
  let sym_e = sym.to_expr();
  self.symbol_table.insert(sym);
 
@@ -175,7 +176,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(true);
+ .with_is_parameter(!self.is_zst_stable(*arg_t));
  // 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

@@ -642,16 +642,15 @@ 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) {
- // For non-parameter objects with ZST rustc does not necessarily generate
- // individual objects.
+ // For ZST objects 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
+ ExprValue::Symbol { .. } => {
+ self.is_zst_stable(place_ty)
  }
  _ => false,
  };
  let address_of = projection.goto_expr.address_of();
- if need_not_be_unique && self.is_zst_stable(place_ty) {
+ if need_not_be_unique {
  let global_zst_name = "__kani_zst_object";
  let zst_typ = self.codegen_ty_stable(place_ty);
  let global_zst_object = self.ensure_global_var(

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())
+ self.gen_stack_variable(c, fname, "var", t, Location::none(), false)
  }
 
  /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable
@@ -149,10 +149,11 @@ 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);
+ let symbol = Symbol::variable(name, base_name, t, loc).with_is_parameter(is_param);
  self.symbol_table.insert(symbol.clone());
  symbol
  }
@@ -166,7 +167,8 @@ 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).to_expr();
+ let var =
+ self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc, false).to_expr();
  let value = value.or_else(|| self.codegen_default_initializer(&var));
  let decl = Stmt::decl(var.clone(), value, loc);
  (var, decl)

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