Audit for rintf* and nearbyintf* intrinsics (rust-lang#1277)

* Restore `rintf*` intrinsics

* Remove negative tests

* Restore `nearbyintf*` intrinsics

* Remove negative tests

* Add tests for `rintf*` and `nearbyintf*`

* Require `diff` to be [0, 0.5]

Author: adpaco-aws

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

@@ -549,12 +549,8 @@ impl<'tcx> GotocCtx<'tcx> {
             "minnumf32" => codegen_simple_intrinsic!(Fminf),
             "minnumf64" => codegen_simple_intrinsic!(Fmin),
             "mul_with_overflow" => codegen_op_with_overflow!(mul_overflow),
-            "nearbyintf32" => codegen_unimplemented_intrinsic!(
-                "https://github.com/model-checking/kani/issues/1025"
-            ),
-            "nearbyintf64" => codegen_unimplemented_intrinsic!(
-                "https://github.com/model-checking/kani/issues/1025"
-            ),
+            "nearbyintf32" => codegen_simple_intrinsic!(Nearbyintf),
+            "nearbyintf64" => codegen_simple_intrinsic!(Nearbyint),
             "needs_drop" => codegen_intrinsic_const!(),
             "offset" => self.codegen_offset(intrinsic, instance, fargs, p, loc),
             "powf32" => unstable_codegen!(codegen_simple_intrinsic!(Powf)),
@@ -567,12 +563,8 @@ impl<'tcx> GotocCtx<'tcx> {
             "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc),
             "ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, p, loc),
             "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc),
-            "rintf32" => codegen_unimplemented_intrinsic!(
-                "https://github.com/model-checking/kani/issues/1025"
-            ),
-            "rintf64" => codegen_unimplemented_intrinsic!(
-                "https://github.com/model-checking/kani/issues/1025"
-            ),
+            "rintf32" => codegen_simple_intrinsic!(Rintf),
+            "rintf64" => codegen_simple_intrinsic!(Rint),
             "rotate_left" => codegen_intrinsic_binop!(rol),
             "rotate_right" => codegen_intrinsic_binop!(ror),
             "roundf32" => codegen_simple_intrinsic!(Roundf),

tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs

@@ -0,0 +1,99 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `nearbyintf32` returns the nearest integer to the argument. The
+// default rounding mode is rounding half to even, which is described here:
+// https://en.wikipedia.org/wiki/Rounding#Round_half_to_even
+#![feature(core_intrinsics)]
+use std::intrinsics::nearbyintf32;
+
+#[kani::proof]
+fn test_one() {
+    let one = 1.0;
+    let result = unsafe { nearbyintf32(one) };
+    assert!(result == 1.0);
+}
+
+#[kani::proof]
+fn test_one_frac() {
+    let one_frac = 1.9;
+    let result = unsafe { nearbyintf32(one_frac) };
+    assert!(result == 2.0);
+}
+
+#[kani::proof]
+fn test_half_down() {
+    let one_frac = 2.5;
+    let result = unsafe { nearbyintf32(one_frac) };
+    assert!(result == 2.0);
+}
+
+#[kani::proof]
+fn test_half_up() {
+    let one_frac = 3.5;
+    let result = unsafe { nearbyintf32(one_frac) };
+    assert!(result == 4.0);
+}
+
+#[kani::proof]
+fn test_conc() {
+    let conc = -42.6;
+    let result = unsafe { nearbyintf32(conc) };
+    assert!(result == -43.0);
+}
+
+#[kani::proof]
+fn test_conc_sci() {
+    let conc = 5.4e-2;
+    let result = unsafe { nearbyintf32(conc) };
+    assert!(result == 0.0);
+}
+
+#[kani::proof]
+fn test_towards_nearest() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let result = unsafe { nearbyintf32(x) };
+    let frac = x.fract().abs();
+    if x.is_sign_positive() {
+        if frac > 0.5 {
+            assert!(result > x);
+        } else if frac < 0.5 {
+            assert!(result <= x);
+        } else {
+            // This would fail if conversion checks were on
+            let integer = x as i64;
+            if integer % 2 == 0 {
+                assert!(result < x);
+            } else {
+                assert!(result > x);
+            }
+        }
+    } else {
+        if frac > 0.5 {
+            assert!(result < x);
+        } else if frac < 0.5 {
+            assert!(result >= x);
+        } else {
+            // This would fail if conversion checks were on
+            let integer = x as i64;
+            if integer % 2 == 0 {
+                assert!(result > x);
+            } else {
+                assert!(result < x);
+            }
+        }
+    }
+}
+
+#[kani::proof]
+fn test_diff_half_one() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let result = unsafe { nearbyintf32(x) };
+    let diff = (x - result).abs();
+    assert!(diff <= 0.5);
+    assert!(diff >= 0.0);
+}

tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs

@@ -0,0 +1,99 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `nearbyintf64` returns the nearest integer to the argument. The
+// default rounding mode is rounding half to even, which is described here:
+// https://en.wikipedia.org/wiki/Rounding#Round_half_to_even
+#![feature(core_intrinsics)]
+use std::intrinsics::nearbyintf64;
+
+#[kani::proof]
+fn test_one() {
+    let one = 1.0;
+    let result = unsafe { nearbyintf64(one) };
+    assert!(result == 1.0);
+}
+
+#[kani::proof]
+fn test_one_frac() {
+    let one_frac = 1.9;
+    let result = unsafe { nearbyintf64(one_frac) };
+    assert!(result == 2.0);
+}
+
+#[kani::proof]
+fn test_half_down() {
+    let one_frac = 2.5;
+    let result = unsafe { nearbyintf64(one_frac) };
+    assert!(result == 2.0);
+}
+
+#[kani::proof]
+fn test_half_up() {
+    let one_frac = 3.5;
+    let result = unsafe { nearbyintf64(one_frac) };
+    assert!(result == 4.0);
+}
+
+#[kani::proof]
+fn test_conc() {
+    let conc = -42.6;
+    let result = unsafe { nearbyintf64(conc) };
+    assert!(result == -43.0);
+}
+
+#[kani::proof]
+fn test_conc_sci() {
+    let conc = 5.4e-2;
+    let result = unsafe { nearbyintf64(conc) };
+    assert!(result == 0.0);
+}
+
+#[kani::proof]
+fn test_towards_nearest() {
+    let x: f64 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let result = unsafe { nearbyintf64(x) };
+    let frac = x.fract().abs();
+    if x.is_sign_positive() {
+        if frac > 0.5 {
+            assert!(result > x);
+        } else if frac < 0.5 {
+            assert!(result <= x);
+        } else {
+            // This would fail if conversion checks were on
+            let integer = x as i64;
+            if integer % 2 == 0 {
+                assert!(result < x);
+            } else {
+                assert!(result > x);
+            }
+        }
+    } else {
+        if frac > 0.5 {
+            assert!(result < x);
+        } else if frac < 0.5 {
+            assert!(result >= x);
+        } else {
+            // This would fail if conversion checks were on
+            let integer = x as i64;
+            if integer % 2 == 0 {
+                assert!(result > x);
+            } else {
+                assert!(result < x);
+            }
+        }
+    }
+}
+
+#[kani::proof]
+fn test_diff_half_one() {
+    let x: f64 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let result = unsafe { nearbyintf64(x) };
+    let diff = (x - result).abs();
+    assert!(diff <= 0.5);
+    assert!(diff >= 0.0);
+}

tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs

@@ -0,0 +1,104 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `rintf32` returns the nearest integer to the argument. The
+// default rounding mode is rounding half to even, which is described here:
+// https://en.wikipedia.org/wiki/Rounding#Round_half_to_even
+//
+// `rintf32` works like `nearbyintf32`, but it may raise an inexact
+// floating-point exception which isn't supported in Rust:
+// https://github.com/rust-lang/rust/issues/10186
+// So in practice, `rintf32` and `nearbyintf32` work the same way.
+#![feature(core_intrinsics)]
+use std::intrinsics::rintf32;
+
+#[kani::proof]
+fn test_one() {
+    let one = 1.0;
+    let result = unsafe { rintf32(one) };
+    assert!(result == 1.0);
+}
+
+#[kani::proof]
+fn test_one_frac() {
+    let one_frac = 1.9;
+    let result = unsafe { rintf32(one_frac) };
+    assert!(result == 2.0);
+}
+
+#[kani::proof]
+fn test_half_down() {
+    let one_frac = 2.5;
+    let result = unsafe { rintf32(one_frac) };
+    assert!(result == 2.0);
+}
+
+#[kani::proof]
+fn test_half_up() {
+    let one_frac = 3.5;
+    let result = unsafe { rintf32(one_frac) };
+    assert!(result == 4.0);
+}
+
+#[kani::proof]
+fn test_conc() {
+    let conc = -42.6;
+    let result = unsafe { rintf32(conc) };
+    assert!(result == -43.0);
+}
+
+#[kani::proof]
+fn test_conc_sci() {
+    let conc = 5.4e-2;
+    let result = unsafe { rintf32(conc) };
+    assert!(result == 0.0);
+}
+
+#[kani::proof]
+fn test_towards_nearest() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let result = unsafe { rintf32(x) };
+    let frac = x.fract().abs();
+    if x.is_sign_positive() {
+        if frac > 0.5 {
+            assert!(result > x);
+        } else if frac < 0.5 {
+            assert!(result <= x);
+        } else {
+            // This would fail if conversion checks were on
+            let integer = x as i64;
+            if integer % 2 == 0 {
+                assert!(result < x);
+            } else {
+                assert!(result > x);
+            }
+        }
+    } else {
+        if frac > 0.5 {
+            assert!(result < x);
+        } else if frac < 0.5 {
+            assert!(result >= x);
+        } else {
+            // This would fail if conversion checks were on
+            let integer = x as i64;
+            if integer % 2 == 0 {
+                assert!(result > x);
+            } else {
+                assert!(result < x);
+            }
+        }
+    }
+}
+
+#[kani::proof]
+fn test_diff_half_one() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let result = unsafe { rintf32(x) };
+    let diff = (x - result).abs();
+    assert!(diff <= 0.5);
+    assert!(diff >= 0.0);
+}