ICE: Argument doesn't check / Function call does not type check

[matthiaskrgr]

I tried this code:

#![allow(unused)]

use std::{
    cell::{Cell, RefCell},
    future::Future,
    marker::Unpin,
    panic,
    pin::Pin,
    ptr,
    rc::Rc,
    task::{Context, Poll, RawWaker, RawWakerVTable, Waker},
};

struct InjectedFailure;

struct Defer<T> {
    ready: bool,
    value: Option<T>,
}

impl<T: Unpin> Future for Defer<T> {
    type Output = T;
    fn poll(mut self: Pin<&mut Self>, cx: &mut Context) -> Poll<Self::Output> {
        if self.ready {
            Poll::Ready(self.value.take().unwrap())
        } else {
            self.ready = true;
            Poll::Pending
        }
    }
}

/// Allocator tracks the creation and destruction of `Ptr`s.
/// The `failing_op`-th operation will panic.
struct Allocator {
    data: RefCell<Vec<bool>>,
    failing_op: usize,
    cur_ops: Cell<usize>,
}

impl panic::UnwindSafe for Allocator {}
impl panic::RefUnwindSafe for Allocator {}

impl Drop for Allocator {
    fn drop(&mut self) {
        let data = self.data.borrow();
        if data.iter().any(|d| *d) {
            panic!("missing free: {:?}", data);
        }
    }
}

impl Allocator {
    fn new(failing_op: usize) -> Self {
        Allocator { failing_op, cur_ops: Cell::new(0), data: RefCell::new(vec![]) }
    }
    fn alloc(&self) -> impl Future<Output = Ptr<'_>> + '_ {
        self.fallible_operation();

        let mut data = self.data.borrow_mut();

        let addr = data.len();
        data.push(true);
        Defer { ready: false, value: Some(Ptr(addr, self)) }
    }
    fn fallible_operation(&self) {
        self.cur_ops.set(self.cur_ops.get() + 1);

        if self.cur_ops.get() == self.failing_op {
            panic::panic_any(InjectedFailure);
        }
    }
}

// Type that tracks whether it was dropped and can panic when it's created or
// destroyed.
struct Ptr<'a>(usize, &'a Allocator);
impl<'a> Drop for Ptr<'a> {
    fn drop(&mut self) {
        match self.1.data.borrow_mut()[self.0] {
            false => panic!("double free at index {:?}", self.0),
            ref mut d => *d = false,
        }

        self.1.fallible_operation();
    }
}

async fn subslice_pattern_reassign(a: Rc<Allocator>) {
    let mut ar = [a.alloc().await, a.alloc().await, a.alloc().await];
    let [_, _, _x] = ar;
    ar = [a.alloc().await, a.alloc().await, a.alloc().await];
    let [_, _y @ ..] = ar;
    a.alloc().await;
}


fn run_test<F, G>(cx: &mut Context<'_>, ref f: F)
where
    F: Fn(Rc<Allocator>) -> G,
    G: Future<Output = ()>,
{
    for polls in 0.. {
        // Run without any panics to find which operations happen after the
        // penultimate `poll`.
        let first_alloc = Rc::new(Allocator::new(usize::MAX));
        let mut fut = Box::pin(f(first_alloc.clone()));
        let mut ops_before_last_poll = 0;
        let mut completed = false;
        for _ in 0..polls {
            ops_before_last_poll = first_alloc.cur_ops.get();
            if let Poll::Ready(()) = fut.as_mut().poll(cx) {
                completed = true;
            }
        }
        drop(fut);

        // Start at `ops_before_last_poll` so that we will always be able to
        // `poll` the expected number of times.
        for failing_op in ops_before_last_poll..first_alloc.cur_ops.get() {
            let alloc = Rc::new(Allocator::new(failing_op + 1));
            let f = &f;
            let cx = &mut *cx;
            let result = panic::catch_unwind(panic::AssertUnwindSafe(move || {
                let mut fut = Box::pin(f(alloc));
                for _ in 0..polls {
                    let _ = fut.as_mut().poll(cx);
                }
                drop(fut);
            }));
            match result {
                Ok(..) => panic!("test executed more ops on first call"),
                Err(e) => {
                    if e.downcast_ref::<InjectedFailure>().is_none() {
                        panic::resume_unwind(e);
                    }
                }
            }
        }

        if completed {
            break;
        }
    }
}

fn clone_waker(data: *const ()) -> RawWaker {
    RawWaker::new(data, &RawWakerVTable::new(clone_waker, drop, drop, drop))
}

#[kani::proof]
fn main() {
    let waker = unsafe { Waker::from_raw(clone_waker(ptr::null())) };
    let context = &mut Context::from_waker(&waker);
    run_test(context, |a| subslice_pattern_reassign(a));

}

using the following command line invocation:

RUST_BACKTRACE=full RUSTFLAGS="--edition=2021" kani dynamic-drop-async.rs`

with Kani version:
kani 0.29.0

I expected to see this happen: explanation

Instead, this happened: explanation

ERROR cprover_bindings::goto_program::expr Argument doesn't check, param=Pointer { typ: StructTag("tag-[_17640226508121321878; 1]") }, arg=StructTag("tag-[_17640226508121321878; 1]")
thread 'rustc' panicked at 'Function call does not type check:
func: Expr { value: Symbol { identifier: "_RINvNtCsg38raRqfonS_4core3ptr13drop_in_placeANtCsbpocqJq3mfW_18dynamic_drop_async3Ptrj1_EBJ_" }, typ: Code { parameters: [Parameter { typ: Pointer { typ: StructTag("tag-[_17640226508121321878; 1]") }, identifier: None, base_name: None }], return_type: StructTag("tag-Unit") }, location: None, size_of_annotation: None }
args: [Expr { value: StatementExpression { statements: [Stmt { body: Block([Stmt { body: Assert { cond: Expr { value: BoolConstant(false), typ: Bool, location: None, size_of_annotation: None }, property_class: "unsupported_construct", msg: "Sub-array binding is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/707" }, location: PropertyUnknownLocation { comment: "Sub-array binding is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/707", property_class: "unsupported_construct" } }, Stmt { body: Assume { cond: Expr { value: BoolConstant(false), typ: Bool, location: None, size_of_annotation: None } }, location: None }]), location: None }, Stmt { body: Expression(Expr { value: Nondet, typ: StructTag("tag-[_17640226508121321878; 1]"), location: None, size_of_annotation: None }), location: None }] }, typ: StructTag("tag-[_17640226508121321878; 1]"), location: None, size_of_annotation: None }]', cprover_bindings/src/goto_program/expr.rs:661:9
stack backtrace:
   0:     0x7f9bf6568cc3 - std::backtrace_rs::backtrace::libunwind::trace::h6dd260ccf76e2a16
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7f9bf6568cc3 - std::backtrace_rs::backtrace::trace_unsynchronized::h60e795a392c2d181
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f9bf6568cc3 - std::sys_common::backtrace::_print_fmt::hb92bc719d8e89e18
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7f9bf6568cc3 - <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:     0x7f9bf65c9c0f - core::fmt::rt::Argument::fmt::hee863a126433a5fe
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/fmt/rt.rs:138:9
   5:     0x7f9bf65c9c0f - core::fmt::write::hecf019f127565c17
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/fmt/mod.rs:1105:21
   6:     0x7f9bf655bd91 - std::io::Write::write_fmt::h4fdee205f020a023
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/io/mod.rs:1712:15
   7:     0x7f9bf6568ad5 - std::sys_common::backtrace::_print::h63f1eb292c01c01d
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7f9bf6568ad5 - std::sys_common::backtrace::print::h29fa6d106f41082b
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7f9bf656b697 - std::panicking::default_hook::{{closure}}::h24c419639c3568dd
  10:     0x7f9bf656b485 - std::panicking::default_hook::hd5faae45a4c2ae6b
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:288:9
  11:     0x560f81d48dfd - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h62fc73136c5344f5
  12:     0x560f81d75d83 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::he03976a598c31555
  13:     0x7f9bf656bdd5 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h8fd551c79732d109
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1976:9
  14:     0x7f9bf656bdd5 - std::panicking::rust_panic_with_hook::hff0f13fd32920cda
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:695:13
  15:     0x7f9bf656bb49 - std::panicking::begin_panic_handler::{{closure}}::h4b94c172e12e7b79
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:582:13
  16:     0x7f9bf6569106 - std::sys_common::backtrace::__rust_end_short_backtrace::h0d54fda82a2d0073
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:150:18
  17:     0x7f9bf656b8a2 - rust_begin_unwind
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:578:5
  18:     0x7f9bf65c5eb3 - core::panicking::panic_fmt::h423e755c13523a61
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/panicking.rs:67:14
  19:     0x560f81f29a9a - cprover_bindings::goto_program::expr::Expr::call::h98f07a48d14e50cf
  20:     0x560f81cf3fdf - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator::hdccc300bfe0c600c
  21:     0x560f81d070a1 - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::h976e66498994fa63
  22:     0x560f81d3173e - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h72b866e5cefa4cb6
  23:     0x560f81d356d1 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::hd63a249ce3b650de
  24:     0x7f9bf89e4e26 - rustc_interface[bc622c2a0f547140]::passes::start_codegen
  25:     0x7f9bf89e2314 - <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>>
  26:     0x7f9bf89e1098 - <rustc_interface[bc622c2a0f547140]::queries::Queries>::ongoing_codegen
  27:     0x7f9bf89e087b - <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>>
  28:     0x7f9bf89de86f - 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}>
  29:     0x7f9bf89ddf00 - 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>>
  30:     0x7f9bf89dd821 - <<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}
  31:     0x7f9bf6576305 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hdbaea59c5dcd35ae
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1962:9
  32:     0x7f9bf6576305 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hedf781cff528734a
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1962:9
  33:     0x7f9bf6576305 - std::sys::unix::thread::Thread::new::thread_start::h8db1b8acf05cf216
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys/unix/thread.rs:108:17
  34:     0x7f9bf6310bb5 - <unknown>
  35:     0x7f9bf6392d90 - <unknown>
  36:                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: subslice_pattern_reassign::{closure#0}
_RNCNvCsbpocqJq3mfW_18dynamic_drop_async25subslice_pattern_reassign0B3_
[Kani] current codegen location: Loc { file: "/home/matthias/vcs/github/rust/tests/ui/drop/dynamic-drop-async.rs", function: None, start_line: 89, start_col: Some(54), end_line: 95, end_col: Some(2) }
error: /home/matthias/.kani/kani-0.29.0/bin/kani-compiler exited with status exit status: 101

[matthiaskrgr]

Still crashing with 0.40