From 5d64679463ec74df0415c1fcf701b098fd5af96e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 30 Apr 2024 22:35:51 +0200 Subject: [PATCH] Do not assume that ZST-typed symbols refer to unique objects (#3134) The Rust specification does not guarantee that ZST-typed symbols are backed by unique objects, and `rustc` appears to make use of this as can be demonstrated for both locals and statics. For parameters no such example has been found, but as there remains a lack of a guarantee we err on the safe side. Resolves: #3129 --- .../codegen/intrinsic.rs | 32 ++++++++++----- .../codegen_cprover_gotoc/codegen/place.rs | 39 +++++++++++++++++-- library/kani/src/mem.rs | 33 ++++------------ .../function-contract/valid_ptr.expected | 2 +- tests/expected/zst/expected | 4 ++ tests/expected/zst/main.rs | 19 +++++++++ tests/kani/Closure/zst_param.rs | 3 +- tests/kani/MemPredicates/thin_ptr_validity.rs | 2 +- 8 files changed, 92 insertions(+), 42 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/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/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index d24e5448c595..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, 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,8 +655,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 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, + ); + 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. + 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/library/kani/src/mem.rs b/library/kani/src/mem.rs index 43062ebed6a1..b857247021ec 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -61,25 +61,18 @@ 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 { + // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be + // stubbed. 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 { @@ -256,18 +249,6 @@ mod tests { assert_valid_ptr(vec_ptr); } - #[test] - #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")] - fn test_dangling_char() { - test_dangling_of_t::(); - } - - #[test] - #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")] - fn test_dangling_slice() { - test_dangling_of_t::<&str>(); - } - #[test] #[should_panic(expected = "Expected valid pointer, but found `null`")] fn test_null_fat_ptr() { 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/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..587e2608c870 --- /dev/null +++ b/tests/expected/zst/main.rs @@ -0,0 +1,19 @@ +// 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); + +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 } +} 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); 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); }