search

model-checking / kani

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

ice: `assertion failed: length >= min_length` #2875

Closed matthiaskrgr closed 12 months ago

matthiaskrgr commented 12 months ago

I tried this code:

// We test the `align_offset` panic below, make sure we test the interpreter impl and not the "real" one.
//@compile-flags: -Zmiri-symbolic-alignment-check
#![feature(never_type)]
#![allow(unconditional_panic, non_fmt_panics)]

use std::cell::Cell;
use std::panic::{catch_unwind, AssertUnwindSafe};
use std::process;

thread_local! {
    static MY_COUNTER: Cell<usize> = Cell::new(0);
    static DROPPED: Cell<bool> = Cell::new(false);
    static HOOK_CALLED: Cell<bool> = Cell::new(false);
}

struct DropTester;
impl Drop for DropTester {
    fn drop(&mut self) {
        DROPPED.with(|c| {
            c.set(true);
        });
    }
}

fn do_panic_counter(do_panic: impl FnOnce(usize) -> !) {
    // If this gets leaked, it will be easy to spot
    // in Miri's leak report
    let _string = "LEAKED FROM do_panic_counter".to_string();

    // When we panic, this should get dropped during unwinding
    let _drop_tester = DropTester;

    // Check for bugs in Miri's panic implementation.
    // If do_panic_counter() somehow gets called more than once,
    // we'll generate a different panic message and stderr will differ.
    let old_val = MY_COUNTER.with(|c| {
        let val = c.get();
        c.set(val + 1);
        val
    });
    do_panic(old_val);
}

#[kani::proof]
fn main() {

    // Built-in panics; also make sure the message is right.
    test(Some("index out of bounds: the len is 3 but the index is 4"), |_old_val| {
        let _val = [0, 1, 2][4];
        process::abort()
    });

}

fn test(expect_msg: Option<&str>, do_panic: impl FnOnce(usize) -> !) {
    // Reset test flags.
    DROPPED.with(|c| c.set(false));
    HOOK_CALLED.with(|c| c.set(false));

    // Cause and catch a panic.
    let res = catch_unwind(AssertUnwindSafe(|| {
        let _string = "LEAKED FROM CLOSURE".to_string();
        do_panic_counter(do_panic)
    }))
    .expect_err("do_panic() did not panic!");

}

using the following command line invocation:

RUST_BACKTRACE=full RUSTFLAGS="-Zmir-opt-level=2" kani catch_panic.rs

with Kani version:

I expected to see this happen: explanation

Instead, this happened: explanation

Kani Rust Verifier 0.40.0 (standalone)
warning: unused variable: `res`
  --> catch_panic.rs:61:9
   |
61 |     let res = catch_unwind(AssertUnwindSafe(|| {
   |         ^^^ help: if this is intentional, prefix it with an underscore: `_res`
   |
   = note: `#[warn(unused_variables)]` on by default

warning: unused variable: `expect_msg`
  --> catch_panic.rs:55:9
   |
55 | fn test(expect_msg: Option<&str>, do_panic: impl FnOnce(usize) -> !) {
   |         ^^^^^^^^^^ help: if this is intentional, prefix it with an underscore: `_expect_msg`

thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:710:17:
assertion failed: length >= min_length
stack backtrace:
   0:     0x7f38f6769cfc - std::backtrace_rs::backtrace::libunwind::trace::h974857262e179b17
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/../../backtrace/src/backtrace/libunwind.rs:104:5
   1:     0x7f38f6769cfc - std::backtrace_rs::backtrace::trace_unsynchronized::h6adce2053c056ac9
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f38f6769cfc - std::sys_common::backtrace::_print_fmt::hcf2018a5ad956761
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x7f38f6769cfc - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h3d39e48ce4d7e36f
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7f38f67cbf50 - core::fmt::rt::Argument::fmt::hef0ae15422a7f61d
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/fmt/rt.rs:142:9
   5:     0x7f38f67cbf50 - core::fmt::write::hf465a4ba34489409
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/fmt/mod.rs:1117:17
   6:     0x7f38f675dc1f - std::io::Write::write_fmt::hf34ad5986fa99e89
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/io/mod.rs:1763:15
   7:     0x7f38f6769ae4 - std::sys_common::backtrace::_print::h5aa7f1d99916c125
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7f38f6769ae4 - std::sys_common::backtrace::print::h036d85b5c81889eb
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7f38f676c777 - std::panicking::default_hook::{{closure}}::h9b311bcc8d2b2a40
  10:     0x7f38f676c4df - std::panicking::default_hook::hd7a03fd029ce4ee2
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:292:9
  11:     0x55b6f5a07c0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h270fbeb056d900dc
  12:     0x55b6f5a07703 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::h410a2f5534eafaf7
  13:     0x7f38f676ceb8 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h079168172b9ee18d
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2021:9
  14:     0x7f38f676ceb8 - std::panicking::rust_panic_with_hook::h9ec5267af19ebd61
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:783:13
  15:     0x7f38f676cbd9 - std::panicking::begin_panic_handler::{{closure}}::hded4ae2a191a7bae
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:649:13
  16:     0x7f38f676a1c6 - std::sys_common::backtrace::__rust_end_short_backtrace::h3b03f6ccd27da73f
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:170:18
  17:     0x7f38f676c972 - rust_begin_unwind
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:645:5
  18:     0x7f38f67c8675 - core::panicking::panic_fmt::h290f6f1be63b094c
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:72:14
  19:     0x7f38f67c8713 - core::panicking::panic::hac1e457063a02956
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:127:5
  20:     0x55b6f58f7f96 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_projection::hfcde4a93dde4059b
  21:     0x55b6f58f9694 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place::h4dc87b5d60ece886
  22:     0x55b6f58ed4c8 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand::h4e38dfde4e70e9b4
  23:     0x55b6f58febd3 - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue::h566e8c357ae4b24c
  24:     0x55b6f590fdb7 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::h67859eadd810316a
  25:     0x55b6f58c3909 - kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block::h892262db0bd2a271
  26:     0x55b6f59270ec - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::hc439f7b37aa26293
  27:     0x55b6f595b10a - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::hc367daaf74d3c1cb
  28:     0x55b6f595fcf5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h2ef5769ca04f3bc4
  29:     0x7f38fb180fd9 - rustc_interface[90d65b0f51490bf6]::passes::start_codegen
  30:     0x7f38fb180a96 - <rustc_interface[90d65b0f51490bf6]::queries::Queries>::ongoing_codegen
  31:     0x7f38fb143693 - std[d7fc13cc5242579e]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[90d65b0f51490bf6]::util::run_in_thread_with_globals<rustc_interface[90d65b0f51490bf6]::interface::run_compiler<core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>, rustc_driver_impl[88c66c37425cba72]::run_compiler::{closure#1}>::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>
  32:     0x7f38fb142909 - <<std[d7fc13cc5242579e]::thread::Builder>::spawn_unchecked_<rustc_interface[90d65b0f51490bf6]::util::run_in_thread_with_globals<rustc_interface[90d65b0f51490bf6]::interface::run_compiler<core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>, rustc_driver_impl[88c66c37425cba72]::run_compiler::{closure#1}>::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#1} as core[53bdee0566a68c19]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  33:     0x7f38f6777c85 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he310d06a8f297797
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2007:9
  34:     0x7f38f6777c85 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h69350f715ad37c20
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2007:9
  35:     0x7f38f6777c85 - std::sys::unix::thread::Thread::new::thread_start::h7310dea1d780d6a0
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys/unix/thread.rs:108:17
  36:     0x7f38f64549eb - <unknown>
  37:     0x7f38f64d87cc - <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::{closure#0}
_RNCNvCsh039Gu1PBd7_11catch_panic4main0B3_
[Kani] current codegen location: Loc { file: "/tmp/icemaker/catch_panic.rs", function: None, start_line: 48, start_col: Some(72), end_line: 48, end_col: Some(82) }
warning: 2 warnings emitted

error: /home/matthias/.kani/kani-0.40.0/bin/kani-compiler exited with status exit status: 101
matthiaskrgr commented 12 months ago

Nvm I think this is https://github.com/model-checking/kani/issues/2732 :)