From c1c71df9573f11e8bea0aee7b30ced3d1ac70f20 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Tue, 14 Jun 2022 18:32:11 -0400 Subject: [PATCH 01/16] Temp commit to suppress aarch64 (m1)issues. Do not commit to master. --- .../src/codegen_cprover_gotoc/compiler_interface.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 6a39fcd9129b..db559a1ea0d7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -225,12 +225,13 @@ fn check_target(session: &Session) { // The requirement below is needed to build a valid CBMC machine model // in function `machine_model_from_session` from // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs - let is_linux_target = session.target.llvm_target == "x86_64-unknown-linux-gnu"; + let _is_linux_target = session.target.llvm_target == "x86_64-unknown-linux-gnu"; // Comparison with `x86_64-apple-darwin` does not work well because the LLVM // target may become `x86_64-apple-macosx10.7.0` (or similar) and fail - let is_darwin_target = session.target.llvm_target.starts_with("x86_64-apple-"); + let _is_darwin_target = session.target.llvm_target.starts_with("x86_64-apple-"); - if !is_linux_target && !is_darwin_target { + if false { + // !is_linux_target && !is_darwin_target { let err_msg = format!( "Kani requires the target platform to be `x86_64-unknown-linux-gnu` or `x86_64-apple-darwin`, but it is {}", &session.target.llvm_target From 2894176fe8c6e602c47b2b99369cedac1431604a Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Tue, 14 Jun 2022 19:22:22 -0400 Subject: [PATCH 02/16] Added enum drop only 1 test. TODO: Add to regressions. --- tests/kani/Enum/drop_enum_only_one_called.rs | 41 ++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 tests/kani/Enum/drop_enum_only_one_called.rs diff --git a/tests/kani/Enum/drop_enum_only_one_called.rs b/tests/kani/Enum/drop_enum_only_one_called.rs new file mode 100644 index 000000000000..3e1aa7527129 --- /dev/null +++ b/tests/kani/Enum/drop_enum_only_one_called.rs @@ -0,0 +1,41 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check drop implementation for an &dyn dynamic trait object. + +static mut CELL: i32 = 0; + +trait T { + fn t(&self) {} +} + +enum EnumWithDifferentDrop { + Add1, + Add2, +} + +impl Drop for EnumWithDifferentDrop { + fn drop(&mut self) { + unsafe { + match self { + EnumWithDifferentDrop::Add1 => CELL += 1, + EnumWithDifferentDrop::Add2 => CELL += 2, + } + } + } +} + +fn get_random_enum_variant(random: u32) -> EnumWithDifferentDrop { + if random % 2 == 0 { EnumWithDifferentDrop::Add1 } else { EnumWithDifferentDrop::Add2 } +} + +#[kani::proof] +fn main() { + { + let _e1 = get_random_enum_variant(kani::any()); + } + unsafe { + assert!(CELL == 1 || CELL == 2); + assert!(CELL != 3); + } +} From aa3170a6a0f18c7f69eb43fc50c72d7f889051ff Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Wed, 15 Jun 2022 11:01:58 -0400 Subject: [PATCH 03/16] Errata: Redundant asert, unused trait, and incorrect comment. --- tests/kani/Enum/drop_enum_only_one_called.rs | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/tests/kani/Enum/drop_enum_only_one_called.rs b/tests/kani/Enum/drop_enum_only_one_called.rs index 3e1aa7527129..409c2c7c7801 100644 --- a/tests/kani/Enum/drop_enum_only_one_called.rs +++ b/tests/kani/Enum/drop_enum_only_one_called.rs @@ -1,14 +1,10 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check drop implementation for an &dyn dynamic trait object. +// Property that dropping enum drops exactly 1 case. static mut CELL: i32 = 0; -trait T { - fn t(&self) {} -} - enum EnumWithDifferentDrop { Add1, Add2, @@ -36,6 +32,5 @@ fn main() { } unsafe { assert!(CELL == 1 || CELL == 2); - assert!(CELL != 3); } } From 766b78504b4482e2de553542a3ae44bf7a6e322d Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Wed, 15 Jun 2022 11:07:02 -0400 Subject: [PATCH 04/16] Made selective drop be the inner type inside enum. --- tests/kani/Enum/drop_enum_only_one_called.rs | 25 ++++++++++++-------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/tests/kani/Enum/drop_enum_only_one_called.rs b/tests/kani/Enum/drop_enum_only_one_called.rs index 409c2c7c7801..1abe40a50b77 100644 --- a/tests/kani/Enum/drop_enum_only_one_called.rs +++ b/tests/kani/Enum/drop_enum_only_one_called.rs @@ -5,24 +5,29 @@ static mut CELL: i32 = 0; -enum EnumWithDifferentDrop { - Add1, - Add2, +struct IncrementCELLWhenDropped { + increment_by: i32, } -impl Drop for EnumWithDifferentDrop { +impl Drop for IncrementCELLWhenDropped { fn drop(&mut self) { unsafe { - match self { - EnumWithDifferentDrop::Add1 => CELL += 1, - EnumWithDifferentDrop::Add2 => CELL += 2, - } + CELL += self.increment_by; } } } -fn get_random_enum_variant(random: u32) -> EnumWithDifferentDrop { - if random % 2 == 0 { EnumWithDifferentDrop::Add1 } else { EnumWithDifferentDrop::Add2 } +enum EnumWithTwoIncrements { + Add1(IncrementCELLWhenDropped), + Add2(IncrementCELLWhenDropped), +} + +fn get_random_enum_variant(random: u32) -> EnumWithTwoIncrements { + if random % 2 == 0 { + EnumWithTwoIncrements::Add1(IncrementCELLWhenDropped { increment_by: 1 }) + } else { + EnumWithTwoIncrements::Add2(IncrementCELLWhenDropped { increment_by: 2 }) + } } #[kani::proof] From fda65657162352b5c73b88fba6f8b0fa2868501d Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Thu, 16 Jun 2022 08:36:24 -0400 Subject: [PATCH 05/16] Add test for drop of objects that are moved into closures. --- .../Closure/drop_after_move_closure_call.rs | 42 +++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 tests/kani/Closure/drop_after_move_closure_call.rs diff --git a/tests/kani/Closure/drop_after_move_closure_call.rs b/tests/kani/Closure/drop_after_move_closure_call.rs new file mode 100644 index 000000000000..796217636dc9 --- /dev/null +++ b/tests/kani/Closure/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 is 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 ()> = 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 ()> = Box::new(move || { + object_to_drop.do_nothing(); + }); + } + assert_eq!(unsafe { CELL }, 2, "Drop should still be called when move fn is not used"); +} From beaf2d81838862780eb86bb48cded719e894bdeb Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Thu, 16 Jun 2022 09:22:14 -0400 Subject: [PATCH 06/16] Added tests dropping after ownership move: channel and RC+Refcell. --- .../kani/Drop/drop_after_mutating_refcell.rs | 53 +++++++++++++++++++ .../fixme_drop_after_moving_across_channel.rs | 30 +++++++++++ 2 files changed, 83 insertions(+) create mode 100644 tests/kani/Drop/drop_after_mutating_refcell.rs create mode 100644 tests/kani/Drop/fixme_drop_after_moving_across_channel.rs diff --git a/tests/kani/Drop/drop_after_mutating_refcell.rs b/tests/kani/Drop/drop_after_mutating_refcell.rs new file mode 100644 index 000000000000..be6fa4961bcd --- /dev/null +++ b/tests/kani/Drop/drop_after_mutating_refcell.rs @@ -0,0 +1,53 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test checks whether dropping after mutating with Rc> +// is handled correctly. +// +// Note: If you were to use Rc>, 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> = Rc::new(RefCell::new(set_to_one)); + + wrapped_drop.borrow_mut().set_inner_value(2); + } + assert_eq!(unsafe { CELL }, 2, "Drop should be called. New value used during drop."); +} diff --git a/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs b/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs new file mode 100644 index 000000000000..442e8c24dc07 --- /dev/null +++ b/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs @@ -0,0 +1,30 @@ +// 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. + +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::(); + send.send(DropSetCELLToOne {}).unwrap(); + let _to_drop: DropSetCELLToOne = recv.recv().unwrap(); + } + assert_eq!(unsafe { CELL }, 1, "Drop should be called"); +} From 0dc3b892ac1c015a050c12b0157274ce1300205e Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Thu, 16 Jun 2022 09:25:26 -0400 Subject: [PATCH 07/16] Undid M1 mac aarch hack --- .../src/codegen_cprover_gotoc/compiler_interface.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index db559a1ea0d7..6a39fcd9129b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -225,13 +225,12 @@ fn check_target(session: &Session) { // The requirement below is needed to build a valid CBMC machine model // in function `machine_model_from_session` from // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs - let _is_linux_target = session.target.llvm_target == "x86_64-unknown-linux-gnu"; + let is_linux_target = session.target.llvm_target == "x86_64-unknown-linux-gnu"; // Comparison with `x86_64-apple-darwin` does not work well because the LLVM // target may become `x86_64-apple-macosx10.7.0` (or similar) and fail - let _is_darwin_target = session.target.llvm_target.starts_with("x86_64-apple-"); + let is_darwin_target = session.target.llvm_target.starts_with("x86_64-apple-"); - if false { - // !is_linux_target && !is_darwin_target { + if !is_linux_target && !is_darwin_target { let err_msg = format!( "Kani requires the target platform to be `x86_64-unknown-linux-gnu` or `x86_64-apple-darwin`, but it is {}", &session.target.llvm_target From bca58b6da2bc85aa343807d3621029222d4328ca Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Thu, 16 Jun 2022 09:33:44 -0400 Subject: [PATCH 08/16] Added comment for why test case is fixme. --- tests/kani/Drop/fixme_drop_after_moving_across_channel.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs b/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs index 442e8c24dc07..ba941c704e41 100644 --- a/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs +++ b/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs @@ -3,6 +3,10 @@ // 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. use std::sync::mpsc::*; From 5317bfaba867fcda15e9adada91bfdd5957a6f1b Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Thu, 16 Jun 2022 11:20:14 -0400 Subject: [PATCH 09/16] fixed is/are typo Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- tests/kani/Closure/drop_after_move_closure_call.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/kani/Closure/drop_after_move_closure_call.rs b/tests/kani/Closure/drop_after_move_closure_call.rs index 796217636dc9..3774456fc2cf 100644 --- a/tests/kani/Closure/drop_after_move_closure_call.rs +++ b/tests/kani/Closure/drop_after_move_closure_call.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// This test checks that structs moved into Box is dropped when +// This test checks that structs moved into Box are dropped when // the function is dropped. static mut CELL: i32 = 0; From 6057cd1f2a527829597df9c2f1581b2ef0a92f62 Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Thu, 16 Jun 2022 11:22:55 -0400 Subject: [PATCH 10/16] Use kani::any() instead of input. @adpaco-aws's suggestion. --- tests/kani/Enum/drop_enum_only_one_called.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/kani/Enum/drop_enum_only_one_called.rs b/tests/kani/Enum/drop_enum_only_one_called.rs index 1abe40a50b77..5a120b5dab21 100644 --- a/tests/kani/Enum/drop_enum_only_one_called.rs +++ b/tests/kani/Enum/drop_enum_only_one_called.rs @@ -22,8 +22,8 @@ enum EnumWithTwoIncrements { Add2(IncrementCELLWhenDropped), } -fn get_random_enum_variant(random: u32) -> EnumWithTwoIncrements { - if random % 2 == 0 { +fn get_random_enum_variant() -> EnumWithTwoIncrements { + if kani::any() { EnumWithTwoIncrements::Add1(IncrementCELLWhenDropped { increment_by: 1 }) } else { EnumWithTwoIncrements::Add2(IncrementCELLWhenDropped { increment_by: 2 }) @@ -33,7 +33,7 @@ fn get_random_enum_variant(random: u32) -> EnumWithTwoIncrements { #[kani::proof] fn main() { { - let _e1 = get_random_enum_variant(kani::any()); + let _e1 = get_random_enum_variant(); } unsafe { assert!(CELL == 1 || CELL == 2); From 5c57e17cf418c3e99f593bf3343431b0eae7c52d Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Thu, 16 Jun 2022 12:46:27 -0400 Subject: [PATCH 11/16] Added link to issue. --- tests/kani/Drop/fixme_drop_after_moving_across_channel.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs b/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs index ba941c704e41..2a2d05c803ce 100644 --- a/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs +++ b/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs @@ -6,7 +6,8 @@ // // 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. +// 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::*; From 0f35141944f0d61d5f2c7a64adac59f6194ba572 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Thu, 16 Jun 2022 12:55:23 -0400 Subject: [PATCH 12/16] Changed to inner comment. --- tests/kani/Drop/fixme_drop_after_moving_across_channel.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs b/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs index 2a2d05c803ce..8ab694ef98e3 100644 --- a/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs +++ b/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs @@ -1,8 +1,8 @@ // 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 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 From 75cc1c717054030debe5ff966c8d54e5b955d646 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Thu, 16 Jun 2022 12:58:09 -0400 Subject: [PATCH 13/16] Changed to inner comment. Forgot 3 other files. --- tests/kani/Closure/drop_after_move_closure_call.rs | 4 ++-- tests/kani/Drop/drop_after_mutating_refcell.rs | 4 ++-- tests/kani/Enum/drop_enum_only_one_called.rs | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/kani/Closure/drop_after_move_closure_call.rs b/tests/kani/Closure/drop_after_move_closure_call.rs index 3774456fc2cf..ee3ab2483de0 100644 --- a/tests/kani/Closure/drop_after_move_closure_call.rs +++ b/tests/kani/Closure/drop_after_move_closure_call.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// This test checks that structs moved into Box are dropped when -// the function is dropped. +//! This test checks that structs moved into Box are dropped when +//! the function is dropped. static mut CELL: i32 = 0; diff --git a/tests/kani/Drop/drop_after_mutating_refcell.rs b/tests/kani/Drop/drop_after_mutating_refcell.rs index be6fa4961bcd..29d67a340806 100644 --- a/tests/kani/Drop/drop_after_mutating_refcell.rs +++ b/tests/kani/Drop/drop_after_mutating_refcell.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// This test checks whether dropping after mutating with Rc> -// is handled correctly. +//! This test checks whether dropping after mutating with +//! Rc> is handled correctly. // // Note: If you were to use Rc>, then // kani will fail with an unsupported feature error. This is because diff --git a/tests/kani/Enum/drop_enum_only_one_called.rs b/tests/kani/Enum/drop_enum_only_one_called.rs index 5a120b5dab21..db3199403054 100644 --- a/tests/kani/Enum/drop_enum_only_one_called.rs +++ b/tests/kani/Enum/drop_enum_only_one_called.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Property that dropping enum drops exactly 1 case. +//! Property that dropping enum drops exactly 1 case. static mut CELL: i32 = 0; From 5f5203b52fd83eb9e10babe619f55164d75ff832 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Thu, 16 Jun 2022 13:56:21 -0400 Subject: [PATCH 14/16] Added assertion to check for update. --- tests/kani/Drop/drop_after_mutating_refcell.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/kani/Drop/drop_after_mutating_refcell.rs b/tests/kani/Drop/drop_after_mutating_refcell.rs index 29d67a340806..4b5553bd87ca 100644 --- a/tests/kani/Drop/drop_after_mutating_refcell.rs +++ b/tests/kani/Drop/drop_after_mutating_refcell.rs @@ -48,6 +48,7 @@ fn main() { let wrapped_drop: Rc> = 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."); } From 53e517796c59ca405de21c0da288a574f2bfd9bd Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Thu, 16 Jun 2022 14:10:38 -0400 Subject: [PATCH 15/16] Moved all drop-related ests to tests/kani/Drop --- tests/kani/{Closure => Drop}/drop_after_move_closure_call.rs | 0 tests/kani/{DynTrait => Drop}/drop_boxed_dyn.rs | 0 tests/kani/{DynTrait => Drop}/drop_concrete.rs | 0 tests/kani/{DynTrait => Drop}/drop_dyn_pointer.rs | 0 tests/kani/{Enum => Drop}/drop_enum_only_one_called.rs | 0 tests/kani/{DynTrait => Drop}/drop_nested_boxed_dyn.rs | 0 tests/kani/{DynTrait => Drop}/drop_nested_boxed_dyn_fail.rs | 0 tests/kani/{DynTrait => Drop}/rc_dyn.rs | 0 8 files changed, 0 insertions(+), 0 deletions(-) rename tests/kani/{Closure => Drop}/drop_after_move_closure_call.rs (100%) rename tests/kani/{DynTrait => Drop}/drop_boxed_dyn.rs (100%) rename tests/kani/{DynTrait => Drop}/drop_concrete.rs (100%) rename tests/kani/{DynTrait => Drop}/drop_dyn_pointer.rs (100%) rename tests/kani/{Enum => Drop}/drop_enum_only_one_called.rs (100%) rename tests/kani/{DynTrait => Drop}/drop_nested_boxed_dyn.rs (100%) rename tests/kani/{DynTrait => Drop}/drop_nested_boxed_dyn_fail.rs (100%) rename tests/kani/{DynTrait => Drop}/rc_dyn.rs (100%) diff --git a/tests/kani/Closure/drop_after_move_closure_call.rs b/tests/kani/Drop/drop_after_move_closure_call.rs similarity index 100% rename from tests/kani/Closure/drop_after_move_closure_call.rs rename to tests/kani/Drop/drop_after_move_closure_call.rs diff --git a/tests/kani/DynTrait/drop_boxed_dyn.rs b/tests/kani/Drop/drop_boxed_dyn.rs similarity index 100% rename from tests/kani/DynTrait/drop_boxed_dyn.rs rename to tests/kani/Drop/drop_boxed_dyn.rs diff --git a/tests/kani/DynTrait/drop_concrete.rs b/tests/kani/Drop/drop_concrete.rs similarity index 100% rename from tests/kani/DynTrait/drop_concrete.rs rename to tests/kani/Drop/drop_concrete.rs diff --git a/tests/kani/DynTrait/drop_dyn_pointer.rs b/tests/kani/Drop/drop_dyn_pointer.rs similarity index 100% rename from tests/kani/DynTrait/drop_dyn_pointer.rs rename to tests/kani/Drop/drop_dyn_pointer.rs diff --git a/tests/kani/Enum/drop_enum_only_one_called.rs b/tests/kani/Drop/drop_enum_only_one_called.rs similarity index 100% rename from tests/kani/Enum/drop_enum_only_one_called.rs rename to tests/kani/Drop/drop_enum_only_one_called.rs diff --git a/tests/kani/DynTrait/drop_nested_boxed_dyn.rs b/tests/kani/Drop/drop_nested_boxed_dyn.rs similarity index 100% rename from tests/kani/DynTrait/drop_nested_boxed_dyn.rs rename to tests/kani/Drop/drop_nested_boxed_dyn.rs diff --git a/tests/kani/DynTrait/drop_nested_boxed_dyn_fail.rs b/tests/kani/Drop/drop_nested_boxed_dyn_fail.rs similarity index 100% rename from tests/kani/DynTrait/drop_nested_boxed_dyn_fail.rs rename to tests/kani/Drop/drop_nested_boxed_dyn_fail.rs diff --git a/tests/kani/DynTrait/rc_dyn.rs b/tests/kani/Drop/rc_dyn.rs similarity index 100% rename from tests/kani/DynTrait/rc_dyn.rs rename to tests/kani/Drop/rc_dyn.rs From e7996f11a25e3112b5197d3e517db1d4d08a63af Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Thu, 16 Jun 2022 14:58:27 -0400 Subject: [PATCH 16/16] Added test case for forgotten memory. --- tests/kani/Drop/forget_no_drop.rs | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 tests/kani/Drop/forget_no_drop.rs diff --git a/tests/kani/Drop/forget_no_drop.rs b/tests/kani/Drop/forget_no_drop.rs new file mode 100644 index 000000000000..81e84c00df6e --- /dev/null +++ b/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); + } +}