From 6422c9c33d8805fbf8150ced2ba0d0a42eb68ce8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 8 Apr 2024 14:14:40 +0000 Subject: [PATCH 1/7] 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: #3129 --- .../codegen_cprover_gotoc/codegen/function.rs | 5 ++- .../codegen_cprover_gotoc/codegen/place.rs | 31 +++++++++++++++++-- .../codegen_cprover_gotoc/context/goto_ctx.rs | 8 ++--- tests/expected/zst/expected | 4 +++ tests/expected/zst/main.rs | 15 +++++++++ 5 files changed, 52 insertions(+), 11 deletions(-) create mode 100644 tests/expected/zst/expected create mode 100644 tests/expected/zst/main.rs 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 } +} From 822f0075ebd4bbd70d143e64e57594cf911c6f68 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 10 Apr 2024 09:20:10 +0000 Subject: [PATCH 2/7] 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); From 7e5b38131be016afdc181856d6848f897f912705 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 10 Apr 2024 09:23:36 +0000 Subject: [PATCH 3/7] Formatting --- kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index d35810fd11ff..a16dd616e7c0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -644,9 +644,7 @@ impl<'tcx> GotocCtx<'tcx> { if self.use_thin_pointer_stable(place_ty) { // For ZST objects rustc does not necessarily generate individual objects. let need_not_be_unique = match projection.goto_expr.value() { - ExprValue::Symbol { .. } => { - self.is_zst_stable(place_ty) - } + ExprValue::Symbol { .. } => self.is_zst_stable(place_ty), _ => false, }; let address_of = projection.goto_expr.address_of(); From e098d8a0f73b87a8b8ddc8fa179a6570931b31a6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 25 Apr 2024 10:25:31 +0000 Subject: [PATCH 4/7] Implement address-of-ZST as nondet integer --- .../codegen_cprover_gotoc/codegen/place.rs | 49 ++++++++++++------- library/kani/src/mem.rs | 23 +++------ 2 files changed, 37 insertions(+), 35 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 9e785910ea0f..56b7da2e7628 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, ExprValue, Location, Type}; +use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type}; use rustc_middle::ty::layout::LayoutOf; use rustc_smir::rustc_internal; use rustc_target::abi::{TagEncoding, Variants}; @@ -636,6 +636,14 @@ impl<'tcx> GotocCtx<'tcx> { } } + fn is_zst_object(&self, expr: &Expr) -> bool { + match expr.value() { + ExprValue::Symbol { .. } => expr.typ().sizeof(&self.symbol_table) == 0, + ExprValue::Member { lhs, .. } => self.is_zst_object(lhs), + _ => false, + } + } + /// Codegen the reference to a given place. /// We currently have a somewhat weird way of handling ZST. /// - For `*(&T)` where `T: Unsized`, the projection's `goto_expr` is a thin pointer, so we @@ -647,25 +655,28 @@ 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 ZST objects rustc does not necessarily generate individual objects. - let need_not_be_unique = match projection.goto_expr.value() { - ExprValue::Symbol { .. } => self.is_zst_stable(place_ty), - _ => false, - }; - let address_of = projection.goto_expr.address_of(); - 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( - global_zst_name, - false, - zst_typ, - Location::none(), - |_, _| None, // zero-sized, so no initialization necessary + // For ZST objects rustc does not necessarily generate any actual objects. + let need_not_be_an_object = self.is_zst_object(&projection.goto_expr); + let address_of = projection.goto_expr.clone().address_of(); + if need_not_be_an_object { + // Create a non-deterministic numeric value, assume it is non-zero and (when + // interpreted as an address) of proper alignment for the type, and cast that + // numeric value to a pointer type. + let loc = projection.goto_expr.location(); + let (var, decl) = + self.decl_temp_variable(Type::size_t(), Some(Type::size_t().nondet()), *loc); + let assume_non_zero = + Stmt::assume(var.clone().neq(Expr::int_constant(0, var.typ().clone())), *loc); + let layout = self.layout_of_stable(place_ty); + let alignment = Expr::int_constant(layout.align.abi.bytes(), var.typ().clone()); + let assume_aligned = Stmt::assume( + var.clone().rem(alignment).eq(Expr::int_constant(0, var.typ().clone())), + *loc, ); - Type::bool().nondet().ternary( - address_of.clone(), - global_zst_object.address_of().cast_to(address_of.typ().clone()), + let cast_to_pointer_type = var.cast_to(address_of.typ().clone()).as_stmt(*loc); + Expr::statement_expression( + vec![decl, assume_non_zero, assume_aligned, cast_to_pointer_type], + address_of.typ().clone(), ) } else { // Just return the address of the place dereferenced. diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index 43062ebed6a1..704b6ebadd4d 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -61,25 +61,16 @@ where crate::assert(!ptr.is_null(), "Expected valid pointer, but found `null`"); let (thin_ptr, metadata) = ptr.to_raw_parts(); - can_read(&metadata, thin_ptr) -} - -fn can_read(metadata: &M, data_ptr: *const ()) -> bool -where - M: PtrProperties, - T: ?Sized, -{ - let marker = Internal; - let sz = metadata.pointee_size(marker); - if metadata.dangling(marker) as *const _ == data_ptr { - crate::assert(sz == 0, "Dangling pointer is only valid for zero-sized access") + let sz = metadata.pointee_size(Internal); + if sz == 0 { + true // ZST pointers are always valid } else { crate::assert( - is_read_ok(data_ptr, sz), + is_read_ok(thin_ptr, sz), "Expected valid pointer, but found dangling pointer", ); + true } - true } mod private { @@ -257,13 +248,13 @@ mod tests { } #[test] - #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")] + #[should_panic(expected = "Expected valid pointer, but found dangling pointer")] fn test_dangling_char() { test_dangling_of_t::(); } #[test] - #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")] + #[should_panic(expected = "Expected valid pointer, but found dangling pointer")] fn test_dangling_slice() { test_dangling_of_t::<&str>(); } From 1c75d723a63f23c07f486d95942f98295540603b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 26 Apr 2024 08:32:59 +0000 Subject: [PATCH 5/7] Remove tests that are no longer feasible --- library/kani/src/mem.rs | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index 704b6ebadd4d..b857247021ec 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -65,6 +65,8 @@ where if sz == 0 { true // ZST pointers are always valid } else { + // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be + // stubbed. crate::assert( is_read_ok(thin_ptr, sz), "Expected valid pointer, but found dangling pointer", @@ -247,18 +249,6 @@ mod tests { assert_valid_ptr(vec_ptr); } - #[test] - #[should_panic(expected = "Expected valid pointer, but found dangling pointer")] - fn test_dangling_char() { - test_dangling_of_t::(); - } - - #[test] - #[should_panic(expected = "Expected valid pointer, but found dangling pointer")] - fn test_dangling_slice() { - test_dangling_of_t::<&str>(); - } - #[test] #[should_panic(expected = "Expected valid pointer, but found `null`")] fn test_null_fat_ptr() { From 1356d23e580c107471bcfb04f6c8271b2249b7ba Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 26 Apr 2024 08:36:10 +0000 Subject: [PATCH 6/7] Copyright and comment in test --- tests/expected/zst/main.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/expected/zst/main.rs b/tests/expected/zst/main.rs index b53b50b5910f..587e2608c870 100644 --- a/tests/expected/zst/main.rs +++ b/tests/expected/zst/main.rs @@ -1,3 +1,7 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This example demonstrates that rustc may choose not to allocate unique locations to ZST objects. #[repr(C)] #[derive(Copy, Clone)] struct Z(i8, i64); From 37a0a08e13dd8818eaa8aa3cfb859c035b007cc8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 26 Apr 2024 10:04:31 +0000 Subject: [PATCH 7/7] Fix raw_eq and tests --- .../codegen/intrinsic.rs | 32 +++++++++++++------ .../function-contract/valid_ptr.expected | 2 +- tests/kani/MemPredicates/thin_ptr_validity.rs | 2 +- 3 files changed, 24 insertions(+), 12 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 8a61d46ed518..4d201a6f8cc4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1221,7 +1221,9 @@ impl<'tcx> GotocCtx<'tcx> { // `raw_eq` determines whether the raw bytes of two values are equal. // https://doc.rust-lang.org/core/intrinsics/fn.raw_eq.html // - // The implementation below calls `memcmp` and returns equal if the result is zero. + // The implementation below calls `memcmp` and returns equal if the result is zero, and + // immediately returns zero when ZSTs are compared to mimic what compare_bytes and our memcmp + // hook do. // // TODO: It's UB to call `raw_eq` if any of the bytes in the first or second // arguments are uninitialized. At present, we cannot detect if there is @@ -1240,13 +1242,17 @@ impl<'tcx> GotocCtx<'tcx> { let dst = fargs.remove(0).cast_to(Type::void_pointer()); let val = fargs.remove(0).cast_to(Type::void_pointer()); let layout = self.layout_of_stable(ty); - let sz = Expr::int_constant(layout.size.bytes(), Type::size_t()) - .with_size_of_annotation(self.codegen_ty_stable(ty)); - let e = BuiltinFn::Memcmp - .call(vec![dst, val, sz], loc) - .eq(Type::c_int().zero()) - .cast_to(Type::c_bool()); - self.codegen_expr_to_place_stable(p, e) + if layout.size.bytes() == 0 { + self.codegen_expr_to_place_stable(p, Expr::int_constant(1, Type::c_bool())) + } else { + let sz = Expr::int_constant(layout.size.bytes(), Type::size_t()) + .with_size_of_annotation(self.codegen_ty_stable(ty)); + let e = BuiltinFn::Memcmp + .call(vec![dst, val, sz], loc) + .eq(Type::c_int().zero()) + .cast_to(Type::c_bool()); + self.codegen_expr_to_place_stable(p, e) + } } // This is an operation that is primarily relevant for stacked borrow @@ -1856,8 +1862,14 @@ impl<'tcx> GotocCtx<'tcx> { "`dst` must be properly aligned", loc, ); - let expr = dst.dereference().assign(src, loc); - Stmt::block(vec![align_check, expr], loc) + let deref = dst.dereference(); + if deref.typ().sizeof(&self.symbol_table) == 0 { + // do not attempt to dereference (and assign) a ZST + align_check + } else { + let expr = deref.assign(src, loc); + Stmt::block(vec![align_check, expr], loc) + } } /// Sets `count * size_of::()` bytes of memory starting at `dst` to `val` diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index a9dc8dd5992d..f45cb4e2e826 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -1,5 +1,5 @@ Checking harness pre_condition::harness_invalid_ptr... -Failed Checks: Dangling pointer is only valid for zero-sized access +Failed Checks: Expected valid pointer, but found dangling pointer Checking harness pre_condition::harness_stack_ptr... VERIFICATION:- SUCCESSFUL diff --git a/tests/kani/MemPredicates/thin_ptr_validity.rs b/tests/kani/MemPredicates/thin_ptr_validity.rs index 638b7e1d1fc8..49e9c403cda8 100644 --- a/tests/kani/MemPredicates/thin_ptr_validity.rs +++ b/tests/kani/MemPredicates/thin_ptr_validity.rs @@ -46,10 +46,10 @@ mod invalid_access { } #[kani::proof] - #[kani::should_panic] pub fn check_invalid_zst() { let raw_ptr: *const [char; 0] = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) } as *const _; + // ZST pointer are always valid assert_valid_ptr(raw_ptr); }