Crash in Kani compiler on chrono crate

[zhassan-aws]

Steps to reproduce:

1. cargo new foo
2. cd foo
3. cargo add [email protected]
4. Add the following code to src/main.rs:

use chrono::{DateTime, Local};

#[kani::proof]
fn main() {
    let t = DateTime::<Local>::MIN_UTC;
    let _ = t.format("%Y").to_string();
}

using the following command line invocation:

cargo kani

with Kani version: f64f53e

I expected to see this happen: Verification successful

Instead, this happened: Kani crashed

$ RUST_BACKTRACE=1 cargo kani
Kani Rust Verifier 0.59.0 (cargo plugin)
   Compiling autocfg v1.4.0
   Compiling iana-time-zone v0.1.61
   Compiling num-traits v0.2.19
   Compiling chrono v0.4.39
   Compiling foo v0.1.0 (/home/ubuntu/examples/new_bug/foo)
warning: target feature `x87` must be enabled to ensure that the ABI of the current target can be implemented correctly
  |
  = note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>

warning: target feature `sse2` must be enabled to ensure that the ABI of the current target can be implemented correctly
  |
  = note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>


thread 'rustc' panicked at compiler/rustc_metadata/src/rmeta/decoder/cstore_impl.rs:242:1:
DefId(23:4368 ~ chrono[e102]::format::strftime::{impl#2}::parse_next_item::D_FMT::{constant#0}) does not have a "type_of"
stack backtrace:
error: internal compiler error: Kani unexpectedly panicked at panicked at compiler/rustc_metadata/src/rmeta/decoder/cstore_impl.rs:242:1:
                                DefId(23:4368 ~ chrono[e102]::format::strftime::{impl#2}::parse_next_item::D_FMT::{constant#0}) does not have a "type_of".

   0: rust_begin_unwind
   1: core::panicking::panic_fmt
   2: rustc_metadata::rmeta::decoder::cstore_impl::provide_extern::type_of::{closure#2}
      [... omitted 1 frame ...]
   3: rustc_middle::query::plumbing::query_get_at::<rustc_query_system::query::caches::DefIdCache<rustc_middle::query::erase::Erased<[u8; 8]>>>
   4: <rustc_smir::rustc_smir::context::TablesWrapper as stable_mir::compiler_interface::Context>::def_ty
   5: kani_compiler::kani_middle::reachability::MonoItemsCollector::visit_static
             at /home/ubuntu/git/kani/kani-compiler/src/kani_middle/reachability.rs:215:25
   6: kani_compiler::kani_middle::reachability::MonoItemsCollector::reachable_items
             at /home/ubuntu/git/kani/kani-compiler/src/kani_middle/reachability.rs:184:53
   7: kani_compiler::kani_middle::reachability::MonoItemsCollector::collect
             at /home/ubuntu/git/kani/kani-compiler/src/kani_middle/reachability.rs:173:9
   8: kani_compiler::kani_middle::reachability::collect_reachable_items
             at /home/ubuntu/git/kani/kani-compiler/src/kani_middle/reachability.rs:57:9
   9: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:93:16
  10: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:798:15
  11: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:92:35
  12: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:280:63
  13: rustc_smir::rustc_internal::init::{{closure}}
             at /home/ubuntu/.rustup/toolchains/nightly-2025-02-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:196:33
  14: scoped_tls::ScopedKey<T>::set
             at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
  15: rustc_smir::rustc_internal::init
             at /home/ubuntu/.rustup/toolchains/nightly-2025-02-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:196:5
  16: rustc_smir::rustc_internal::run::{{closure}}
             at /home/ubuntu/.rustup/toolchains/nightly-2025-02-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:227:53
  17: stable_mir::compiler_interface::run::{{closure}}
             at /home/ubuntu/.rustup/toolchains/nightly-2025-02-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/stable_mir/src/compiler_interface.rs:265:40
  18: scoped_tls::ScopedKey<T>::set
             at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
  19: stable_mir::compiler_interface::run
             at /home/ubuntu/.rustup/toolchains/nightly-2025-02-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/stable_mir/src/compiler_interface.rs:265:9
  20: rustc_smir::rustc_internal::run
             at /home/ubuntu/.rustup/toolchains/nightly-2025-02-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:227:5
  21: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:237:23
  22: <rustc_interface::queries::Linker>::codegen_and_build_linker
  23: rustc_interface::passes::create_and_enter_global_ctxt::<core::option::Option<rustc_interface::queries::Linker>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2}>::{closure#2}::{closure#0}
  24: 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] no current codegen item.
[Kani] no current codegen location.
error: could not compile `foo` (bin "foo"); 2 warnings emitted

Caused by:
  process didn't exit successfully: `/home/ubuntu/git/kani/target/kani/bin/kani-compiler --crate-name foo --edition=2021 src/main.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=305 --crate-type bin --emit=dep-info,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata=e146a46e8f63abf6 -C extra-filename=-5e68f2f04b38f6e3 --out-dir /home/ubuntu/examples/new_bug/foo/target/kani/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=/home/ubuntu/examples/new_bug/foo/target/kani/x86_64-unknown-linux-gnu/debug/incremental -L dependency=/home/ubuntu/examples/new_bug/foo/target/kani/x86_64-unknown-linux-gnu/debug/deps -L dependency=/home/ubuntu/examples/new_bug/foo/target/kani/debug/deps --extern chrono=/home/ubuntu/examples/new_bug/foo/target/kani/x86_64-unknown-linux-gnu/debug/deps/libchrono-8ff5e118fefb66dd.rlib -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/ubuntu/git/kani/target/kani -L /home/ubuntu/git/kani/target/kani/lib --extern kani --extern 'noprelude:std=/home/ubuntu/git/kani/target/kani/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.59.0 --log-level=warn --assertion-reach-checks'` (exit status: 101)
error: Failed to compile `foo` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at compiler/rustc_metadata/src/rmeta/decoder/cstore_impl.rs:242:1:
                                DefId(23:4368 ~ chrono[e102]::format::strftime::{impl#2}::parse_next_item::D_FMT::{constant#0}) does not have a "type_of".