Kani implementation of drop for Struct<dyn T> is broken

[celinval]

We were handling drop_in_place incorrectly when the object to be dropped had type Struct<dyn T> like in the example below.

For now, we are going to codegen unimplemented, so if this code is reachable, the verification will fail.

I tried this code:

use std::rc::Rc;

pub trait DummyTrait {}

pub struct Wrapper<T: ?Sized> {
    pub w_id: u128,
    pub inner: T,
}

impl<T: ?Sized> Drop for Wrapper<T> {
    fn drop(&mut self) {
        assert_eq!(self.w_id, 0);
    }
}

struct DummyImpl {
    pub id: u128,
}

impl DummyTrait for DummyImpl {}

impl Drop for DummyImpl {
    fn drop(&mut self) {
        assert_eq!(self.id, 1);
    }
}

#[kani::proof]
fn check_drop_dyn() {
    let original = Rc::new(Wrapper { w_id: 0, inner: DummyImpl { id: 1 } });
    let _wrapper =
        unsafe { Rc::from_raw(Rc::into_raw(original) as *const Wrapper<dyn DummyTrait>) };
}

using the following command line invocation:

kani check.rs

with Kani version:

I expected to see this happen: Harness should succeed.

Instead, this happened:

• With codegen unimplemented check, this harness fails with:

Failed Checks: drop unsized struct: Wrapper<dyn DummyTrait>

• Without codegen unimplemented check, this harness fails with:

Failed Checks: assertion failed: self.id == 1

[tedinski]

I think the fix for this MIGHT be to refactor the "virtual table drop" code to actually call the normal virtual table invocation code, instead of sort of duplicating it, apparently incorrectly. I'm not sure if that's the only issue here however.

Also, this refactoring is not quite as straightforward as it sounds for uninteresting reasons: drop returns unit/void, but our existing virtual table function invocation code expects a Place to store the return value. So THAT in turn needs refactoring to separate out those two steps, which in turn suggests some refactorings to codegen_function...