ICE: "assign statement with unequal types" ; StructTag / StructTag #2237

matthiaskrgr · 2023-02-25T07:47:13Z

I tried this code:

fn id<'c, 'b>(f: &'c &'b dyn Fn(&i32)) -> &'c &'b dyn Fn(&'static i32) {
    f
}

#[kani::proof]
fn main() {
    let f: &dyn Fn(&i32) = &|x| {};
    id(&f);
}

using the following command line invocation:

kani <file>

with Kani version: 0.22.0

I expected to see this happen: explanation

Instead, this happened: explanation

warning: unused variable: `x`
 --> issue-47638.rs:7:30
  |
7 |     let f: &dyn Fn(&i32) = &|x| {};
  |                              ^ help: if this is intentional, prefix it with an underscore: `_x`
  |
  = note: `#[warn(unused_variables)]` on by default

thread '<unnamed>' panicked at 'assertion failed: `(left == right)`
  left: `Pointer { typ: StructTag("tag-_4019304343755080956::FatPtr") }`,
 right: `Pointer { typ: StructTag("tag-_11920736723328834979::FatPtr") }`: Error: assign statement with unequal types lhs Pointer { typ: StructTag("tag-_4019304343755080956::FatPtr") } rhs Pointer { typ: StructTag("tag-_11920736723328834979::FatPtr") }', cprover_bindings/src/goto_program/stmt.rs:170:9
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] current codegen item: codegen_function: id
_RNvCs4Ip2CT9LJTJ_11issue_476382id
[Kani] current codegen location: Loc { file: "/tmp/im/issue-47638.rs", function: None, start_line: 1, start_col: Some(1), end_line: 1, end_col: Some(71) }
warning: 1 warning emitted

The text was updated successfully, but these errors were encountered:

matthiaskrgr · 2023-02-25T07:47:32Z

warning: unused variable: `x`
 --> issue-47638.rs:7:30
  |
7 |     let f: &dyn Fn(&i32) = &|x| {};
  |                              ^ help: if this is intentional, prefix it with an underscore: `_x`
  |
  = note: `#[warn(unused_variables)]` on by default

thread '<unnamed>' panicked at 'assertion failed: `(left == right)`
  left: `Pointer { typ: StructTag("tag-_4019304343755080956::FatPtr") }`,
 right: `Pointer { typ: StructTag("tag-_11920736723328834979::FatPtr") }`: Error: assign statement with unequal types lhs Pointer { typ: StructTag("tag-_4019304343755080956::FatPtr") } rhs Pointer { typ: StructTag("tag-_11920736723328834979::FatPtr") }', cprover_bindings/src/goto_program/stmt.rs:170:9
stack backtrace:
   0:     0x7fae1dc417da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7fae1dc417da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7fae1dc417da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7fae1dc417da - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h9271b09f3576b7e0
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7fae1dca42ee - core::fmt::write::h27d0bbb767cff1d5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17
   5:     0x7fae1dc31c65 - std::io::Write::write_fmt::hc409ea2bb818fbea
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15
   6:     0x7fae1dc415a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5
   7:     0x7fae1dc415a5 - std::sys_common::backtrace::print::he69ac0980f15620d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9
   8:     0x7fae1dc442ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22
   9:     0x7fae1dc4402b - std::panicking::default_hook::h380e71f8d8d49df7
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9
  10:     0x55b6f8baeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462
  11:     0x55b6f8b04f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a
  12:     0x7fae1dc44b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9
  13:     0x7fae1dc44b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13
  14:     0x7fae1dc448a9 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:579:13
  15:     0x7fae1dc41c8c - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:137:18
  16:     0x7fae1dc445b2 - rust_begin_unwind
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:575:5
  17:     0x7fae1dca0cd3 - core::panicking::panic_fmt::hbacb72817da3b060
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:64:14
  18:     0x7fae1dca11b9 - core::panicking::assert_failed_inner::hac89d137c8eb08b5
  19:     0x55b6f8a7393b - core::panicking::assert_failed::h991deaaec5d8e4bb
  20:     0x55b6f8d177aa - cprover_bindings::goto_program::stmt::Stmt::assign::h045ddde843be864f
  21:     0x55b6f8ce8c4d - cprover_bindings::goto_program::expr::Expr::assign::h2c9c2bd44389a1ad
  22:     0x55b6f8ad80d7 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::h4c6e1c8bf226a338
  23:     0x55b6f8a7ef10 - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::h541ea7f90d847b35
  24:     0x55b6f8b0abf0 - std::thread::local::LocalKey<T>::with::hb907a536239d23f6
  25:     0x55b6f8b964c8 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6
  26:     0x7fae1bc86fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}>
  27:     0x7fae1bc86ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen
  28:     0x7fae1bc847a6 - <rustc_interface[aec886e93b1add3f]::passes::QueryContext>::enter::<<rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  29:     0x7fae1bc81a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen
  30:     0x7fae1bc80f67 - <rustc_interface[aec886e93b1add3f]::interface::Compiler>::enter::<rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}::{closure#2}, core[6d94cc961ac87456]::result::Result<core[6d94cc961ac87456]::option::Option<rustc_interface[aec886e93b1add3f]::queries::Linker>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  31:     0x7fae1bc7bf88 - rustc_span[ae2df7aa7c6c667b]::with_source_map::<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  32:     0x7fae1bc7ba75 - <scoped_tls[db87656d258d017b]::ScopedKey<rustc_span[ae2df7aa7c6c667b]::SessionGlobals>>::set::<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  33:     0x7fae1bc7b062 - std[acd1f573e90225f]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  34:     0x7fae1c2ec49e - <<std[acd1f573e90225f]::thread::Builder>::spawn_unchecked_<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#1} as core[6d94cc961ac87456]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  35:     0x7fae1d7da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  36:     0x7fae1d7da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  37:     0x7fae1d7da2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17
  38:     0x7fae195afbb5 - <unknown>
  39:     0x7fae19631d90 - <unknown>
  40:                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] current codegen item: codegen_function: id
_RNvCs4Ip2CT9LJTJ_11issue_476382id
[Kani] current codegen location: Loc { file: "/tmp/im/issue-47638.rs", function: None, start_line: 1, start_col: Some(1), end_line: 1, end_col: Some(71) }
warning: 1 warning emitted

zhassan-aws · 2023-02-25T16:19:41Z

Thanks for filing these issues @matthiaskrgr. Are the examples from the Rust compiler unit tests? If so, are you running them manually or through a script? We were interested in including rustc unit tests in our regressions to capture such corner cases.

matthiaskrgr · 2023-02-25T16:47:12Z

Yes, these are rustc tests. 🙂
I've added some cheap kani support to https://github.com/matthiaskrgr/icemaker/ yesterday night and I try to slap kani::proof onto fndefs that I think kani can run and filter out the crashes.

zhassan-aws · 2023-02-25T21:57:51Z

Cool, thanks 🙂

matthiaskrgr · 2023-02-26T12:19:18Z

BTW do you kani folks have by any chance some automatic way to instrument fn parameters with kani::any() ?

fn very_fun_ction(a: String, b: &Vec<i32>, c: usize)  -> Object {

// blah
}

Would become

#[kani::proof]
fn very_fun_ction()  -> Object {
   let a: String = kani::any();
   let b: &Vec<i32> = kani::any();
   let c: usize = kani::any();
// blah
}

and could be tested automatically

zhassan-aws · 2023-02-26T22:43:09Z

Not yet.

matthiaskrgr · 2023-03-02T20:40:55Z

ok, I think I got it to roughly to work :D
https://github.com/matthiaskrgr/icemaker/blob/master/src/run_commands.rs#L940
I noticed some problems where collection types like String or Vec would not impl kani::arbitrary but I try to fall back to Default::default() instead of kani::any() in such cases

(there may still be a bunch of cases where I just break the code without noticing, but eh... )

zhassan-aws · 2023-03-02T21:05:41Z

Cool! Yeah, kani::any() is only supported for primitive types at the moment:

https://github.com/model-checking/kani/blob/main/library/kani/src/arbitrary.rs

So you might want to do the opposite: provide a list of supported types and default anything else.

matthiaskrgr · 2023-06-02T17:18:53Z

This one is probably related:

// check-pass

#[kani::proof]
fn main() {
    if let Some([b'@', filename @ ..]) = Some(b"@abc123") {
        println!("filename {:?}", filename);
    }
}

thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `Pointer { typ: StructTag("tag-[_5574462982184004571; 6]") }`,
 right: `StructTag("tag-[_5574462982184004571; 6]")`: Error: assign statement with unequal types lhs Pointer { typ: StructTag("tag-[_5574462982184004571; 6]") } rhs StructTag("tag-[_5574462982184004571; 6]")', cprover_bindings/src/goto_program/stmt.rs:170:9
stack backtrace:
   0:     0x7fbf51768cc3 - std::backtrace_rs::backtrace::libunwind::trace::h6dd260ccf76e2a16
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7fbf51768cc3 - std::backtrace_rs::backtrace::trace_unsynchronized::h60e795a392c2d181
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7fbf51768cc3 - std::sys_common::backtrace::_print_fmt::hb92bc719d8e89e18
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7fbf51768cc3 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h433d7296fbd4df36
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7fbf517c9c0f - core::fmt::rt::Argument::fmt::hee863a126433a5fe
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/fmt/rt.rs:138:9
   5:     0x7fbf517c9c0f - core::fmt::write::hecf019f127565c17
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/fmt/mod.rs:1105:21
   6:     0x7fbf5175bd91 - std::io::Write::write_fmt::h4fdee205f020a023
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/io/mod.rs:1712:15
   7:     0x7fbf51768ad5 - std::sys_common::backtrace::_print::h63f1eb292c01c01d
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7fbf51768ad5 - std::sys_common::backtrace::print::h29fa6d106f41082b
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7fbf5176b697 - std::panicking::default_hook::{{closure}}::h24c419639c3568dd
  10:     0x7fbf5176b485 - std::panicking::default_hook::hd5faae45a4c2ae6b
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:288:9
  11:     0x55c565148dfd - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h62fc73136c5344f5
  12:     0x55c565175d83 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::he03976a598c31555
  13:     0x7fbf5176bdd5 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h8fd551c79732d109
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1976:9
  14:     0x7fbf5176bdd5 - std::panicking::rust_panic_with_hook::hff0f13fd32920cda
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:695:13
  15:     0x7fbf5176bb49 - std::panicking::begin_panic_handler::{{closure}}::h4b94c172e12e7b79
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:582:13
  16:     0x7fbf51769106 - std::sys_common::backtrace::__rust_end_short_backtrace::h0d54fda82a2d0073
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:150:18
  17:     0x7fbf5176b8a2 - rust_begin_unwind
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:578:5
  18:     0x7fbf517c5eb3 - core::panicking::panic_fmt::h423e755c13523a61
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/panicking.rs:67:14
  19:     0x7fbf517c6459 - core::panicking::assert_failed_inner::h8ca5b0e75c0ef7cc
  20:     0x55c5650a069b - core::panicking::assert_failed::h11f38e652828bfee
  21:     0x55c565339720 - cprover_bindings::goto_program::stmt::Stmt::assign::haf63951f6b6f27a9
  22:     0x55c56532e263 - cprover_bindings::goto_program::expr::Expr::assign::hc3b054ff6e28a113
  23:     0x55c5650f119c - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::hf245d0e3b1ff69c3
  24:     0x55c5651072de - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::h976e66498994fa63
  25:     0x55c56513173e - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h72b866e5cefa4cb6
  26:     0x55c5651356d1 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::hd63a249ce3b650de
  27:     0x7fbf53be4e26 - rustc_interface[bc622c2a0f547140]::passes::start_codegen
  28:     0x7fbf53be2314 - <rustc_middle[913649502f287e96]::ty::context::GlobalCtxt>::enter::<<rustc_interface[bc622c2a0f547140]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<alloc[ab6e9888d17cae42]::boxed::Box<dyn core[7ab4a128a7734c10]::any::Any>, rustc_span[14f600a439c86087]::ErrorGuaranteed>>
  29:     0x7fbf53be1098 - <rustc_interface[bc622c2a0f547140]::queries::Queries>::ongoing_codegen
  30:     0x7fbf53be087b - <rustc_interface[bc622c2a0f547140]::interface::Compiler>::enter::<rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}::{closure#2}, core[7ab4a128a7734c10]::result::Result<core[7ab4a128a7734c10]::option::Option<rustc_interface[bc622c2a0f547140]::queries::Linker>, rustc_span[14f600a439c86087]::ErrorGuaranteed>>
  31:     0x7fbf53bde86f - rustc_span[14f600a439c86087]::set_source_map::<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  32:     0x7fbf53bddf00 - std[f87cae68a756700d]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[bc622c2a0f547140]::util::run_in_thread_pool_with_globals<rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>
  33:     0x7fbf53bdd821 - <<std[f87cae68a756700d]::thread::Builder>::spawn_unchecked_<rustc_interface[bc622c2a0f547140]::util::run_in_thread_pool_with_globals<rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#1} as core[7ab4a128a7734c10]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  34:     0x7fbf51776305 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hdbaea59c5dcd35ae
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1962:9
  35:     0x7fbf51776305 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hedf781cff528734a
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1962:9
  36:     0x7fbf51776305 - std::sys::unix::thread::Thread::new::thread_start::h8db1b8acf05cf216
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys/unix/thread.rs:108:17
  37:     0x7fbf51510bb5 - <unknown>
  38:     0x7fbf51592d90 - <unknown>
  39:                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] current codegen item: codegen_function: main
main
[Kani] current codegen location: Loc { file: "/home/matthias/vcs/github/rust/tests/ui/pattern/issue-74954.rs", function: None, start_line: 4, start_col: Some(1), end_line: 4, end_col: Some(10) }
error: /home/matthias/.kani/kani-0.29.0/bin/kani-compiler exited with status exit status: 101

matthiaskrgr · 2023-11-12T21:19:22Z

Triage: kani 0.40

original example fixed, #2237 (comment) still crashing

matthiaskrgr added the [C] Bug This is a bug. Something isn't working. label Feb 25, 2023

matthiaskrgr changed the title ~~ICE: "assign statement with unequal types"~~ ICE: "assign statement with unequal types" ; StructTag / StructTag Feb 25, 2023

zhassan-aws added the [F] Crash Kani crashed label Mar 2, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

ICE: "assign statement with unequal types" ; StructTag / StructTag #2237

ICE: "assign statement with unequal types" ; StructTag / StructTag #2237

matthiaskrgr commented Feb 25, 2023

matthiaskrgr commented Feb 25, 2023 •

edited

Loading

zhassan-aws commented Feb 25, 2023

matthiaskrgr commented Feb 25, 2023

zhassan-aws commented Feb 25, 2023

matthiaskrgr commented Feb 26, 2023

zhassan-aws commented Feb 26, 2023

matthiaskrgr commented Mar 2, 2023 •

edited

Loading

zhassan-aws commented Mar 2, 2023 •

edited

Loading

matthiaskrgr commented Jun 2, 2023

matthiaskrgr commented Nov 12, 2023

ICE: "assign statement with unequal types" ; StructTag / StructTag #2237

ICE: "assign statement with unequal types" ; StructTag / StructTag #2237

Comments

matthiaskrgr commented Feb 25, 2023

matthiaskrgr commented Feb 25, 2023 • edited Loading

zhassan-aws commented Feb 25, 2023

matthiaskrgr commented Feb 25, 2023

zhassan-aws commented Feb 25, 2023

matthiaskrgr commented Feb 26, 2023

zhassan-aws commented Feb 26, 2023

matthiaskrgr commented Mar 2, 2023 • edited Loading

zhassan-aws commented Mar 2, 2023 • edited Loading

matthiaskrgr commented Jun 2, 2023

matthiaskrgr commented Nov 12, 2023

matthiaskrgr commented Feb 25, 2023 •

edited

Loading

matthiaskrgr commented Mar 2, 2023 •

edited

Loading

zhassan-aws commented Mar 2, 2023 •

edited

Loading