From ac1f63aaf66813a225fe5b16a72527c95227526c Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 28 Jan 2025 16:20:31 -0800
Subject: [PATCH] Fix missing function declaration issue

In cases where a function pointer is created, but its value is never
used, Kani crashes due to missing function declaration.

For now, collect any instance that has its address taken even if its
never used.

Fixes #3799
---
 kani-compiler/src/kani_middle/reachability.rs | 16 +++++++++++
 tests/kani/CodegenMisc/missing_mut_fn.rs      | 27 +++++++++++++++++++
 2 files changed, 43 insertions(+)
 create mode 100644 tests/kani/CodegenMisc/missing_mut_fn.rs

diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index dea7cca60844..2267af56a684 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -470,6 +470,22 @@ impl MirVisitor for MonoItemsFnCollector<'_, '_> {
 
         self.super_terminator(terminator, location);
     }
+
+    /// Collect any function definition that may occur as a type.
+    ///
+    /// The codegen stage will require the definition to be available.
+    /// This is a conservative approach, since there are cases where the function is never
+    /// actually used, so we don't need the body.
+    ///
+    /// Another alternative would be to lazily declare functions, but it would require a bigger
+    /// change to codegen.
+    fn visit_ty(&mut self, ty: &Ty, _: Location) {
+        if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = ty.kind() {
+            let instance = Instance::resolve(def, &args).unwrap();
+            self.collect_instance(instance, true);
+        }
+        self.super_ty(ty);
+    }
 }
 
 fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty) {
diff --git a/tests/kani/CodegenMisc/missing_mut_fn.rs b/tests/kani/CodegenMisc/missing_mut_fn.rs
new file mode 100644
index 000000000000..ae7bfe753bf0
--- /dev/null
+++ b/tests/kani/CodegenMisc/missing_mut_fn.rs
@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Ensure Kani can codegen code with a pointer to a function that is never used
+//! See <https://github.com/model-checking/kani/issues/3799> for more details.
+fn foo<F: Fn()>(_func: &mut F) {}
+fn foo_dyn(_func: &mut dyn Fn()) {}
+
+#[kani::proof]
+fn check_foo() {
+    fn f() {}
+
+    foo(&mut f);
+}
+
+#[kani::proof]
+fn check_foo_dyn() {
+    fn f() {}
+
+    foo_dyn(&mut f);
+}
+
+#[kani::proof]
+fn check_foo_unused() {
+    fn f() {}
+
+    let ptr = &mut f;
+}