From ce022e216aed69d1b71c9a017784a1ed14c510ee Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 8 Mar 2024 12:37:26 -0800
Subject: [PATCH] Add a expected test using the new method in a contract

---
 .../function-contract/valid_ptr.expected      | 11 ++++
 tests/expected/function-contract/valid_ptr.rs | 61 +++++++++++++++++++
 2 files changed, 72 insertions(+)
 create mode 100644 tests/expected/function-contract/valid_ptr.expected
 create mode 100644 tests/expected/function-contract/valid_ptr.rs

diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected
new file mode 100644
index 000000000000..a9dc8dd5992d
--- /dev/null
+++ b/tests/expected/function-contract/valid_ptr.expected
@@ -0,0 +1,11 @@
+Checking harness pre_condition::harness_invalid_ptr...
+Failed Checks: Dangling pointer is only valid for zero-sized access
+
+Checking harness pre_condition::harness_stack_ptr...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness pre_condition::harness_head_ptr...
+VERIFICATION:- SUCCESSFUL
+
+Verification failed for - pre_condition::harness_invalid_ptr
+Complete - 2 successfully verified harnesses, 1 failures, 3 total
diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs
new file mode 100644
index 000000000000..da212c7fa63e
--- /dev/null
+++ b/tests/expected/function-contract/valid_ptr.rs
@@ -0,0 +1,61 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts -Zmem-predicates
+
+//! Test that it is sound to use `assert_valid_ptr` inside a contract pre-condition.
+//! We cannot validate post-condition yet. This can be done once we fix:
+//! <https://github.com/model-checking/kani/issues/2997>
+#![feature(pointer_is_aligned)]
+
+mod pre_condition {
+    /// This contract should succeed only if the input is a valid pointer.
+    #[kani::requires(kani::mem::assert_valid_ptr(ptr) && ptr.is_aligned())]
+    unsafe fn read_ptr(ptr: *const i32) -> i32 {
+        *ptr
+    }
+
+    #[kani::proof_for_contract(read_ptr)]
+    fn harness_head_ptr() {
+        let boxed = Box::new(10);
+        let raw_ptr = Box::into_raw(boxed);
+        assert_eq!(unsafe { read_ptr(raw_ptr) }, 10);
+        let _ = unsafe { Box::from_raw(raw_ptr) };
+    }
+
+    #[kani::proof_for_contract(read_ptr)]
+    fn harness_stack_ptr() {
+        let val = -20;
+        assert_eq!(unsafe { read_ptr(&val) }, -20);
+    }
+
+    #[kani::proof_for_contract(read_ptr)]
+    fn harness_invalid_ptr() {
+        let ptr = std::ptr::NonNull::<i32>::dangling().as_ptr();
+        assert_eq!(unsafe { read_ptr(ptr) }, -20);
+    }
+}
+
+/// TODO: Enable once we fix: <https://github.com/model-checking/kani/issues/2997>
+#[cfg(not_supported)]
+mod post_condition {
+
+    /// This contract should fail since we are creating a dangling pointer.
+    #[kani::ensures(kani::mem::assert_valid_ptr(result.0))]
+    unsafe fn new_invalid_ptr() -> PtrWrapper<char> {
+        let var = 'c';
+        PtrWrapper(&var as *const _)
+    }
+
+    #[kani::proof_for_contract(new_invalid_ptr)]
+    fn harness() {
+        let _ = unsafe { new_invalid_ptr() };
+    }
+
+    struct PtrWrapper<T>(*const T);
+
+    impl<T> kani::Arbitrary for PtrWrapper<T> {
+        fn any() -> Self {
+            unreachable!("Do not invoke stubbing")
+        }
+    }
+}