From 271037b2a0cd31f64b036b13d1795508c25ee5df Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 11 Apr 2022 21:14:44 +0000
Subject: [PATCH] Tests for "absolute" intrinsics

---
 tests/kani/Intrinsics/Math/fabsf32.rs | 26 ++++++++++++++++++++++++++
 tests/kani/Intrinsics/Math/fabsf64.rs | 26 ++++++++++++++++++++++++++
 2 files changed, 52 insertions(+)
 create mode 100644 tests/kani/Intrinsics/Math/fabsf32.rs
 create mode 100644 tests/kani/Intrinsics/Math/fabsf64.rs

diff --git a/tests/kani/Intrinsics/Math/fabsf32.rs b/tests/kani/Intrinsics/Math/fabsf32.rs
new file mode 100644
index 000000000000..bd8b95ac7c6b
--- /dev/null
+++ b/tests/kani/Intrinsics/Math/fabsf32.rs
@@ -0,0 +1,26 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `fabsf32` returns the expected results: absolute value if argument
+// is not NaN, otherwise NaN
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn test_abs_finite() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    let abs_x = unsafe { std::intrinsics::fabsf32(x) };
+    if x < 0.0 {
+        assert!(-x == abs_x);
+    } else {
+        assert!(x == abs_x);
+    }
+}
+
+#[kani::proof]
+fn test_abs_nan() {
+    let x: f32 = kani::any();
+    kani::assume(x.is_nan());
+    let abs_x = unsafe { std::intrinsics::fabsf32(x) };
+    assert!(abs_x.is_nan());
+}
diff --git a/tests/kani/Intrinsics/Math/fabsf64.rs b/tests/kani/Intrinsics/Math/fabsf64.rs
new file mode 100644
index 000000000000..e561ef9b5448
--- /dev/null
+++ b/tests/kani/Intrinsics/Math/fabsf64.rs
@@ -0,0 +1,26 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `fabsf64` returns the expected results: absolute value if argument
+// is not NaN, otherwise NaN
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn test_abs_finite() {
+    let x: f64 = kani::any();
+    kani::assume(!x.is_nan());
+    let abs_x = unsafe { std::intrinsics::fabsf64(x) };
+    if x < 0.0 {
+        assert!(-x == abs_x);
+    } else {
+        assert!(x == abs_x);
+    }
+}
+
+#[kani::proof]
+fn test_abs_nan() {
+    let x: f64 = kani::any();
+    kani::assume(x.is_nan());
+    let abs_x = unsafe { std::intrinsics::fabsf64(x) };
+    assert!(abs_x.is_nan());
+}