From 1e0b71dfa44176c32d1ac80bfee375c6ff64d5b8 Mon Sep 17 00:00:00 2001
From: Matias Scharager <matias.scharager@gmail.com>
Date: Tue, 30 Jul 2024 00:11:40 -0400
Subject: [PATCH] Function Contracts: Interior Mutability Tests (#3351)

Test cases for interior mutability using Cell, OnceCell, UnsafeCell, and
RefCell.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Matias Scharager <mscharag@amazon.com>
Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>
---
 .../interior-mutability/api/cell.expected     |  6 +++
 .../interior-mutability/api/cell.rs           | 25 ++++++++++++
 .../api/cell_stub.expected                    |  9 +++++
 .../interior-mutability/api/cell_stub.rs      | 40 +++++++++++++++++++
 .../api/unsafecell.expected                   |  6 +++
 .../interior-mutability/api/unsafecell.rs     | 24 +++++++++++
 .../whole-struct/cell.expected                |  6 +++
 .../interior-mutability/whole-struct/cell.rs  | 25 ++++++++++++
 .../whole-struct/oncecell.expected            |  6 +++
 .../whole-struct/oncecell.rs                  | 24 +++++++++++
 .../whole-struct/refcell.expected             |  6 +++
 .../whole-struct/refcell.rs                   | 25 ++++++++++++
 .../whole-struct/unsafecell.expected          |  6 +++
 .../whole-struct/unsafecell.rs                | 25 ++++++++++++
 14 files changed, 233 insertions(+)
 create mode 100644 tests/expected/function-contract/interior-mutability/api/cell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/api/cell.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/api/cell_stub.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/api/cell_stub.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/api/unsafecell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/api/unsafecell.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/cell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected
 create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs

diff --git a/tests/expected/function-contract/interior-mutability/api/cell.expected b/tests/expected/function-contract/interior-mutability/api/cell.expected
new file mode 100644
index 000000000000..d9b0f5d51e5c
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get() < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/api/cell.rs b/tests/expected/function-contract/interior-mutability/api/cell.rs
new file mode 100644
index 000000000000..671b6b206ef3
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// Mutating Cell via `as_ptr` in contracts
+use std::cell::Cell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(im.x.as_ptr())]
+#[kani::ensures(|_| im.x.get() < 101)]
+///im is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    im.x.set(im.x.get() + 1)
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.expected b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected
new file mode 100644
index 000000000000..b8da35411e53
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected
@@ -0,0 +1,9 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| old(im.x.get() + im.x.get()) == im.x.get()"\
+
+assertion\
+- Status: SUCCESS\
+- Description: "|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get()"\
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
new file mode 100644
index 000000000000..d01ca379655f
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
@@ -0,0 +1,40 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple.
+/// This shows that we can generate `kani::any()` for Cell.
+use std::cell::Cell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::ensures(|_| old(im.x.get() + im.x.get()) == im.x.get())]
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(im.x.as_ptr())]
+fn double(im: &InteriorMutability) {
+    im.x.set(im.x.get() + im.x.get())
+}
+
+#[kani::proof_for_contract(double)]
+fn double_harness() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    double(&im);
+}
+
+#[kani::ensures(|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get())]
+#[kani::requires(im.x.get() < 50)]
+#[kani::modifies(im.x.as_ptr())]
+fn quadruple(im: &InteriorMutability) {
+    double(im);
+    double(im)
+}
+
+#[kani::proof_for_contract(quadruple)]
+#[kani::stub_verified(double)]
+fn quadruple_harness() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    quadruple(&im);
+}
diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.expected b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected
new file mode 100644
index 000000000000..1646a8a78e7f
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.get() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
new file mode 100644
index 000000000000..8125e3e3c077
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+use std::cell::UnsafeCell;
+
+/// This struct contains UnsafeCell which can be mutated
+struct InteriorMutability {
+    x: UnsafeCell<u32>,
+}
+
+#[kani::requires(unsafe{*im.x.get()} < 100)]
+#[kani::modifies(im.x.get())]
+#[kani::ensures(|_| unsafe{*im.x.get()} < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    unsafe { *im.x.get() += 1 }
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected
new file mode 100644
index 000000000000..d9b0f5d51e5c
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get() < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
new file mode 100644
index 000000000000..9f42f6fa1f6c
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of a Cell used as interior mutability in an immutable struct
+use std::cell::Cell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| im.x.get() < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    im.x.set(im.x.get() + 1)
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected
new file mode 100644
index 000000000000..a367bcd9fb95
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get().is_some()"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
new file mode 100644
index 000000000000..6ca32251b60c
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of an OnceCell used as interior mutability in an immutable struct
+use std::cell::OnceCell;
+
+/// This struct contains OnceCell which can be mutated
+struct InteriorMutability {
+    x: OnceCell<u32>,
+}
+
+#[kani::requires(im.x.get().is_none())]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| im.x.get().is_some())]
+fn modify(im: &InteriorMutability) {
+    im.x.set(5).expect("")
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: OnceCell::new() };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected
new file mode 100644
index 000000000000..225c290a171e
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.as_ptr() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
new file mode 100644
index 000000000000..1cce5e2364c3
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct
+use std::cell::RefCell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: RefCell<u32>,
+}
+
+#[kani::requires(unsafe{*im.x.as_ptr()} < 100)]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| unsafe{*im.x.as_ptr()} < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    im.x.replace_with(|&mut old| old + 1);
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: RefCell::new(kani::any()) };
+    modify(&im)
+}
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected
new file mode 100644
index 000000000000..1646a8a78e7f
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected
@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.get() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
new file mode 100644
index 000000000000..6adb7b12c8b1
--- /dev/null
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of an UnsafeCell used as interior mutability in an immutable struct
+use std::cell::UnsafeCell;
+
+/// This struct contains UnsafeCell which can be mutated
+struct InteriorMutability {
+    x: UnsafeCell<u32>,
+}
+
+#[kani::requires(unsafe{*im.x.get()} < 100)]
+#[kani::modifies(im.x.get())]
+#[kani::ensures(|_| unsafe{*im.x.get()} < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    unsafe { *im.x.get() += 1 }
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+    modify(&im)
+}