From b453484d204b2eb4a5460865a06e10137fc20b97 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 24 Apr 2023 17:23:14 +0000 Subject: [PATCH 1/4] Add `Arbitrary` implementation for `Box` --- library/kani/src/arbitrary.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 2e13f90e3aef..2d89e7084d36 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -161,3 +161,12 @@ impl Arbitrary for std::marker::PhantomPinned { PhantomPinned } } + +impl Arbitrary for std::boxed::Box +where + T: Arbitrary, +{ + fn any() -> Self { + Box::new(T::any()) + } +} From 736df8ba86ea2fc37844d98469e2d1bb7d37ba90 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 24 Apr 2023 20:25:37 +0000 Subject: [PATCH 2/4] Add test --- tests/expected/derive-arbitrary/box/expected | 7 +++++++ tests/expected/derive-arbitrary/box/test.rs | 18 ++++++++++++++++++ 2 files changed, 25 insertions(+) create mode 100644 tests/expected/derive-arbitrary/box/expected create mode 100644 tests/expected/derive-arbitrary/box/test.rs diff --git a/tests/expected/derive-arbitrary/box/expected b/tests/expected/derive-arbitrary/box/expected new file mode 100644 index 000000000000..b524388a59ff --- /dev/null +++ b/tests/expected/derive-arbitrary/box/expected @@ -0,0 +1,7 @@ +Status: SATISFIED\ +Description: "cover condition: *foo.boxed >= i32::MIN && *foo.boxed <= i32::MAX" +Status: UNSATISFIABLE\ +Description: "cover condition: *foo.boxed < i32::MIN" +Status: UNSATISFIABLE\ +Description: "cover condition: *foo.boxed > i32::MAX" +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/derive-arbitrary/box/test.rs b/tests/expected/derive-arbitrary/box/test.rs new file mode 100644 index 000000000000..d9e3ac75295b --- /dev/null +++ b/tests/expected/derive-arbitrary/box/test.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that Kani can automatically derive `Arbitrary` on a struct with a +//! member of type `Box` + +#[derive(kani::Arbitrary)] +struct Foo { + boxed: Box, +} + +#[kani::proof] +fn main() { + let foo: Foo = kani::any(); + kani::cover!(*foo.boxed >= i32::MIN && *foo.boxed <= i32::MAX); + kani::cover!(*foo.boxed < i32::MIN); // <-- this condition should be `UNSATISFIABLE` + kani::cover!(*foo.boxed > i32::MAX); // <-- this condition should be `UNSATISFIABLE` +} From ea83eec82d88226ec965a57e077b91404087c147 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 24 Apr 2023 20:28:55 +0000 Subject: [PATCH 3/4] Move phantom data tests to `expected` --- tests/{ui => expected}/derive-arbitrary/phantom_data/expected | 0 tests/{ui => expected}/derive-arbitrary/phantom_data/test.rs | 0 tests/{ui => expected}/derive-arbitrary/phantom_pinned/expected | 0 tests/{ui => expected}/derive-arbitrary/phantom_pinned/test.rs | 0 4 files changed, 0 insertions(+), 0 deletions(-) rename tests/{ui => expected}/derive-arbitrary/phantom_data/expected (100%) rename tests/{ui => expected}/derive-arbitrary/phantom_data/test.rs (100%) rename tests/{ui => expected}/derive-arbitrary/phantom_pinned/expected (100%) rename tests/{ui => expected}/derive-arbitrary/phantom_pinned/test.rs (100%) diff --git a/tests/ui/derive-arbitrary/phantom_data/expected b/tests/expected/derive-arbitrary/phantom_data/expected similarity index 100% rename from tests/ui/derive-arbitrary/phantom_data/expected rename to tests/expected/derive-arbitrary/phantom_data/expected diff --git a/tests/ui/derive-arbitrary/phantom_data/test.rs b/tests/expected/derive-arbitrary/phantom_data/test.rs similarity index 100% rename from tests/ui/derive-arbitrary/phantom_data/test.rs rename to tests/expected/derive-arbitrary/phantom_data/test.rs diff --git a/tests/ui/derive-arbitrary/phantom_pinned/expected b/tests/expected/derive-arbitrary/phantom_pinned/expected similarity index 100% rename from tests/ui/derive-arbitrary/phantom_pinned/expected rename to tests/expected/derive-arbitrary/phantom_pinned/expected diff --git a/tests/ui/derive-arbitrary/phantom_pinned/test.rs b/tests/expected/derive-arbitrary/phantom_pinned/test.rs similarity index 100% rename from tests/ui/derive-arbitrary/phantom_pinned/test.rs rename to tests/expected/derive-arbitrary/phantom_pinned/test.rs From d5934f81e666287aab6757b439e435749430e0b9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 25 Apr 2023 20:29:09 +0000 Subject: [PATCH 4/4] Cover specific cases instead of ranges --- tests/expected/derive-arbitrary/box/expected | 6 +++++- tests/expected/derive-arbitrary/box/test.rs | 4 +++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/tests/expected/derive-arbitrary/box/expected b/tests/expected/derive-arbitrary/box/expected index b524388a59ff..4cef537ffd6a 100644 --- a/tests/expected/derive-arbitrary/box/expected +++ b/tests/expected/derive-arbitrary/box/expected @@ -1,5 +1,9 @@ Status: SATISFIED\ -Description: "cover condition: *foo.boxed >= i32::MIN && *foo.boxed <= i32::MAX" +Description: "cover condition: *foo.boxed == i32::MIN" +Status: SATISFIED\ +Description: "cover condition: *foo.boxed == 0" +Status: SATISFIED\ +Description: "cover condition: *foo.boxed == i32::MAX" Status: UNSATISFIABLE\ Description: "cover condition: *foo.boxed < i32::MIN" Status: UNSATISFIABLE\ diff --git a/tests/expected/derive-arbitrary/box/test.rs b/tests/expected/derive-arbitrary/box/test.rs index d9e3ac75295b..f3e95115a6d4 100644 --- a/tests/expected/derive-arbitrary/box/test.rs +++ b/tests/expected/derive-arbitrary/box/test.rs @@ -12,7 +12,9 @@ struct Foo { #[kani::proof] fn main() { let foo: Foo = kani::any(); - kani::cover!(*foo.boxed >= i32::MIN && *foo.boxed <= i32::MAX); + kani::cover!(*foo.boxed == i32::MIN); + kani::cover!(*foo.boxed == 0); + kani::cover!(*foo.boxed == i32::MAX); kani::cover!(*foo.boxed < i32::MIN); // <-- this condition should be `UNSATISFIABLE` kani::cover!(*foo.boxed > i32::MAX); // <-- this condition should be `UNSATISFIABLE` }