From 53013f35d8a78db685e2ce6cf95b0146df148ecb Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 29 Jan 2025 00:24:15 -0800
Subject: [PATCH] Fix missing function declaration issue (#3862)

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

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 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;
+}