Function Contracts: Interior Mutability Tests

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

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)
+}

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

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);
+}

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

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)
+}

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

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)
+}

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

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)
+}

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

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)
+}

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

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)
+}