[0.65.0] ICE related to const generics when verifying Firecracker harnesses

[roypat]

Heya, recently we went to update kani from 0.60.0 to 0.65.0 in the Firecracker CI, but with the new kani version we are hitting an internal compiler error that seems to be related to some const generics (it mentioned a type parameter L, which I am assuming will be this one)

using the following command line invocation:

git clone https://github.com/firecracker-microvm/firecracker
cd firecracker
RUST_BACKTRACE=full cargo kani -Z unstable-options -Z stubbing -Z function-contracts -Z restrict-vtable -j --output-format terse --harness-timeout 40m --workspace

with Kani version: 0.65.0

I expected to see this happen: verification to succeed, as it did with kani 0.60.0 (I've tried 0.64.0 and also didn't see the ICE, but didn't wait for verification to finish because my laptop doesnt have enough memory)

Instead, this happened: Kani crashed with an internal compiler error:

error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/kani_middle/stubbing/mod.rs:62:46:
                                Const(TyConst { kind: Param(ParamConst { index: 0, name: "L" }), id: TyConstId(0) }).


thread 'rustc' panicked at kani-compiler/src/kani_middle/stubbing/mod.rs:62:46:
Const(TyConst { kind: Param(ParamConst { index: 0, name: "L" }), id: TyConstId(0) })
stack backtrace:
   0:     0x76a65ae0d5a3 - <std::sys::backtrace::BacktraceLock::print::DisplayBacktrace as core::fmt::Display>::fmt::ha068512c9c0314cf
   1:     0x76a65b602d77 - core::fmt::write::hca39e7f1c4949f2f
   2:     0x76a65ae03073 - std::io::Write::write_fmt::h05178edb38996d65
   3:     0x76a65ae0d402 - std::sys::backtrace::BacktraceLock::print::he3a0ea40b93c8704
   4:     0x76a65ae10ea7 - std::panicking::default_hook::{{closure}}::h0e31ce668f62dfb4
   5:     0x76a65ae10a0b - std::panicking::default_hook::hda7bb82674e0f884
   6:     0x57490c2d4cb4 - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::hfc48559e5d8fe491
   7:     0x57490c2d50e9 - kani_compiler::session::JSON_PANIC_HOOK::{{closure}}::{{closure}}::h120ed010f7a65dc7
   8:     0x57490c2cfa50 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::h92423f34cadccb12
   9:     0x76a65ae116ee - std::panicking::panic_with_hook::h093560016ef7e9a8
  10:     0x76a65ae113ea - std::panicking::begin_panic_handler::{{closure}}::head7a07d4d4d1698
  11:     0x76a65ae0da79 - std::sys::backtrace::__rust_end_short_backtrace::h5a08801764b60456
  12:     0x76a65ae110cd - __rustc[bdbcc5634e94d7b8]::rust_begin_unwind
  13:     0x76a6574d4ea0 - core::panicking::panic_fmt::hcb81039f1ac88573
  14:     0x76a65a806f07 - <rustc_public[51a8841c850a497b]::ty::GenericArgKind>::expect_ty
  15:     0x57490c2fd40e - kani_compiler::kani_middle::stubbing::generic_args_len_without_self::h8f43800235f98afc
  16:     0x57490c2fdc44 - kani_compiler::kani_middle::stubbing::check_compatibility::h15ed8e7eb2b0fdcb
  17:     0x57490c282412 - kani_compiler::kani_middle::codegen_units::validate_units::h61d30aa24795967c
  18:     0x57490c27d5ea - kani_compiler::kani_middle::codegen_units::CodegenUnits::new::h1fed511ee5d238f0
  19:     0x57490c217fa3 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}::h8daa829467d4e34b
  20:     0x57490c23d1ae - rustc_public::rustc_internal::init::hccd195fed7e33d02
  21:     0x57490c2b9769 - rustc_public::compiler_interface::run::h08f9edb7e4c5f315
  22:     0x57490c23d120 - rustc_public::rustc_internal::run::hcc72249900a6937e
  23:     0x57490c217219 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h0c9b0e0899150d3b
  24:     0x76a65cab3c0a - <rustc_interface[6928205aa426efe4]::queries::Linker>::codegen_and_build_linker
  25:     0x76a65cab17bc - rustc_interface[6928205aa426efe4]::passes::create_and_enter_global_ctxt::<core[7c52ce2a1de942a3]::option::Option<rustc_interface[6928205aa426efe4]::queries::Linker>, rustc_driver_impl[7f0887fb4468f064]::run_compiler::{closure#0}::{closure#2}>::{closure#2}::{closure#0}
  26:     0x76a65c8948f1 - rustc_interface[6928205aa426efe4]::interface::run_compiler::<(), rustc_driver_impl[7f0887fb4468f064]::run_compiler::{closure#0}>::{closure#1}
  27:     0x76a65c7a93c1 - std[16222f0ba70c5179]::sys::backtrace::__rust_begin_short_backtrace::<rustc_interface[6928205aa426efe4]::util::run_in_thread_with_globals<rustc_interface[6928205aa426efe4]::util::run_in_thread_pool_with_globals<rustc_interface[6928205aa426efe4]::interface::run_compiler<(), rustc_driver_impl[7f0887fb4468f064]::run_compiler::{closure#0}>::{closure#1}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()>
  28:     0x76a65c7a90a2 - <<std[16222f0ba70c5179]::thread::Builder>::spawn_unchecked_<rustc_interface[6928205aa426efe4]::util::run_in_thread_with_globals<rustc_interface[6928205aa426efe4]::util::run_in_thread_pool_with_globals<rustc_interface[6928205aa426efe4]::interface::run_compiler<(), rustc_driver_impl[7f0887fb4468f064]::run_compiler::{closure#0}>::{closure#1}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()>::{closure#1} as core[7c52ce2a1de942a3]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  29:     0x76a65c7af185 - std::sys::pal::unix::thread::Thread::new::thread_start::hdedb734e67ba6c5f
  30:     0x76a655fa1aa4 - <unknown>
  31:     0x76a65602ec3c - <unknown>
  32:                0x0 - <unknown>

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] no current codegen item.
[Kani] no current codegen location.
error: could not compile `vmm` (lib)

Caused by:
  process didn't exit successfully: `/root/.kani/kani-0.65.0/bin/kani-compiler --crate-name vmm --edition=2024 src/vmm/src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=91 --crate-type lib --emit=dep-info,metadata,link -C panic=abort -C embed-bitcode=no -C debuginfo=2 --warn=unexpected_cfgs '--warn=clippy::undocumented_unsafe_blocks' '--warn=clippy::tests_outside_test_module' '--warn=clippy::ptr_as_ptr' '--warn=clippy::or_fun_call' --warn=missing_debug_implementations '--warn=clippy::exit' '--warn=clippy::error_impl_error' '--warn=clippy::cast_sign_loss' '--warn=clippy::cast_possible_wrap' '--warn=clippy::cast_possible_truncation' '--warn=clippy::assertions_on_result_states' --check-cfg 'cfg(kani)' --cfg 'feature="default"' --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values("arrayvec", "default", "gdb", "gdbstub", "gdbstub_arch", "log-instrument", "tracing"))' -C metadata=8c43a0ce1ccc0090 -C extra-filename=-6932d5a6b8e9f0a7 --out-dir /firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/incremental -L dependency=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps -L dependency=/firecracker/build/cargo_target/kani/debug/deps --extern acpi_tables=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libacpi_tables-f64e897ccf08eb9a.rmeta --extern aes_gcm=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libaes_gcm-3be9d19b06da82b3.rmeta --extern anyhow=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libanyhow-edb1fb879f1930c0.rmeta --extern aws_lc_rs=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libaws_lc_rs-83bf4c7fd6e4afad.rmeta --extern base64=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libbase64-bcdee7c2ac1270d3.rmeta --extern bincode=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libbincode-e06baab0f91760b6.rmeta --extern bitflags=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libbitflags-c949113b312dda20.rmeta --extern byteorder=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libbyteorder-7967cc1fe051b8c9.rmeta --extern crc64=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libcrc64-c1cb28e4acc35de9.rmeta --extern derive_more=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libderive_more-41ed3b0cba15eab6.rmeta --extern displaydoc=/firecracker/build/cargo_target/kani/debug/deps/libdisplaydoc-a2775ff14ae724c6.so --extern event_manager=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libevent_manager-45f5a762c405f349.rmeta --extern kvm_bindings=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libkvm_bindings-aeedc1682178799a.rmeta --extern kvm_ioctls=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libkvm_ioctls-6b5763b0d669ad99.rmeta --extern libc=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/liblibc-2bf8659d1830081f.rmeta --extern linux_loader=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/liblinux_loader-d47ad6cef73c9ae3.rmeta --extern log=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/liblog-9bf27f673d454403.rmeta --extern memfd=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libmemfd-2db2fe9cdc03aad5.rmeta --extern micro_http=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libmicro_http-e9b4d1aaa706a919.rmeta --extern pci=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libpci-b88653e5fde134cd.rmeta --extern semver=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libsemver-40b7d98f57323581.rmeta --extern serde=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libserde-4f626d63f39ff5d9.rmeta --extern serde_json=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libserde_json-bece3e71cc50aee6.rmeta --extern slab=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libslab-c4c228091367f695.rmeta --extern thiserror=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libthiserror-7ac6a51c6f95a274.rmeta --extern timerfd=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libtimerfd-44eb2d774aa6b18d.rmeta --extern userfaultfd=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libuserfaultfd-f87f62b0ed76dcd4.rmeta --extern utils=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libutils-4773a82707953809.rmeta --extern uuid=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libuuid-296b08e379645a10.rmeta --extern vhost=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libvhost-95245df16ad11091.rmeta --extern vm_allocator=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libvm_allocator-50b56550876baac2.rmeta --extern vm_device=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libvm_device-1c25cdf205c401ce.rmeta --extern vm_memory=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libvm_memory-2752deb32f8c6447.rmeta --extern vm_superio=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libvm_superio-697a567132f94292.rmeta --extern vmm_sys_util=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libvmm_sys_util-f0314a25eb3aa96a.rmeta --extern zerocopy=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/deps/libzerocopy-cdfac95540edab64.rmeta '-Cllvm-args=--reachability=harnesses --log-level=warn --restrict-vtable-fn-ptrs --assertion-reach-checks --enable-stubbing -Z unstable-options -Z stubbing -Z function-contracts -Z restrict-vtable' -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 /root/.kani/kani-0.65.0 -L /root/.kani/kani-0.65.0/lib --extern kani --extern 'noprelude:std=/root/.kani/kani-0.65.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)' -Clinker=echo --kani-compiler -Cllvm-args=--check-version=0.65.0 -L native=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/build/aws-lc-sys-5a48f40b6b730d35/out/build/artifacts -L native=/firecracker/build/cargo_target/kani/x86_64-unknown-linux-gnu/debug/build/userfaultfd-sys-4d93d3635fa35098/out` (exit status: 101)
error: Failed to compile `vmm` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/kani_middle/stubbing/mod.rs:62:46:
                                Const(TyConst { kind: Param(ParamConst { index: 0, name: "L" }), id: TyConstId(0) }).

[roypat]

I tried finding a more minimal reproducer, but simply having a struct with a const type param in a harness itself isnt enough to trigger the crash :/

[zhassan-aws]

Hi @roypat. Thanks for filing this issue. Here's a minimal reproducer:

struct Foo<const C: usize> {
    _a: [i32; C],
    x: bool,
}

impl<const C: usize> Foo<C> {
    fn foo(&self) -> bool {
        self.x
    }
}

pub fn bar(_x: i32) -> bool {
    false
}

#[kani::proof]
#[kani::stub(Foo::foo, bar)]
fn main() {
    let f = Foo { _a: [1, 2, 3], x: true };
    assert!(!f.foo());
}

This results in:

$ kani iss4322.rs -Zstubbing
Kani Rust Verifier 0.65.0 (standalone)

thread 'rustc' (225424) panicked at kani-compiler/src/kani_middle/stubbing/mod.rs:63:46:
Const(TyConst { kind: Param(ParamConst { index: 0, name: "C" }), id: TyConstId(1) })
note: run with `RUST_BACKTRACE=1` environment variable to display a 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] no current codegen item.
[Kani] no current codegen location.
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101