Kani fails to compile tokio: unable to find field 0 for type StructTag(...) #1835
Description
I tried this code: https://github.com/tokio-rs/tokio at commit ca8e176ce98d2372c24c74839877189cbc9883dc, but the issue is not specific to this commit.
using the following command line invocation:
git clone https://github.com/tokio-rs/tokio.git
cd tokio
git checkout ca8e176ce98d2372c24c74839877189cbc9883dc # but not specific to this commit
cargo kani --enable-unstable assess
with Kani version: 0.14.0 (commit: 6ef19f2)
I expected to see this happen: successful assess report
Instead, this happened: Kani crashed.
Details
thread '<unnamed>' panicked at 'internal error: entered unreachable code: unable to find field 0 for type StructTag("tag-_9643296503468271010")', cprover_bindings/src/goto_program/expr.rs:662:13
stack backtrace:
0: rust_begin_unwind
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/std/src/panicking.rs:575:5
1: core::panicking::panic_fmt
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/panicking.rs:65:14
2: cprover_bindings::goto_program::expr::Expr::member
at [redacted]/kani/cprover_bindings/src/goto_program/expr.rs:662:13
3: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_field
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:292:20
4: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_projection
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:421:28
5: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place::{{closure}}
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:579:53
6: core::iter::adapters::copied::copy_fold::{{closure}}
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/iter/adapters/copied.rs:31:22
7: core::iter::traits::iterator::Iterator::fold
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/iter/traits/iterator.rs:2414:21
8: <core::iter::adapters::copied::Copied<I> as core::iter::traits::iterator::Iterator>::fold
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/iter/adapters/copied.rs:76:9
9: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:576:22
10: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue_ref
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:134:72
11: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:400:63
12: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:56:33
13: kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs:27:29
14: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{{closure}}
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:118:69
15: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/iter/traits/iterator.rs:828:29
16: core::iter::adapters::map::map_fold::{{closure}}
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/iter/adapters/map.rs:84:21
17: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold::enumerate::{{closure}}
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/iter/adapters/enumerate.rs:106:27
18: core::iter::traits::iterator::Iterator::fold
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/iter/traits/iterator.rs:2414:21
19: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/iter/adapters/enumerate.rs:112:9
20: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/iter/adapters/map.rs:124:9
21: core::iter::traits::iterator::Iterator::for_each
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/core/src/iter/traits/iterator.rs:831:9
22: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:118:13
23: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:109:31
24: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::{{closure}}
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:68:13
25: std::thread::local::LocalKey<T>::try_with
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/std/src/thread/local.rs:446:16
26: std::thread::local::LocalKey<T>::with
at /rustc/7fcf850d7942804990a1d2e3fe036622a0fe4c74/library/std/src/thread/local.rs:422:9
27: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:65:9
28: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
at [redacted]/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:108:21
29: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
30: <rustc_interface::passes::QueryContext>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorGuaranteed>>
31: <rustc_interface::queries::Queries>::ongoing_codegen
32: <rustc_interface::interface::Compiler>::enter::<rustc_driver::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorGuaranteed>>
33: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}::{closure#1}>
34: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
Kani unexpectedly panicked during compilation.
If you are seeing this message, 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: std::option::Option::<trybuild::diff::r#impl::Diff>::as_ref
_RNvMNtCs9CMEppwhzwL_4core6optionINtB2_6OptionNtNtNtCs5euqUyQzkrV_8trybuild4diff4impl4DiffE6as_refBN_
[Kani] current codegen location: Loc { file: "[redacted]/.rustup/toolchains/nightly-2022-10-24-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs", function: None, start_line: 629, start_col: Some(5), end_line: 629, end_col: Some(45) }
error: could not compile `tests-build`
Error: cargo exited with status exit status: 101