From e0fb6197f1aca29ff890f05ad6df824e0dd5424d Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 21 Mar 2022 13:28:43 +0000
Subject: [PATCH] More tests for `exact_div`

---
 tests/kani/ExactDiv/main.rs                       | 11 -----------
 tests/kani/Intrinsics/ExactDiv/divisor_is_zero.rs | 14 ++++++++++++++
 tests/kani/Intrinsics/ExactDiv/main.rs            | 15 +++++++++++++++
 .../Intrinsics/ExactDiv/not_exact_division.rs     | 14 ++++++++++++++
 .../kani/Intrinsics/ExactDiv/overflow_division.rs | 14 ++++++++++++++
 5 files changed, 57 insertions(+), 11 deletions(-)
 delete mode 100644 tests/kani/ExactDiv/main.rs
 create mode 100644 tests/kani/Intrinsics/ExactDiv/divisor_is_zero.rs
 create mode 100644 tests/kani/Intrinsics/ExactDiv/main.rs
 create mode 100644 tests/kani/Intrinsics/ExactDiv/not_exact_division.rs
 create mode 100644 tests/kani/Intrinsics/ExactDiv/overflow_division.rs

diff --git a/tests/kani/ExactDiv/main.rs b/tests/kani/ExactDiv/main.rs
deleted file mode 100644
index b22636525620..000000000000
--- a/tests/kani/ExactDiv/main.rs
+++ /dev/null
@@ -1,11 +0,0 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-#![feature(core_intrinsics)]
-
-#[kani::proof]
-fn main() {
-    let a: u8 = 8;
-    let b: u8 = 4;
-    let i = unsafe { std::intrinsics::exact_div(a, b) };
-    assert!(i == 2);
-}
diff --git a/tests/kani/Intrinsics/ExactDiv/divisor_is_zero.rs b/tests/kani/Intrinsics/ExactDiv/divisor_is_zero.rs
new file mode 100644
index 000000000000..821d0c85da41
--- /dev/null
+++ b/tests/kani/Intrinsics/ExactDiv/divisor_is_zero.rs
@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `exact_div` results in undefined behavior if `y == 0`
+// https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = kani::any();
+    let y = 0;
+    let _ = unsafe { std::intrinsics::exact_div(x, y) };
+}
diff --git a/tests/kani/Intrinsics/ExactDiv/main.rs b/tests/kani/Intrinsics/ExactDiv/main.rs
new file mode 100644
index 000000000000..a079aba22ad9
--- /dev/null
+++ b/tests/kani/Intrinsics/ExactDiv/main.rs
@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `exact_div` returns the expected result if none
+// of the conditions for undefined behavior are met
+// https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = 8;
+    let y = 4;
+    let res = unsafe { std::intrinsics::exact_div(x, y) };
+    assert!(res == 2);
+}
diff --git a/tests/kani/Intrinsics/ExactDiv/not_exact_division.rs b/tests/kani/Intrinsics/ExactDiv/not_exact_division.rs
new file mode 100644
index 000000000000..376186769a59
--- /dev/null
+++ b/tests/kani/Intrinsics/ExactDiv/not_exact_division.rs
@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `exact_div` results in undefined behavior if `x % y != 0`
+// https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = 9;
+    let y = 4;
+    let _ = unsafe { std::intrinsics::exact_div(x, y) };
+}
diff --git a/tests/kani/Intrinsics/ExactDiv/overflow_division.rs b/tests/kani/Intrinsics/ExactDiv/overflow_division.rs
new file mode 100644
index 000000000000..c87edd5d6a48
--- /dev/null
+++ b/tests/kani/Intrinsics/ExactDiv/overflow_division.rs
@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `exact_div` results in undefined behavior if `x == T::MIN && y == -1`
+// https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = i32::MIN;
+    let y = -1;
+    let _ = unsafe { std::intrinsics::exact_div(x, y) };
+}