diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 76dc4c1b3c72..61c97979f220 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -362,34 +362,17 @@ impl GotocCtx<'_, '_> { } } - /// If a local is a function definition, ignore the local variable name and - /// generate a function call based on the def id. + /// If a local is a function definition, use the function item's singleton instead of the + /// named variable. /// - /// Note that this is finicky. A local might be a function definition, a - /// pointer to one, or a boxed pointer to one. For example, the - /// auto-generated code for Fn::call_once uses a local FnDef to call the - /// wrapped function, while the auto-generated code for Fn::call and - /// Fn::call_mut both use pointers to a FnDef. In these cases, we need to - /// generate an expression that references the existing FnDef rather than - /// a named variable. + /// For example, the auto-generated code for Fn::call_once uses a local FnDef to call the + /// wrapped function. A function item is zero-sized, so every value of it is the same. /// - /// Recursively finds the actual FnDef from a pointer or box. + /// A pointer to a function item, or a `Box` of one, is not zero-sized: it is an ordinary + /// variable that holds whatever address was assigned to it. fn codegen_local_fndef(&mut self, ty: Ty, loc: Location) -> Option { match ty.kind() { - // A local that is itself a FnDef, like Fn::call_once TyKind::RigidTy(RigidTy::FnDef(def, args)) => Some(self.codegen_fndef(def, &args, loc)), - // A local can be pointer to a FnDef, like Fn::call and Fn::call_mut - TyKind::RigidTy(RigidTy::RawPtr(inner, _)) => self - .codegen_local_fndef(inner, loc) - .map(|f| if f.can_take_address_of() { f.address_of() } else { f }), - // A local can be a boxed function pointer - TyKind::RigidTy(RigidTy::Adt(def, args)) if def.is_box() => { - let boxed_ty = self.codegen_ty_stable(ty); - // The type of `T` for `Box` can be derived from the first definition args. - let inner_ty = args.0[0].ty().unwrap(); - self.codegen_local_fndef(*inner_ty, loc) - .map(|f| self.box_value(f.address_of(), boxed_ty)) - } _ => None, } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs index 4c5e48362907..e6b48d3b5a55 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs @@ -68,50 +68,7 @@ impl GotocCtx<'_, '_> { } } -/// Members traverse path to get to the raw pointer of a box (b.0.pointer.pointer). -const RAW_PTR_FROM_BOX: [&str; 3] = ["0", "pointer", "pointer"]; - impl GotocCtx<'_, '_> { - /// `Box` initializer - /// - /// Traverse over the Box representation and only initialize the raw_ptr field. All other - /// members are left uninitialized. - /// `boxed_type` is the type of the resulting expression - pub fn box_value(&self, boxed_value: Expr, boxed_type: Type) -> Expr { - self.assert_is_rust_box_like(&boxed_type); - tracing::debug!(?boxed_type, ?boxed_value, "box_value"); - let mut inner_type = boxed_type; - let type_members = RAW_PTR_FROM_BOX - .iter() - .map(|name| { - let outer_type = inner_type.clone(); - inner_type = outer_type.lookup_field_type(name, &self.symbol_table).unwrap(); - (*name, outer_type) - }) - .collect::>(); - - // `inner_type` is now the innermost field's type, which wraps the raw pointer in a - // pattern-type struct. Rebuild that wrapping so the value matches the field. - let boxed_value = self.codegen_ptr_in_wrappers(inner_type, boxed_value); - - type_members.iter().rfold(boxed_value, |value, (name, typ)| { - Expr::struct_expr_with_nondet_fields( - typ.clone(), - btree_string_map![(*name, value),], - &self.symbol_table, - ) - }) - } - - /// Best effort check if the struct represents a rust `std::alloc::Global` - fn assert_is_rust_global_alloc_like(&self, t: &Type) { - // TODO: A `std::alloc::Global` appears to be an empty struct, in the cases we've seen. - // Is there something smarter we can do here? - assert!(t.is_struct_like()); - let components = t.lookup_components(&self.symbol_table).unwrap(); - assert_eq!(components.len(), 0); - } - /// Best effort check if the struct represents a rust `std::marker::PhantomData` pub fn assert_is_rust_phantom_data_like(&self, t: &Type) { // TODO: A `std::marker::PhantomData` appears to be an empty struct, in the cases we've seen. @@ -171,91 +128,6 @@ impl GotocCtx<'_, '_> { } expr } - - /// Best effort check if the struct represents a Rust `Box`. May return false positives. - fn assert_is_rust_box_like(&self, t: &Type) { - // struct std::boxed::Box<[u8; 8]>::15334369982748499855 - // { - // // 1 - // struct std::alloc::Global::13633191317886109837 1; - // // 0 - // struct std::ptr::Unique<[u8; 8]>::14713681870393313245 0; - // }; - assert!(t.is_struct_like()); - let components = t.lookup_components(&self.symbol_table).unwrap(); - assert_eq!(components.len(), 2); - for c in components { - match c.name().to_string().as_str() { - "0" => self.assert_is_rust_unique_pointer_like(&c.typ()), - "1" => self.assert_is_rust_global_alloc_like(&c.typ()), - _ => panic!("Unexpected component {} in {t:?}", c.name()), - } - } - } - - /// Checks if the struct represents a Rust `std::ptr::Unique` - fn assert_is_rust_unique_pointer_like(&self, t: &Type) { - // struct std::ptr::Unique<[u8; 8]>::14713681870393313245 - // { - // // _marker - // struct std::marker::PhantomData<[u8; 8]>::18073278521438838603 _marker; - // // pointer - // NonNull pointer; - // }; - assert!(t.is_struct_like()); - let components = t.lookup_components(&self.symbol_table).unwrap(); - assert_eq!(components.len(), 2); - for c in components { - match c.name().to_string().as_str() { - "_marker" => self.assert_is_rust_phantom_data_like(&c.typ()), - "pointer" => self.assert_is_non_null_like(&c.typ()), - _ => panic!("Unexpected component {} in {t:?}", c.name()), - } - } - } - - /// Whether `t` is a pointer, or a chain of single-field struct wrappers around one. - /// - /// Recursing keeps this independent of how many wrappers the standard library uses, and - /// mirrors the chain that [`Self::codegen_ptr_in_wrappers`] rebuilds. - fn is_wrapped_pointer(&self, t: &Type) -> bool { - if t.is_pointer() || t.is_rust_fat_ptr(&self.symbol_table) { - return true; - } - if !t.is_struct_like() { - return false; - } - let Some(components) = t.lookup_components(&self.symbol_table) else { - return false; - }; - let fields: Vec<_> = components.iter().filter(|c| !c.is_padding()).collect(); - fields.len() == 1 && self.is_wrapped_pointer(&fields[0].typ()) - } - - /// Best effort check if the struct represents a `std::ptr::NonNull`. - /// - /// This assumes the following structure. Any changes to this will break this code. - /// ``` - /// pub struct NonNull { - /// pointer: pattern_type!(*const T is !null), - /// } - /// ``` - /// The `pointer` field is not a bare pointer: the pattern type is itself codegenned as a - /// single-field struct, so the pointer sits one level further down, c.f. - /// [`Self::codegen_ptr_in_wrappers`]. - fn assert_is_non_null_like(&self, t: &Type) { - assert!(t.is_struct_like()); - let components = t.lookup_components(&self.symbol_table).unwrap(); - let fields: Vec<_> = components.iter().filter(|c| !c.is_padding()).collect(); - assert_eq!(fields.len(), 1); - let component = fields[0]; - assert_eq!(component.name().to_string().as_str(), "pointer"); - assert!( - self.is_wrapped_pointer(&component.typ()), - "Expected the `pointer` field of {t:?} to hold a pointer, but found {:?}", - component.typ() - ) - } } pub fn span_err(tcx: TyCtxt, span: Span, msg: String) { diff --git a/tests/kani/DynTrait/boxed_fn_item.rs b/tests/kani/DynTrait/boxed_fn_item.rs index ed9737a80316..a7b2191ecb9a 100644 --- a/tests/kani/DynTrait/boxed_fn_item.rs +++ b/tests/kani/DynTrait/boxed_fn_item.rs @@ -1,13 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --only-codegen -// -// Check that we can codegen a boxed dyn Fn built from a function item. -// A function item coerces through a zero-sized singleton, so the pointer stored in the -// box is a bare pointer to that singleton rather than one already shaped like the field. -// Codegen only: past codegen, CBMC stops in symex with -// `l2_rename_rvalues case 'address_of' not handled`, a separate problem. +// Check that we can verify a call to a boxed dyn Fn built from a function item. fn hook(x: &i32) { assert!(*x == 2); @@ -29,6 +23,6 @@ impl Hook { #[kani::proof] fn main() { - // `Hook::Custom(Box::new(hook))` reaches the same `box_value` path, so one call is enough. + // `Hook::Custom(Box::new(hook))` builds the box the same way, so one call is enough. Hook::Default.into_box()(&2); } diff --git a/tests/kani/FunctionSymbols/fn_item_address.rs b/tests/kani/FunctionSymbols/fn_item_address.rs new file mode 100644 index 000000000000..64b90b0ce17e --- /dev/null +++ b/tests/kani/FunctionSymbols/fn_item_address.rs @@ -0,0 +1,38 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks pointers to a function item. A function item is zero-sized, but a pointer to one is an +//! ordinary value that holds the address it was given. +//! See . + +fn foo() -> u32 { + 42 +} + +fn null_of(_: T) -> *const T { + core::ptr::null() +} + +/// The program from the issue: `{:p}` formats the address of the function item. +#[kani::proof] +#[allow(function_item_references)] +fn check_print_address() { + println!("{:p}", &foo); +} + +#[kani::proof] +fn check_pointer_value() { + let p: *const _ = &foo; + assert!(!p.is_null()); + assert!(null_of(foo).is_null()); +} + +/// Fails if a pointer to a function item is read as some other address than the one assigned. +#[kani::proof] +#[kani::should_panic] +fn check_null_stays_null() { + // Calling `foo` declares its symbol, so with the old code this fails on the assertion rather + // than on the #2255 crash. + assert_eq!(foo(), 42); + assert!(!null_of(foo).is_null()); +}