From e6872d4cb65a199756cc32e98f0bbede353d4ef8 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 13 Mar 2024 16:31:17 -0700 Subject: [PATCH] Add a multi-crate test for #3061 --- tests/cargo-kani/storage-markers/Cargo.toml | 5 +++++ .../storage-markers/crate-with-bug/Cargo.toml | 8 ++++++++ .../storage-markers/crate-with-bug/src/lib.rs | 12 ++++++++++++ .../storage-markers/crate-with-harness/Cargo.toml | 9 +++++++++ .../crate-with-harness/call_fn_with_bug.expected | 3 +++ .../storage-markers/crate-with-harness/src/lib.rs | 11 +++++++++++ 6 files changed, 48 insertions(+) create mode 100644 tests/cargo-kani/storage-markers/Cargo.toml create mode 100644 tests/cargo-kani/storage-markers/crate-with-bug/Cargo.toml create mode 100644 tests/cargo-kani/storage-markers/crate-with-bug/src/lib.rs create mode 100644 tests/cargo-kani/storage-markers/crate-with-harness/Cargo.toml create mode 100644 tests/cargo-kani/storage-markers/crate-with-harness/call_fn_with_bug.expected create mode 100644 tests/cargo-kani/storage-markers/crate-with-harness/src/lib.rs diff --git a/tests/cargo-kani/storage-markers/Cargo.toml b/tests/cargo-kani/storage-markers/Cargo.toml new file mode 100644 index 000000000000..cb98b6df5835 --- /dev/null +++ b/tests/cargo-kani/storage-markers/Cargo.toml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[workspace] +members = ["crate-with-bug", "crate-with-harness"] +resolver = "2" diff --git a/tests/cargo-kani/storage-markers/crate-with-bug/Cargo.toml b/tests/cargo-kani/storage-markers/crate-with-bug/Cargo.toml new file mode 100644 index 000000000000..3cec8dac16b0 --- /dev/null +++ b/tests/cargo-kani/storage-markers/crate-with-bug/Cargo.toml @@ -0,0 +1,8 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "crate-with-bug" +version = "0.1.0" +edition = "2021" + +[dependencies] diff --git a/tests/cargo-kani/storage-markers/crate-with-bug/src/lib.rs b/tests/cargo-kani/storage-markers/crate-with-bug/src/lib.rs new file mode 100644 index 000000000000..3e6967bdbfe4 --- /dev/null +++ b/tests/cargo-kani/storage-markers/crate-with-bug/src/lib.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This function contains a use-after-free bug. + +pub fn fn_with_bug() -> i32 { + let raw_ptr = { + let var = 10; + &var as *const i32 + }; + unsafe { *raw_ptr } +} diff --git a/tests/cargo-kani/storage-markers/crate-with-harness/Cargo.toml b/tests/cargo-kani/storage-markers/crate-with-harness/Cargo.toml new file mode 100644 index 000000000000..7cfe7126d845 --- /dev/null +++ b/tests/cargo-kani/storage-markers/crate-with-harness/Cargo.toml @@ -0,0 +1,9 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "crate-with-harness" +version = "0.1.0" +edition = "2021" + +[dependencies] +crate-with-bug = { path = "../crate-with-bug" } diff --git a/tests/cargo-kani/storage-markers/crate-with-harness/call_fn_with_bug.expected b/tests/cargo-kani/storage-markers/crate-with-harness/call_fn_with_bug.expected new file mode 100644 index 000000000000..68ef53cc06ec --- /dev/null +++ b/tests/cargo-kani/storage-markers/crate-with-harness/call_fn_with_bug.expected @@ -0,0 +1,3 @@ +Status: FAILURE\ +Description: "dereference failure: dead object"\ +in function crate_with_bug::fn_with_bug diff --git a/tests/cargo-kani/storage-markers/crate-with-harness/src/lib.rs b/tests/cargo-kani/storage-markers/crate-with-harness/src/lib.rs new file mode 100644 index 000000000000..a44cfaf976be --- /dev/null +++ b/tests/cargo-kani/storage-markers/crate-with-harness/src/lib.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test checks that Kani captures the case of a use-after-free issue as +// described in https://github.com/model-checking/kani/issues/3061 even across +// crates. The test calls a function from another crate that has the bug. + +#[kani::proof] +pub fn call_fn_with_bug() { + let _x = crate_with_bug::fn_with_bug(); +}