Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

ICE: Function call does not type check: #![feature(unboxed_closures/tuple_trait)] #2260

Closed
matthiaskrgr opened this issue Mar 2, 2023 · 3 comments · Fixed by #2994
Closed

ICE: Function call does not type check: #![feature(unboxed_closures/tuple_trait)] #2260

matthiaskrgr opened this issue Mar 2, 2023 · 3 comments · Fixed by #2994
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed

Comments

@matthiaskrgr
Copy link
Contributor

I tried this code:

#![feature(unboxed_closures, tuple_trait)]

extern "rust-call" fn foo<T: std::marker::Tuple>(_: T) {}

#[kani::proof]
fn main() {
    foo(());
}

using the following command line invocation:

kani file.rs

with Kani version: 0.22.0

I expected to see this happen: explanation

Instead, this happened: explanation

thread '<unnamed>' panicked at 'Function call does not type check:
func: Expr { value: Dereference(Expr { value: Member { lhs: Expr { value: Dereference(Expr { value: Member { lhs: Expr { value: Symbol { identifier: "main::1::var_7" }, typ: StructTag("tag-_3536752393460457139::FatPtr"), location: None }, field: "vtable" }, typ: Pointer { typ: StructTag("tag-_3536752393460457139::vtable") }, location: None }), typ: StructTag("tag-_3536752393460457139::vtable"), location: None }, field: "4" }, typ: Pointer { typ: Code { parameters: [Parameter { typ: Pointer { typ: TypeDef { name: "_3536752393460457139Inner", typ: StructTag("tag-Unit") } }, identifier: None, base_name: None }, Parameter { typ: StructTag("tag-Unit"), identifier: None, base_name: None }], return_type: StructTag("tag-Unit") } }, location: None }), typ: Code { parameters: [Parameter { typ: Pointer { typ: TypeDef { name: "_3536752393460457139Inner", typ: StructTag("tag-Unit") } }, identifier: None, base_name: None }, Parameter { typ: StructTag("tag-Unit"), identifier: None, base_name: None }], return_type: StructTag("tag-Unit") }, location: None }
args: [Expr { value: Member { lhs: Expr { value: Symbol { identifier: "main::1::var_7" }, typ: StructTag("tag-_3536752393460457139::FatPtr"), location: None }, field: "data" }, typ: Pointer { typ: TypeDef { name: "_3536752393460457139Inner", typ: StructTag("tag-Unit") } }, location: None }]', cprover_bindings/src/goto_program/expr.rs:639:9
stack backtrace:
   0:     0x7fba0b3667da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7fba0b3667da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7fba0b3667da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7fba0b3667da - <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:     0x7fba0b3c92ee - core::fmt::write::h27d0bbb767cff1d5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17
   5:     0x7fba0b356c65 - std::io::Write::write_fmt::hc409ea2bb818fbea
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15
   6:     0x7fba0b3665a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5
   7:     0x7fba0b3665a5 - std::sys_common::backtrace::print::he69ac0980f15620d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9
   8:     0x7fba0b3692ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22
   9:     0x7fba0b36902b - std::panicking::default_hook::h380e71f8d8d49df7
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9
  10:     0x5617339aeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462
  11:     0x561733904f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a
  12:     0x7fba0b369b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9
  13:     0x7fba0b369b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13
  14:     0x7fba0b3698a9 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:579:13
  15:     0x7fba0b366c8c - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:137:18
  16:     0x7fba0b3695b2 - rust_begin_unwind
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:575:5
  17:     0x7fba0b3c5cd3 - core::panicking::panic_fmt::hbacb72817da3b060
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:64:14
  18:     0x561733ae1a2d - cprover_bindings::goto_program::expr::Expr::call::h8d61813f13668ae2
  19:     0x5617338def81 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_virtual_funcall::he501b7b32961032d
  20:     0x5617338dc90f - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator::hba20b41c6ebc6f6b
  21:     0x56173387f15d - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::h541ea7f90d847b35
  22:     0x56173390abf0 - std::thread::local::LocalKey<T>::with::hb907a536239d23f6
  23:     0x5617339964c8 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6
  24:     0x7fba0d886fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}>
  25:     0x7fba0d886ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen
  26:     0x7fba0d8847a6 - <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>>
  27:     0x7fba0d881a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen
  28:     0x7fba0d880f67 - <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>>
  29:     0x7fba0d87bf88 - 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}>
  30:     0x7fba0d87ba75 - <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>>
  31:     0x7fba0d87b062 - 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>>
  32:     0x7fba0deec49e - <<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}
  33:     0x7fba0f3da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  34:     0x7fba0f3da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  35:     0x7fba0f3da2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17
  36:     0x7fba0b01dbb5 - <unknown>
  37:     0x7fba0b09fd90 - <unknown>
  38:                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/icemaker/kani/b.rs", function: None, start_line: 11, start_col: Some(1), end_line: 11, end_col: Some(10) }
error: /home/matthias/.kani/kani-0.22.0/bin/kani-compiler exited with status exit status: 101
@matthiaskrgr matthiaskrgr added the [C] Bug This is a bug. Something isn't working. label Mar 2, 2023
@matthiaskrgr matthiaskrgr changed the title ICE: Function call does not type check: #![feature(unboxed_closures)] ICE: Function call does not type check: #![feature(unboxed_closures/tuple_trait)] Mar 2, 2023
@zhassan-aws zhassan-aws added the [F] Crash Kani crashed label Mar 2, 2023
@zhassan-aws zhassan-aws mentioned this issue Mar 22, 2023
Closed
@celinval
Copy link
Contributor

I get a different error than originally reported:

$ RUST_BACKTRACE=1 kani tuple_trait.rs 
Kani Rust Verifier 0.37.0 (standalone)
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:271:13:
assertion failed: prev_args.len() == 1
stack backtrace:
   0: rust_begin_unwind
             at /rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/std/src/panicking.rs:619:5
   1: core::panicking::panic_fmt
             at /rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/panicking.rs:72:14
   2: core::panicking::panic
             at /rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/panicking.rs:127:5
   3: kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::sig_with_untupled_args
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:271:13
   4: kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::fn_sig_of_instance
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:410:28
   5: kani_compiler::codegen_cprover_gotoc::context::current_fn::CurrentFnCtx::new
             at /kani/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs:48:18
   6: kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx::set_current_fn
             at /kani/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs:305:32
   7: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::declare_function
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:227:9
   8: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:104:39
   9: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:68:13
  10: std::thread::local::LocalKey<T>::try_with
             at /rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/std/src/thread/local.rs:270:16
  11: std::thread::local::LocalKey<T>::with
             at /rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/std/src/thread/local.rs:246:9
  12: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
             at /kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:65:9
  13: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:103:29
  14: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:752:15
  15: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:97:9
  16: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:243:25
  17: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
  18: rustc_interface::passes::start_codegen
  19: <rustc_middle::ty::context::GlobalCtxt>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_span::ErrorGuaranteed>>
  20: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
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] current codegen item: declare_function: foo::<()>
[Kani] current codegen location: Loc { file: "/tmp/tuple_trait.rs", function: None, start_line: 3, start_col: Some(1), end_line: 3, end_col: Some(55) }

@celinval
Copy link
Contributor

celinval commented Sep 28, 2023 •
edited
Loading

This seems related to the "rust-call" ABI handling. Using arguments also triggers the issue I mentioned above:

extern "rust-call" fn equal<T, U>(args: (T, U)) -> bool
where
    T: PartialEq<U>,
{
    args.0 == args.1
}

#[kani::proof]
fn check_empty() {
    let input: u8 = kani::any();
    assert!(equal((input, input)));
}

@matthiaskrgr
Copy link
Contributor Author

I get a different error than originally reported:

Ah yes I also get that now, maybe I just accidentally copied a wrong stacktrace.
triage: still crashing with 0.40 🙃

@celinval celinval mentioned this issue Feb 6, 2024
Merged
celinval added a commit that referenced this issue Feb 6, 2024
@celinval
Fix ICEs due to mismatched arguments (#2994)
a82bad4 
Use FnAbi instead of function signature when generating code for
function types. Properly check the `PassMode::Ignore`. For foreign
functions, instead of ignoring the declaration type, cast the arguments
and return value.

For now, we also ignore the caller location, since we don't currently
support tracking caller location. This change makes it easier for us to
do so. We might want to wait for this issue to get fixed so we can
easily add support using stable APIs:
rust-lang/project-stable-mir#62

Resolves #2260
Resolves #2312
Resolves #1365
Resolves #1350
@feliperodri feliperodri mentioned this issue Feb 9, 2024
Merged
feliperodri added a commit that referenced this issue Feb 9, 2024
@feliperodri @celinval
Bump Kani version to 0.46.0 (#3013)
0fb87be 
## What's Changed
* `modifies` Clauses for Function Contracts by @JustusAdam in
#2800
* Fix ICEs due to mismatched arguments by @celinval in
#2994. Resolves the following
issues:
  * #2260
  * #2312
* Enable powf*, exp*, log* intrinsics by @tautschnig in
#2996
* Upgrade Rust toolchain to nightly-2024-01-24 by @celinval @feliperodri
@qinheping

**Full Changelog**:
kani-0.45.0...kani-0.46.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Co-authored-by: Celina G. Val <celinval@amazon.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix ICEs due to mismatched arguments celinval/kani-dev
3 participants
@matthiaskrgr @celinval @zhassan-aws