Audit for roundf* (rust-lang#1266)

* Restore `roundf*` intrinsics

* Remove negative tests

* Add tests for `roundf*`

Author: adpaco-aws

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -573,12 +573,8 @@ impl<'tcx> GotocCtx<'tcx> {
             ),
             "rotate_left" => codegen_intrinsic_binop!(rol),
             "rotate_right" => codegen_intrinsic_binop!(ror),
-            "roundf32" => codegen_unimplemented_intrinsic!(
-                "https://github.com/model-checking/kani/issues/1025"
-            ),
-            "roundf64" => codegen_unimplemented_intrinsic!(
-                "https://github.com/model-checking/kani/issues/1025"
-            ),
+            "roundf32" => codegen_simple_intrinsic!(Roundf),
+            "roundf64" => codegen_simple_intrinsic!(Round),
             "saturating_add" => codegen_intrinsic_binop_with_mm!(saturating_add),
             "saturating_sub" => codegen_intrinsic_binop_with_mm!(saturating_sub),
             "sinf32" => codegen_simple_intrinsic!(Sinf),

tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs

@@ -0,0 +1,72 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `roundf32` does return:
+//  * The nearest integer to the argument for some concrete cases.
+//  * A value that is closer to one of the limits (zero, infinity or negative
+//    infinity, based on the fractional part of the argument) in all cases.
+//  * A value such that the difference between it and the argument is between
+//    zero and 0.5.
+#![feature(core_intrinsics)]
+use std::intrinsics::roundf32;
+
+#[kani::proof]
+fn test_one() {
+    let one = 1.0;
+    let result = unsafe { roundf32(one) };
+    assert!(result == 1.0);
+}
+
+#[kani::proof]
+fn test_one_frac() {
+    let one_frac = 1.9;
+    let result = unsafe { roundf32(one_frac) };
+    assert!(result == 2.0);
+}
+
+#[kani::proof]
+fn test_conc() {
+    let conc = -42.6;
+    let result = unsafe { roundf32(conc) };
+    assert!(result == -43.0);
+}
+
+#[kani::proof]
+fn test_conc_sci() {
+    let conc = 5.4e-2;
+    let result = unsafe { roundf32(conc) };
+    assert!(result == 0.0);
+}
+
+#[kani::proof]
+fn test_towards_closer() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let result = unsafe { roundf32(x) };
+    let frac = x.fract().abs();
+    if x.is_sign_positive() {
+        if frac >= 0.5 {
+            assert!(result > x);
+        } else {
+            assert!(result <= x);
+        }
+    } else {
+        if frac >= 0.5 {
+            assert!(result < x);
+        } else {
+            assert!(result >= x);
+        }
+    }
+}
+
+#[kani::proof]
+fn test_diff_one() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let result = unsafe { roundf32(x) };
+    let diff = (x - result).abs();
+    assert!(diff <= 0.5);
+    assert!(diff >= 0.0);
+}

tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs

@@ -0,0 +1,72 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `roundf64` does return:
+//  * The nearest integer to the argument for some concrete cases.
+//  * A value that is closer to one of the limits (zero, infinity or negative
+//    infinity, based on the fractional part of the argument) in all cases.
+//  * A value such that the difference between it and the argument is between
+//    zero and 0.5.
+#![feature(core_intrinsics)]
+use std::intrinsics::roundf64;
+
+#[kani::proof]
+fn test_one() {
+    let one = 1.0;
+    let result = unsafe { roundf64(one) };
+    assert!(result == 1.0);
+}
+
+#[kani::proof]
+fn test_one_frac() {
+    let one_frac = 1.9;
+    let result = unsafe { roundf64(one_frac) };
+    assert!(result == 2.0);
+}
+
+#[kani::proof]
+fn test_conc() {
+    let conc = -42.6;
+    let result = unsafe { roundf64(conc) };
+    assert!(result == -43.0);
+}
+
+#[kani::proof]
+fn test_conc_sci() {
+    let conc = 5.4e-2;
+    let result = unsafe { roundf64(conc) };
+    assert!(result == 0.0);
+}
+
+#[kani::proof]
+fn test_towards_closer() {
+    let x: f64 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let result = unsafe { roundf64(x) };
+    let frac = x.fract().abs();
+    if x.is_sign_positive() {
+        if frac >= 0.5 {
+            assert!(result > x);
+        } else {
+            assert!(result <= x);
+        }
+    } else {
+        if frac >= 0.5 {
+            assert!(result < x);
+        } else {
+            assert!(result >= x);
+        }
+    }
+}
+
+#[kani::proof]
+fn test_diff_one() {
+    let x: f64 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let result = unsafe { roundf64(x) };
+    let diff = (x - result).abs();
+    assert!(diff <= 0.5);
+    assert!(diff >= 0.0);
+}