From d4a8fc092f8443da6623df9e84878d3ffdc67437 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Mon, 30 Dec 2024 15:44:36 -0500
Subject: [PATCH] tests

---
 .../assert-postconditions.expected            |  9 +++
 .../as-assertions/assert-postconditions.rs    | 32 ++++++++++
 .../assert-preconditions.expected             | 21 ++++++
 .../as-assertions/assert-preconditions.rs     | 64 +++++++++++++++++++
 .../as-assertions/precedence.expected         | 13 ++++
 .../as-assertions/precedence.rs               | 48 ++++++++++++++
 6 files changed, 187 insertions(+)
 create mode 100644 tests/expected/function-contract/as-assertions/assert-postconditions.expected
 create mode 100644 tests/expected/function-contract/as-assertions/assert-postconditions.rs
 create mode 100644 tests/expected/function-contract/as-assertions/assert-preconditions.expected
 create mode 100644 tests/expected/function-contract/as-assertions/assert-preconditions.rs
 create mode 100644 tests/expected/function-contract/as-assertions/precedence.expected
 create mode 100644 tests/expected/function-contract/as-assertions/precedence.rs

diff --git a/tests/expected/function-contract/as-assertions/assert-postconditions.expected b/tests/expected/function-contract/as-assertions/assert-postconditions.expected
new file mode 100644
index 000000000000..08b8171aa4e1
--- /dev/null
+++ b/tests/expected/function-contract/as-assertions/assert-postconditions.expected
@@ -0,0 +1,9 @@
+assertion\
+	 - Status: FAILURE\
+	 - Description: "|result| old(*add_two_ptr + 1) == *add_two_ptr"
+
+assertion\
+	 - Status: SUCCESS\
+	 - Description: "|result| old(*add_one_ptr + 1) == *add_one_ptr"
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/as-assertions/assert-postconditions.rs b/tests/expected/function-contract/as-assertions/assert-postconditions.rs
new file mode 100644
index 000000000000..fb6a0dbcc849
--- /dev/null
+++ b/tests/expected/function-contract/as-assertions/assert-postconditions.rs
@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions
+
+// Test -Zcontracts-as-assertions for postconditions.
+
+#[kani::requires(*add_three_ptr < 100)]
+#[kani::modifies(add_three_ptr)]
+fn add_three(add_three_ptr: &mut u32) {
+    *add_three_ptr += 1;
+    add_two(add_three_ptr);
+}
+
+#[kani::ensures(|result| old(*add_two_ptr + 1) == *add_two_ptr)] // incorrect -- should be old(*add_two_ptr + 1)
+fn add_two(add_two_ptr: &mut u32) {
+    *add_two_ptr += 1;
+    add_one(add_two_ptr)
+}
+
+#[kani::requires(*add_one_ptr < 102)]
+#[kani::modifies(add_one_ptr)]
+#[kani::ensures(|result| old(*add_one_ptr + 1) == *add_one_ptr)] // correct -- assertion should always succeed
+fn add_one(add_one_ptr: &mut u32) {
+    *add_one_ptr += 1;
+}
+
+// -Zcontracts-as-assertions introduces this failure; without it, add_two's and add_one's contracts are ignored.
+#[kani::proof_for_contract(add_three)]
+fn prove_add_three() {
+    let mut i = kani::any();
+    add_three(&mut i);
+}
diff --git a/tests/expected/function-contract/as-assertions/assert-preconditions.expected b/tests/expected/function-contract/as-assertions/assert-preconditions.expected
new file mode 100644
index 000000000000..3d496f83c925
--- /dev/null
+++ b/tests/expected/function-contract/as-assertions/assert-preconditions.expected
@@ -0,0 +1,21 @@
+assertion\
+	 - Status: SUCCESS\
+	 - Description: "*ptr < 100"\
+
+assertion\
+	 - Status: FAILURE\
+	 - Description: "*ptr == 1"
+
+assertion\
+	 - Status: FAILURE\
+	 - Description: "*ptr < 100"
+
+assertion\
+	 - Status: FAILURE\
+	 - Description: "*ptr == 1"
+
+Summary:
+Verification failed for - should_fail::prove_add_three_contract
+Verification failed for - should_fail::prove_add_one
+Verification failed for - should_fail::prove_add_three
+Complete - 1 successfully verified harnesses, 3 failures, 4 total.
diff --git a/tests/expected/function-contract/as-assertions/assert-preconditions.rs b/tests/expected/function-contract/as-assertions/assert-preconditions.rs
new file mode 100644
index 000000000000..6bd0f47c6be8
--- /dev/null
+++ b/tests/expected/function-contract/as-assertions/assert-preconditions.rs
@@ -0,0 +1,64 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions
+
+// Test -Zcontracts-as-assertions for preconditions.
+
+#[kani::requires(*ptr < 100)]
+#[kani::ensures(|result| old(*ptr + 3) == *ptr)]
+#[kani::modifies(ptr)]
+fn add_three(ptr: &mut u32) {
+    *ptr += 1;
+    add_two(ptr);
+}
+
+#[kani::requires(*ptr < 101)]
+#[kani::ensures(|result| old(*ptr + 2) == *ptr)]
+fn add_two(ptr: &mut u32) {
+    *ptr += 1;
+    add_one(ptr);
+}
+
+#[kani::requires(*ptr == 1)]
+#[kani::modifies(ptr)]
+fn add_one(ptr: &mut u32) {
+    *ptr += 1;
+}
+
+mod should_fail {
+    use crate::*;
+
+    // add_three and add_one's preconditions are asserted, causing failure.
+    #[kani::proof]
+    fn prove_add_three() {
+        let mut i = kani::any();
+        add_three(&mut i);
+    }
+
+    // add_three's precondition is asserted, causing failure.
+    #[kani::proof_for_contract(add_one)]
+    fn prove_add_one() {
+        let mut i = kani::any();
+        add_three(&mut i);
+    }
+
+    // Since add_three is the target of the proof_for_contract, its precondition gets assumed.
+    // However, add_one's precondition is still asserted, causing failure.
+    #[kani::proof_for_contract(add_three)]
+    fn prove_add_three_contract() {
+        let mut i = kani::any();
+        add_three(&mut i);
+    }
+}
+
+mod should_pass {
+    use crate::*;
+    // Same as should_fail::prove_add_one, with the added assumption of add_three's precondition.
+    // Note that add_one's precondition gets assumed since it's the target of the proof_for_contract.
+    #[kani::proof_for_contract(add_one)]
+    fn prove_add_one() {
+        let mut i = kani::any();
+        kani::assume(i < 100);
+        add_three(&mut i);
+    }
+}
diff --git a/tests/expected/function-contract/as-assertions/precedence.expected b/tests/expected/function-contract/as-assertions/precedence.expected
new file mode 100644
index 000000000000..16fcc8fa1c75
--- /dev/null
+++ b/tests/expected/function-contract/as-assertions/precedence.expected
@@ -0,0 +1,13 @@
+assertion\
+	 - Status: UNREACHABLE\
+	 - Description: "*add_one_ptr == 1"
+
+assertion\
+	 - Status: UNREACHABLE\
+	 - Description: "|result| old(*add_one_ptr + 1) == *add_one_ptr"
+
+assertion\
+	 - Status: UNREACHABLE\
+	 - Description: "|result| old(*add_one_ptr + 1) == *add_one_ptr"
+
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/expected/function-contract/as-assertions/precedence.rs b/tests/expected/function-contract/as-assertions/precedence.rs
new file mode 100644
index 000000000000..06af70eaa372
--- /dev/null
+++ b/tests/expected/function-contract/as-assertions/precedence.rs
@@ -0,0 +1,48 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions
+
+// If a function is the target of a proof_for_contract or stub_verified, we should defer to the contract handling for those modes.
+// i.e., test that -Zcontracts-as-assertions does not override the contract handling for proof_for_contract and stub_verified.
+
+#[kani::modifies(add_three_ptr)]
+#[kani::requires(*add_three_ptr < 100)]
+fn add_three(add_three_ptr: &mut u32) {
+    *add_three_ptr += 1;
+    add_two(add_three_ptr);
+}
+
+#[kani::requires(*add_two_ptr < 101)]
+#[kani::ensures(|result| old(*add_two_ptr + 2) == *add_two_ptr)]
+fn add_two(add_two_ptr: &mut u32) {
+    *add_two_ptr += 1;
+    add_one(add_two_ptr);
+}
+
+#[kani::modifies(add_one_ptr)]
+#[kani::requires(*add_one_ptr == 1)]
+#[kani::ensures(|result| old(*add_one_ptr + 1) == *add_one_ptr)]
+fn add_one(add_one_ptr: &mut u32) {
+    *add_one_ptr += 1;
+}
+
+// Test that proof_for_contract takes precedence over the assert mode, i.e.
+// that the target of the proof for contract still has its preconditions assumed.
+#[kani::proof_for_contract(add_one)]
+fn proof_for_contract_takes_precedence() {
+    let mut i = kani::any();
+    // if add_one's precondition was asserted, verification would fail,
+    // but since it's assumed, we get a vacuously successful proof instead.
+    kani::assume(i == 2);
+    add_one(&mut i);
+}
+
+// Test that stub_verified takes precedence over the assert mode.
+// Verification should succeed because we stub add_two by its contract,
+// meaning we never reach add_one's contract.
+#[kani::proof_for_contract(add_three)]
+#[kani::stub_verified(add_two)]
+fn stub_verified_takes_precedence() {
+    let mut i = kani::any();
+    add_three(&mut i);
+}