Proof harness crashes when verifying a function with a `&mut FnMut` argument

[BusyBeaver-42]

Context: The crash does not happen on every harness verifying a function with a &mut F argument where F: FnMut. For instance, I wrote several such harnesses here that do not trigger a crash. I first encountered this crash while using proof on insertion_sort_shift_left with stub_verified(insert_tail). However, if I remove stub_verified(insert_tail) then kani does not crash.

I tried this code:

fn foo<F>(_: &mut F) {}

#[proof]
fn check_foo() {
    fn f() {}

    foo(&mut f);
}

using the following command line invocation:

RUST_BACKTRACE=1 cargo kani

with Kani version: cargo-kani 0.57.0

Kani crashed with the following error and backtrace.

thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:641:36:
Function `_RNvNvCs552KuoMe0Qq_9smallsort9check_foo1f` should've been declared before usage
stack backtrace:
error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:641:36:
                                Function `_RNvNvCs552KuoMe0Qq_9smallsort9check_foo1f` should've been declared before usage.

   0: rust_begin_unwind
   1: core::panicking::panic_fmt
   2: kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_func_symbol
   3: kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_fn_item
   4: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_local_fndef
   5: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_local
   6: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place_stable
   7: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place_ref_stable
   8: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue_stable
   9: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement
  10: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
  11: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
  12: scoped_tls::ScopedKey<T>::set
  13: rustc_smir::rustc_internal::init
  14: scoped_tls::ScopedKey<T>::set
  15: rustc_smir::rustc_internal::run
  16: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
  17: <rustc_interface::queries::Linker>::codegen_and_build_linker
  18: rustc_interface::interface::run_compiler::<(), rustc_driver_impl::run_compiler::{closure#0}>::{closure#1}
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: check_foo
_RNvCs552KuoMe0Qq_9smallsort9check_foo
[Kani] current codegen location: Loc { file: "src/lib.rs", function: None, start_line: 4, start_col: Some(1), end_line: 4, end_col: Some(15), pragmas: [] }
error: could not compile `smallsort` (lib)

Caused by:
  process didn't exit successfully: `/home/busybeaver42/.kani/kani-0.57.0/bin/kani-compiler --crate-name smallsort --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=209 --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs)' --check-cfg 'cfg(feature, values())' -C metadata=db6192a70326ea4d -C extra-filename=-541997cde10067f2 --out-dir /home/busybeaver42/projects/smallsort/target/kani/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=/home/busybeaver42/projects/smallsort/target/kani/x86_64-unknown-linux-gnu/debug/incremental -L dependency=/home/busybeaver42/projects/smallsort/target/kani/x86_64-unknown-linux-gnu/debug/deps -L dependency=/home/busybeaver42/projects/smallsort/target/kani/debug/deps -Cllvm-args=--reachability=harnesses -C overflow-checks=on -Z unstable-options -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -Z always-encode-mir --cfg=kani -Z 'crate-attr=feature(register_tool)' -Z 'crate-attr=register_tool(kanitool)' --sysroot /home/busybeaver42/.kani/kani-0.57.0 -L /home/busybeaver42/.kani/kani-0.57.0/lib --extern kani --extern 'noprelude:std=/home/busybeaver42/.kani/kani-0.57.0/lib/libstd.rlib' -C panic=abort -C symbol-mangling-version=v0 -Z panic_abort_tests=yes -Z mir-enable-passes=-RemoveStorageMarkers '--check-cfg=cfg(kani)' --kani-compiler '-Cllvm-args=--check-version=0.57.0 --log-level=warn --assertion-reach-checks'` (exit status: 101)
error: Failed to compile `smallsort` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:641:36:
                                Function `_RNvNvCs552KuoMe0Qq_9smallsort9check_foo1f` should've been declared before usage.

[celinval]

I believe the problem is that the function itself is never used but its type is. Kani's reachability algorithm doesn't include unused functions.