Crash in Kani compiler on chrono crate

[zhassan-aws]

Steps to reproduce:

1. cargo new foo
2. cd foo
3. cargo add chrono@0.4.39
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".

[tautschnig]

It seems the problem is that type_of is not implemented for anonymous constants. I am, however, struggling to create Rust code that would even yield such an anonymous constant. The following seemed to be a minimal variant of the chrono code, but apparently does not yield such an anonymous constant (still pasting it here in case someone has ideas on how it has to be extended):

#[derive(PartialEq)]
enum Numeric {
    A,
    B,
    C
}

#[derive(PartialEq)]
enum Item<'a> {
    Numeric(Numeric),
    Literal(&'a str)
}

#[kani::proof]
pub fn harness() {
    static FOO: &[Item<'static>] = &[Item::Numeric(Numeric::A), Item::Literal("/")];
    assert!(FOO[0] == num(Numeric::A));
}

Even in the absence of a smaller reproducer: the only way I found that may tell us about anonymous constants is this:

--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -219,20 +219,27 @@ fn visit_static(&mut self, def: StaticDef) -> Vec<CollectedItem> {
         let _guard = debug_span!("visit_static", ?def).entered();
         let mut next_items = vec![];

-        // Collect drop function.
-        let static_ty = def.ty();
-        let instance = Instance::resolve_drop_in_place(static_ty);
-        next_items
-            .push(CollectedItem { item: instance.into(), reason: CollectionReason::StaticDrop });
-
-        // Collect initialization.
-        let alloc = def.eval_initializer().unwrap();
-        for (_, prov) in alloc.provenance.ptrs {
-            next_items.extend(
-                collect_alloc_items(prov.0)
-                    .into_iter()
-                    .map(|item| CollectedItem { item, reason: CollectionReason::Static }),
-            );
+        // Collect drop function, unless it's an anonymous static.
+        let int_def_id = rustc_internal::internal(self.tcx, def.def_id());
+        let anonymous = match self.tcx.def_kind(int_def_id) {
+            rustc_hir::def::DefKind::Static { nested, .. } => nested,
+            _ => false
+        };
+        if !anonymous {
+            let static_ty = def.ty();
+            let instance = Instance::resolve_drop_in_place(static_ty);
+            next_items
+                .push(CollectedItem { item: instance.into(), reason: CollectionReason::StaticDrop });
+
+            // Collect initialization.
+            let alloc = def.eval_initializer().unwrap();
+            for (_, prov) in alloc.provenance.ptrs {
+                next_items.extend(
+                    collect_alloc_items(prov.0)
+                        .into_iter()
+                        .map(|item| CollectedItem { item, reason: CollectionReason::Static }),
+                );
+            }
         }

         next_items

But then this leads to problems in check_reachable_items. Anyone with a better understanding of rustc internals have a clue?

[zhassan-aws]

Thanks for looking into this @tautschnig!

But then this leads to problems in check_reachable_items

What kind of problems?

[carolynzech]

This code:

static mut FOO: &mut u32 = &mut 42;

fn main() {
    unsafe {
        *FOO = 43;
    }
}

produces an anonymous static:

alloc1 (static: FOO, size: 8, align: 8) {
    ╾───────alloc2────────╼                         │ ╾──────╼
}

alloc2 (static: FOO::{constant#0}, size: 4, align: 4) {
    2a 00 00 00                                     │ *...
}

Consider this slightly more complicated example, inspired by rust-lang/rust#79738 (comment), which produces

alloc5 (static: BAZ, size: 8, align: 8) {
    ╾─────alloc3<imm>─────╼                         │ ╾──────╼
}

alloc3 (size: 4, align: 4) {
    2a 00 00 00                                     │ *...
}

alloc4 (static: BAR, size: 8, align: 8) {
    ╾─────alloc3<imm>─────╼                         │ ╾──────╼
}

See also rust-lang/rust#61345, rust-lang/rust#67000, and rust-lang/rust#116564 for inspiration/context .

I extended @tautschnig's code in https://github.com/carolynzech/kani/tree/issue-3904. The two examples in this comment verify successfully if I make their main functions harnesses, and the original code from this issue also codegens successfully. Verification is still running after ~30 mins, which isn't necessarily surprising in string code.

I haven't made a PR for this branch yet because I want to convince myself a bit more that this is actually the right logic. Thoughts appreciated :) @zhassan-aws @tautschnig

[zhassan-aws]

Awesome, thanks @carolynzech! I looked at your branch, and I don't see anything that looks wrong. I'm a bit confused about the part than handles interior mutability though, and why this is needed in the first place.

[tautschnig]

Awesome, thanks @carolynzech! I looked at your branch, and I don't see anything that looks wrong. I'm a bit confused about the part than handles interior mutability though, and why this is needed in the first place.

+1 to everything that Zyad said: Thank you for coming up with the full fix, please include the tests that you came up with in that PR. And, yes, I am also wondering why that "except for this line" difference is needed, can you please expand the comment in the code for the version to be PR'ed?

[carolynzech]

@tautschnig @zhassan-aws You're right--I was trying to make the distinction that the allocations are mutable, but that wasn't the right way to do it. I've made some changes to the approach, see #3953