From 822f0075ebd4bbd70d143e64e57594cf911c6f68 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 10 Apr 2024 09:20:10 +0000 Subject: [PATCH] Parameters are not to be treated different --- .../src/codegen_cprover_gotoc/codegen/function.rs | 5 +++-- kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs | 9 ++++----- .../src/codegen_cprover_gotoc/context/goto_ctx.rs | 8 +++++--- tests/kani/Closure/zst_param.rs | 3 ++- 4 files changed, 14 insertions(+), 11 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index ec3cb357948f..d55696bfdc87 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/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. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 2dc93f76f3ab..d35810fd11ff 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/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( 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 095f907228a4..3a6501d544d8 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()) + 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) diff --git a/tests/kani/Closure/zst_param.rs b/tests/kani/Closure/zst_param.rs index 3eee1e5ac672..7a93619a9e16 100644 --- a/tests/kani/Closure/zst_param.rs +++ b/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);