Open matthiaskrgr opened 1 year ago
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
Still crashing with 0.40
matthiaskrgr
commented
10 months ago matthiaskrgr
commented
10 months ago
I tried this code:
using the following command line invocation:
with Kani version: kani 0.29.0
I expected to see this happen: explanation
Instead, this happened: explanation