Add tests for trigonometric intrinsics (rust-lang#1043)

* Add test for `sinf32`

* Add test for `sinf64`

* Add test for `cosf32`

* Add test for `cosf64`

* Minor fix

Author: adpaco-aws

tests/kani/Intrinsics/Math/Trigonometry/cosf32.rs

@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `cosf32` returns the expected results.
+// Note: The CBMC model for this function is an over-approximation that returns:
+//  * A nondet. value between -1 and 1
+//  * 1.0 if the argument is 0.0
+#![feature(core_intrinsics)]
+
+fn fp_equals(value: f32, expected: f32) -> bool {
+    let abs_diff = (value - expected).abs();
+    abs_diff <= f32::EPSILON
+}
+
+#[kani::proof]
+fn cosine_range() {
+    let x: f32 = kani::any();
+    kani::assume(x.is_finite());
+    let cosine = unsafe { std::intrinsics::cosf32(x) };
+    assert!(cosine < 1.0 || fp_equals(cosine, 1.0));
+    assert!(cosine > -1.0 || fp_equals(cosine, -1.0));
+}
+
+#[kani::proof]
+fn cosine_const() {
+    let x = 0.0;
+    let cosine = unsafe { std::intrinsics::cosf32(x) };
+    assert!(fp_equals(cosine, 1.0));
+}

tests/kani/Intrinsics/Math/Trigonometry/cosf64.rs

@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `cosf64` returns the expected results.
+// Note: The CBMC model for this function is an over-approximation that returns:
+//  * A nondet. value between -1 and 1
+//  * 1.0 if the argument is 0.0
+#![feature(core_intrinsics)]
+
+fn fp_equals(value: f64, expected: f64) -> bool {
+    let abs_diff = (value - expected).abs();
+    abs_diff <= f64::EPSILON
+}
+
+#[kani::proof]
+fn cosine_range() {
+    let x: f64 = kani::any();
+    kani::assume(x.is_finite());
+    let cosine = unsafe { std::intrinsics::cosf64(x) };
+    assert!(cosine < 1.0 || fp_equals(cosine, 1.0));
+    assert!(cosine > -1.0 || fp_equals(cosine, -1.0));
+}
+
+#[kani::proof]
+fn cosine_const() {
+    let x = 0.0;
+    let cosine = unsafe { std::intrinsics::cosf64(x) };
+    assert!(fp_equals(cosine, 1.0));
+}

tests/kani/Intrinsics/Math/Trigonometry/sinf32.rs

@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `sinf32` returns the expected results.
+// Note: The CBMC model for this function is an over-approximation that returns:
+//  * A nondet. value between -1 and 1
+//  * 0.0 if the argument is 0.0
+#![feature(core_intrinsics)]
+
+fn fp_equals(value: f32, expected: f32) -> bool {
+    let abs_diff = (value - expected).abs();
+    abs_diff <= f32::EPSILON
+}
+
+#[kani::proof]
+fn sine_range() {
+    let x: f32 = kani::any();
+    kani::assume(x.is_finite());
+    let sine = unsafe { std::intrinsics::sinf32(x) };
+    assert!(sine < 1.0 || fp_equals(sine, 1.0));
+    assert!(sine > -1.0 || fp_equals(sine, -1.0));
+}
+
+#[kani::proof]
+fn sine_const() {
+    let x = 0.0;
+    let sine = unsafe { std::intrinsics::sinf32(x) };
+    assert!(fp_equals(sine, 0.0));
+}

tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs

@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `sinf64` returns the expected results.
+// Note: The CBMC model for this function is an over-approximation that returns:
+//  * A nondet. value between -1 and 1
+//  * 0.0 if the argument is 0.0
+#![feature(core_intrinsics)]
+
+fn fp_equals(value: f64, expected: f64) -> bool {
+    let abs_diff = (value - expected).abs();
+    abs_diff <= f64::EPSILON
+}
+
+#[kani::proof]
+fn sine_range() {
+    let x: f64 = kani::any();
+    kani::assume(x.is_finite());
+    let sine = unsafe { std::intrinsics::sinf64(x) };
+    assert!(sine < 1.0 || fp_equals(sine, 1.0));
+    assert!(sine > -1.0 || fp_equals(sine, -1.0));
+}
+
+#[kani::proof]
+fn sine_const() {
+    let x = 0.0;
+    let sine = unsafe { std::intrinsics::sinf64(x) };
+    assert!(fp_equals(sine, 0.0));
+}