Added more tests for Drop

tests/kani/Drop/drop_after_move_closure_call.rs

@@ -0,0 +1,42 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that structs moved into Box<Fn> are dropped when
+//! the function is dropped.
+
+static mut CELL: i32 = 0;
+
+struct DropIncrementCELLByOne {}
+
+impl DropIncrementCELLByOne {
+    fn do_nothing(&self) {}
+}
+
+impl Drop for DropIncrementCELLByOne {
+    fn drop(&mut self) {
+        unsafe {
+            CELL += 1;
+        }
+    }
+}
+
+#[kani::proof]
+fn main() {
+    {
+        let object_to_drop = DropIncrementCELLByOne {};
+        let fun: Box<dyn FnOnce() -> ()> = Box::new(move || {
+            object_to_drop.do_nothing();
+        });
+
+        fun();
+    }
+    assert_eq!(unsafe { CELL }, 1, "Drop should be called when move fn is used");
+
+    {
+        let object_to_drop = DropIncrementCELLByOne {};
+        let _fun: Box<dyn FnOnce() -> ()> = Box::new(move || {
+            object_to_drop.do_nothing();
+        });
+    }
+    assert_eq!(unsafe { CELL }, 2, "Drop should still be called when move fn is not used");
+}

tests/kani/Drop/drop_after_mutating_refcell.rs

@@ -0,0 +1,54 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks whether dropping after mutating with
+//! Rc<Refcell<>> is handled correctly.
+//
+// Note: If you were to use Rc<RefCell<dyn CELLValueInFuture>>, then
+// kani will fail with an unsupported feature error. This is because
+// RefCell uses UnsafeCell inside, and that is not entirely supported
+// as of kani 0.4.0.
+
+use std::cell::RefCell;
+use std::rc::Rc;
+
+static mut CELL: i32 = 0;
+
+trait CELLValueInFuture {
+    fn set_inner_value(&mut self, new_value: i32);
+    fn get_inner_value(&self) -> i32;
+}
+
+struct DropSetCELLToInner {
+    set_cell_to: i32,
+}
+
+impl CELLValueInFuture for DropSetCELLToInner {
+    fn set_inner_value(&mut self, new_value: i32) {
+        self.set_cell_to = new_value;
+    }
+
+    fn get_inner_value(&self) -> i32 {
+        self.set_cell_to
+    }
+}
+
+impl Drop for DropSetCELLToInner {
+    fn drop(&mut self) {
+        unsafe {
+            CELL = self.get_inner_value();
+        }
+    }
+}
+
+#[kani::proof]
+fn main() {
+    {
+        let set_to_one = DropSetCELLToInner { set_cell_to: 1 };
+        let wrapped_drop: Rc<RefCell<DropSetCELLToInner>> = Rc::new(RefCell::new(set_to_one));
+
+        wrapped_drop.borrow_mut().set_inner_value(2);
+        assert_eq!(wrapped_drop.borrow().get_inner_value(), 2, "Value should be updated.");
+    }
+    assert_eq!(unsafe { CELL }, 2, "Drop should be called. New value used during drop.");
+}

tests/kani/Drop/drop_enum_only_one_called.rs

@@ -0,0 +1,41 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Property that dropping enum drops exactly 1 case.
+
+static mut CELL: i32 = 0;
+
+struct IncrementCELLWhenDropped {
+    increment_by: i32,
+}
+
+impl Drop for IncrementCELLWhenDropped {
+    fn drop(&mut self) {
+        unsafe {
+            CELL += self.increment_by;
+        }
+    }
+}
+
+enum EnumWithTwoIncrements {
+    Add1(IncrementCELLWhenDropped),
+    Add2(IncrementCELLWhenDropped),
+}
+
+fn get_random_enum_variant() -> EnumWithTwoIncrements {
+    if kani::any() {
+        EnumWithTwoIncrements::Add1(IncrementCELLWhenDropped { increment_by: 1 })
+    } else {
+        EnumWithTwoIncrements::Add2(IncrementCELLWhenDropped { increment_by: 2 })
+    }
+}
+
+#[kani::proof]
+fn main() {
+    {
+        let _e1 = get_random_enum_variant();
+    }
+    unsafe {
+        assert!(CELL == 1 || CELL == 2);
+    }
+}

tests/kani/Drop/fixme_drop_after_moving_across_channel.rs

@@ -0,0 +1,35 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks whether dropping objects passed through
+//! std::sync::mpsc::channel is handled.
+//
+// This test case fails to resolve in a reasonable amount of
+// time. Settign kani::unwind(1) is insufficient for verification, but
+// kani::unwind(2) takes longer than 10m on a M1 Mac. For details,
+// please see: https://github.com/model-checking/kani/issues/1286
+
+use std::sync::mpsc::*;
+
+static mut CELL: i32 = 0;
+
+struct DropSetCELLToOne {}
+
+impl Drop for DropSetCELLToOne {
+    fn drop(&mut self) {
+        unsafe {
+            CELL = 1;
+        }
+    }
+}
+
+#[kani::unwind(1)]
+#[kani::proof]
+fn main() {
+    {
+        let (send, recv) = channel::<DropSetCELLToOne>();
+        send.send(DropSetCELLToOne {}).unwrap();
+        let _to_drop: DropSetCELLToOne = recv.recv().unwrap();
+    }
+    assert_eq!(unsafe { CELL }, 1, "Drop should be called");
+}

tests/kani/Drop/forget_no_drop.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Tests the property that if you let memory leak via
+//! std::mem::forget, drop will not be called.
+
+static mut CELL: i32 = 0;
+
+struct IncrementCELLWhenDropped;
+impl Drop for IncrementCELLWhenDropped {
+    fn drop(&mut self) {
+        unsafe {
+            CELL = 1;
+        }
+    }
+}
+
+#[kani::proof]
+fn main() {
+    {
+        let x1 = IncrementCELLWhenDropped {};
+        std::mem::forget(x1);
+    }
+    unsafe {
+        assert!(CELL == 0);
+    }
+}