diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index d55696bfdc87..ec3cb357948f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/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. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 6b764fb63365..2dc93f76f3ab 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/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() diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 3a6501d544d8..095f907228a4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/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) diff --git a/tests/expected/zst/expected b/tests/expected/zst/expected new file mode 100644 index 000000000000..bec891bea92c --- /dev/null +++ b/tests/expected/zst/expected @@ -0,0 +1,4 @@ +Status: FAILURE\ +Description: "dereference failure: pointer NULL" + +VERIFICATION:- FAILED diff --git a/tests/expected/zst/main.rs b/tests/expected/zst/main.rs new file mode 100644 index 000000000000..b53b50b5910f --- /dev/null +++ b/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 } +}