Treat pointer and Box locals of function items as ordinary variables

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -365,31 +365,15 @@ impl GotocCtx<'_, '_> {
     /// If a local is a function definition, ignore the local variable name and
     /// generate a function call based on the def id.
     ///
-    /// 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 and we
+    /// can use its singleton instead of a named variable.
     ///
-    /// 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<Expr> {
         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<T>` 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,
         }
     }

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

@@ -93,37 +93,6 @@ impl GotocCtx<'_, '_> {
         self.peel_ptr_wrappers(expr)
     }
 
-    /// `Box<T>` 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::<Vec<_>>();
-
-        // `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.

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);
 }

tests/kani/FunctionSymbols/fn_item_address.rs

@@ -0,0 +1,35 @@
+// 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 <https://github.com/model-checking/kani/issues/2255>.
+
+fn foo() -> u32 {
+    42
+}
+
+fn null_of<T>(_: 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() {
+    assert!(!null_of(foo).is_null());
+}