From 6dfe0a0eb9a677c8832b651c041f0353bfb8cc88 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Wed, 13 Mar 2024 18:01:34 -0700
Subject: [PATCH] Add a multi-crate test for #3061 (#3076)

This is a follow-up on #3063 that adds a test with multiple crates to
make sure this scenario is correctly handled and that Kani reports the
bug.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 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();
+}