ICE: Argument doesn't check / Function call does not type check #2497
Description
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