search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.23k stars 92 forks source link

ICE: `BinaryOperation Expression does not typecheck Plus Expr` #2683

Open matthiaskrgr opened 1 year ago

matthiaskrgr commented 1 year ago

I tried this code:

rust/tests/ui/dynamically-sized-types/dst-struct.rs

// run-pass
struct Fat<T: ?Sized> {
    f1: isize,
    f2: &'static str,
    ptr: T
}

// x is a fat pointer
fn foo(x: &Fat<[isize]>) {
    let y = &x.ptr;
    assert_eq!(y[0], 1);
}

#[kani::proof]
pub fn main() {
    // With a vec of ints.
    let f1 = Fat { f1: 5, f2: "some str", ptr: [1, 2, 3] };
    foo(&f1);

}

using the following command line invocation:

 RUSTFLAGS="-Zmir-opt-level=2" kani dst-struct.rs

with Kani version: 0.34.0

I expected to see this happen: explanation

Instead, this happened: explanation


Kani Rust Verifier 0.34.0 (standalone)
warning: fields `f1` and `f2` are never read
 --> dst-struct.rs:3:5
  |
2 | struct Fat<T: ?Sized> {
  |        --- fields in this struct
3 |     f1: isize,
  |     ^^
4 |     f2: &'static str,
  |     ^^
  |
  = note: `#[warn(dead_code)]` on by default

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:1029:9:
BinaryOperation Expression does not typecheck Plus Expr { value: Member { lhs: Expr { value: Dereference(Expr { value: Member { lhs: Expr { value: Symbol { identifier: "_RNvCs1amkcWqkymA_10dst_struct3foo::1::var_1::x" }, typ: StructTag("tag-&_212445076144030373480958249808482652875"), location: None, size_of_annotation: None }, field: "data" }, typ: Pointer { typ: StructTag("tag-_212445076144030373480958249808482652875") }, location: None, size_of_annotation: None }), typ: StructTag("tag-_212445076144030373480958249808482652875"), location: None, size_of_annotation: None }, field: "ptr" }, typ: FlexibleArray { typ: CInteger(SSizeT) }, location: None, size_of_annotation: None } Expr { value: IntConstant(0), typ: CInteger(SizeT), location: None, size_of_annotation: None }
stack backtrace:
   0:     0x7fba0016319c - std::backtrace_rs::backtrace::libunwind::trace::haf256adafafbe58d
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7fba0016319c - std::backtrace_rs::backtrace::trace_unsynchronized::hfe1951132ff691c0
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7fba0016319c - std::sys_common::backtrace::_print_fmt::h9a0fe52434930c36
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x7fba0016319c - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h24adccbf3e1ada83
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7fba001c989c - core::fmt::rt::Argument::fmt::h18ba555e398addfe
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/core/src/fmt/rt.rs:138:9
   5:     0x7fba001c989c - core::fmt::write::hbf3ee2d80be74759
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/core/src/fmt/mod.rs:1094:21
   6:     0x7fba0015590e - std::io::Write::write_fmt::hfc2b3251522ff943
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/io/mod.rs:1714:15
   7:     0x7fba00162f85 - std::sys_common::backtrace::_print::hfdc8ddb5f3ddee36
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7fba00162f85 - std::sys_common::backtrace::print::h316f264b298c7a30
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7fba001660da - std::panicking::panic_hook_with_disk_dump::{{closure}}::h136bbb963feeea4a
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:278:22
  10:     0x7fba00165d73 - std::panicking::panic_hook_with_disk_dump::hd91a018a982a84f7
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:312:9
  11:     0x55afc674771d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::hbdcd1e2153d1f24b
  12:     0x55afc6745e63 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hc68eaec26ff64861
  13:     0x7fba00166980 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hd99b1fe24ccd07b5
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/alloc/src/boxed.rs:2021:9
  14:     0x7fba00166980 - std::panicking::rust_panic_with_hook::h1593161995c9c003
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:733:13
  15:     0x7fba00166707 - std::panicking::begin_panic_handler::{{closure}}::h6b4a934e37237346
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:621:13
  16:     0x7fba001636d6 - std::sys_common::backtrace::__rust_end_short_backtrace::h365e31c6291fdffa
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys_common/backtrace.rs:170:18
  17:     0x7fba00166452 - rust_begin_unwind
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:617:5
  18:     0x7fba001c5c53 - core::panicking::panic_fmt::hbd2564497e278309
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/core/src/panicking.rs:67:14
  19:     0x55afc6962373 - cprover_bindings::goto_program::expr::Expr::binop::hfde2f1595b998cec
  20:     0x55afc6962a42 - cprover_bindings::goto_program::expr::Expr::plus::h7e1518fc405778fe
  21:     0x55afc66e82ff - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_projection::h8ef94609a9faa773
  22:     0x55afc66ea182 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place::hca2771dc57ddaeac
  23:     0x55afc66dee82 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand::hdb64779d690c624d
  24:     0x55afc66ec853 - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue::h2d1feaaf678662c2
  25:     0x55afc66f9f93 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::hbe3635206b55fa31
  26:     0x55afc66b2860 - kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block::had8f57135e8154af
  27:     0x55afc670f87b - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::he08100d10d5a8739
  28:     0x55afc67dbf7e - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h1c7461510b84019a
  29:     0x55afc67e09e5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h72f45c460ba9f3e3
  30:     0x7fba02694dc2 - <rustc_session[83a530cc07544870]::session::Session>::time::<alloc[b2a4fa84f81d55c8]::boxed::Box<dyn core[8e2a8f22f3da315]::any::Any>, rustc_interface[b10bd5cb1b971de9]::passes::start_codegen::{closure#0}>
  31:     0x7fba0269490b - rustc_interface[b10bd5cb1b971de9]::passes::start_codegen
  32:     0x7fba0268ef1a - <rustc_middle[32728bc096d751c7]::ty::context::GlobalCtxt>::enter::<<rustc_interface[b10bd5cb1b971de9]::queries::Queries>::ongoing_codegen::{closure#0}, core[8e2a8f22f3da315]::result::Result<alloc[b2a4fa84f81d55c8]::boxed::Box<dyn core[8e2a8f22f3da315]::any::Any>, rustc_span[9abd768efbccd329]::ErrorGuaranteed>>
  33:     0x7fba0268df53 - <rustc_interface[b10bd5cb1b971de9]::interface::Compiler>::enter::<rustc_driver_impl[2c2bb0da6cfb3826]::run_compiler::{closure#1}::{closure#2}, core[8e2a8f22f3da315]::result::Result<core[8e2a8f22f3da315]::option::Option<rustc_interface[b10bd5cb1b971de9]::queries::Linker>, rustc_span[9abd768efbccd329]::ErrorGuaranteed>>
  34:     0x7fba02686fc8 - std[b7e5a9c79ea9fbed]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[b10bd5cb1b971de9]::util::run_in_thread_pool_with_globals<rustc_interface[b10bd5cb1b971de9]::interface::run_compiler<core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>, rustc_driver_impl[2c2bb0da6cfb3826]::run_compiler::{closure#1}>::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>
  35:     0x7fba0268674e - <<std[b7e5a9c79ea9fbed]::thread::Builder>::spawn_unchecked_<rustc_interface[b10bd5cb1b971de9]::util::run_in_thread_pool_with_globals<rustc_interface[b10bd5cb1b971de9]::interface::run_compiler<core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>, rustc_driver_impl[2c2bb0da6cfb3826]::run_compiler::{closure#1}>::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[8e2a8f22f3da315]::result::Result<(), rustc_span[9abd768efbccd329]::ErrorGuaranteed>>::{closure#1} as core[8e2a8f22f3da315]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  36:     0x7fba00171125 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hb18992c0c074fb04
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/alloc/src/boxed.rs:2007:9
  37:     0x7fba00171125 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::ha4998f5f9033c44e
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/alloc/src/boxed.rs:2007:9
  38:     0x7fba00171125 - std::sys::unix::thread::Thread::new::thread_start::h3370231efa79af31
                               at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/sys/unix/thread.rs:108:17
  39:     0x7fb9ffc8c9eb - <unknown>
  40:     0x7fb9ffd10ebc - <unknown>
  41:                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: foo
_RNvCs1amkcWqkymA_10dst_struct3foo
[Kani] current codegen location: Loc { file: "/tmp/kani/dst-struct.rs", function: None, start_line: 9, start_col: Some(1), end_line: 9, end_col: Some(25) }
warning: 1 warning emitted

error: /home/matthias/.kani/kani-0.34.0/bin/kani-compiler exited with status exit status: 101
rahulku commented 1 year ago

Thanks @matthiaskrgr We will triage this.

matthiaskrgr commented 12 months ago

Still crashing with 0.40