Function Contracts: Interior Mutability Tests

tests/expected/function-contract/interior-mutability/cell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| *unsafe{ x.x.hack() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/cell.rs

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+use std::cell::{Cell, OnceCell, UnsafeCell};
+use std::mem::transmute;
+
+trait ToHack<T: ?Sized> {
+ unsafe fn hack(&self) -> &T;
+}
+
+impl<T: ?Sized> ToHack<T> for UnsafeCell<T> {
+ unsafe fn hack(&self) -> &T {
+ transmute(self)
+ }
+}
+
+impl<T: ?Sized> ToHack<T> for Cell<T> {
+ unsafe fn hack(&self) -> &T {
+ transmute(self)
+ }
+}
+
+impl<T> ToHack<Option<T>> for OnceCell<T> {
+ unsafe fn hack(&self) -> &Option<T> {
+ transmute(self)
+ }
+}
+
+// ---------------------------------------------------
+
+struct InteriorMutability {
+ x: Cell<u32>,
+}
+
+#[kani::requires(*unsafe{x.x.hack()} < 100)]
+#[kani::modifies(x.x.hack())]
+#[kani::ensures(|_| *unsafe{x.x.hack()} < 101)]
+fn modify(x: &InteriorMutability) {
+ x.x.set(x.x.get() + 1)
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+ let x: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+ modify(&x)
+}

tests/expected/function-contract/interior-mutability/oncecell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ x.x.hack() }.is_some()"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/oncecell.rs

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+use std::cell::{Cell, OnceCell, UnsafeCell};
+use std::mem::transmute;
+
+trait ToHack<T: ?Sized> {
+ unsafe fn hack(&self) -> &T;
+}
+
+impl<T: ?Sized> ToHack<T> for UnsafeCell<T> {
+ unsafe fn hack(&self) -> &T {
+ transmute(self)
+ }
+}
+
+impl<T: ?Sized> ToHack<T> for Cell<T> {
+ unsafe fn hack(&self) -> &T {
+ transmute(self)
+ }
+}
+
+impl<T> ToHack<Option<T>> for OnceCell<T> {
+ unsafe fn hack(&self) -> &Option<T> {
+ transmute(self)
+ }
+}
+
+// ---------------------------------------------------
+
+struct InteriorMutability {
+ x: OnceCell<u32>,
+}
+
+#[kani::requires(unsafe{x.x.hack()}.is_none())]
+#[kani::modifies(x.x.hack())]
+#[kani::ensures(|_| unsafe{x.x.hack()}.is_some())]
+fn modify(x: &InteriorMutability) {
+ x.x.set(5).expect("")
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+ let x: InteriorMutability = InteriorMutability { x: OnceCell::new() };
+ modify(&x)
+}

tests/expected/function-contract/interior-mutability/unsafecell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| *unsafe{ x.x.hack() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/unsafecell.rs

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+use std::cell::{Cell, OnceCell, UnsafeCell};
+use std::mem::transmute;
+
+trait ToHack<T: ?Sized> {
+ unsafe fn hack(&self) -> &T;
+}
+
+impl<T: ?Sized> ToHack<T> for UnsafeCell<T> {
+ unsafe fn hack(&self) -> &T {
+ transmute(self)
+ }
+}
+
+impl<T: ?Sized> ToHack<T> for Cell<T> {
+ unsafe fn hack(&self) -> &T {
+ transmute(self)
+ }
+}
+
+impl<T> ToHack<Option<T>> for OnceCell<T> {
+ unsafe fn hack(&self) -> &Option<T> {
+ transmute(self)
+ }
+}
+
+// ---------------------------------------------------
+
+struct InteriorMutability {
+ x: UnsafeCell<u32>,
+}
+
+#[kani::requires(*unsafe{x.x.hack()} < 100)]
+#[kani::modifies(x.x.hack())]
+#[kani::ensures(|_| *unsafe{x.x.hack()} < 101)]
+fn modify(x: &InteriorMutability) {
+ unsafe { *x.x.get() += 1 }
+}
+
+#[kani::proof_for_contract(modify)]
+fn main() {
+ let x: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+ modify(&x)
+}