Disable remaining rounding intrinsics (rust-lang#1028)

* Disable remaining rounding intrinsics

* Update support table

* Fix format

Author: adpaco-aws

docs/src/rust-feature-support.md

@@ -356,8 +356,8 @@ minnumf32 | Yes | |
 minnumf64 | Yes | |
 move_val_init | No | |
 mul_with_overflow | Yes | |
-nearbyintf32 | Yes | |
-nearbyintf64 | Yes | |
+nearbyintf32 | No | |
+nearbyintf64 | No | |
 needs_drop | Yes | |
 nontemporal_store | No | |
 offset | Partial | Missing undefined behavior checks |
@@ -374,8 +374,8 @@ ptr_guaranteed_eq | Partial | |
 ptr_guaranteed_ne | Partial | |
 ptr_offset_from | Partial | Missing undefined behavior checks |
 raw_eq | Partial | Missing undefined behavior checks |
-rintf32 | Yes | |
-rintf64 | Yes | |
+rintf32 | No | |
+rintf64 | No | |
 rotate_left | Yes | |
 rotate_right | Yes | |
 roundf32 | No | |
@@ -391,8 +391,8 @@ sqrtf32 | Yes | |
 sqrtf64 | Yes | |
 sub_with_overflow | Yes | |
 transmute | Yes | |
-truncf32 | Yes | |
-truncf64 | Yes | |
+truncf32 | No | |
+truncf64 | No | |
 try | No | [#267](https://github.com/model-checking/kani/issues/267) |
 type_id | Yes | |
 type_name | Yes | |

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

@@ -462,8 +462,12 @@ 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_simple_intrinsic!(Nearbyintf),
-            "nearbyintf64" => codegen_simple_intrinsic!(Nearbyint),
+            "nearbyintf32" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
+            "nearbyintf64" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
             "needs_drop" => codegen_intrinsic_const!(),
             "offset" => codegen_op_with_overflow_check!(add_overflow),
             "powf32" => codegen_simple_intrinsic!(Powf),
@@ -475,8 +479,12 @@ impl<'tcx> GotocCtx<'tcx> {
             "ptr_guaranteed_ne" => codegen_intrinsic_boolean_binop!(neq),
             "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc),
             "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc),
-            "rintf32" => codegen_simple_intrinsic!(Rintf),
-            "rintf64" => codegen_simple_intrinsic!(Rint),
+            "rintf32" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
+            "rintf64" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
             "rotate_left" => codegen_intrinsic_binop!(rol),
             "rotate_right" => codegen_intrinsic_binop!(ror),
             "roundf32" => codegen_unimplemented_intrinsic!(
@@ -525,8 +533,12 @@ impl<'tcx> GotocCtx<'tcx> {
             "sqrtf64" => codegen_simple_intrinsic!(Sqrt),
             "sub_with_overflow" => codegen_op_with_overflow!(sub_overflow),
             "transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, p),
-            "truncf32" => codegen_simple_intrinsic!(Truncf),
-            "truncf64" => codegen_simple_intrinsic!(Trunc),
+            "truncf32" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
+            "truncf64" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
             "try" => {
                 codegen_unimplemented_intrinsic!(
                     "https://github.com/model-checking/kani/issues/267"

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

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `nearbyintf32` is not supported until
+// https://github.com/model-checking/kani/issues/1025 is fixed
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = kani::any();
+    let n = unsafe { std::intrinsics::nearbyintf32(x) };
+}

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

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `nearbyintf64` is not supported until
+// https://github.com/model-checking/kani/issues/1025 is fixed
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = kani::any();
+    let n = unsafe { std::intrinsics::nearbyintf64(x) };
+}

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

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `rintf32` is not supported until
+// https://github.com/model-checking/kani/issues/1025 is fixed
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = kani::any();
+    let n = unsafe { std::intrinsics::rintf32(x) };
+}

tests/kani/Intrinsics/Math/Rounding/rintf64.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `rintf64` is not supported until
+// https://github.com/model-checking/kani/issues/1025 is fixed
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = kani::any();
+    let n = unsafe { std::intrinsics::rintf64(x) };
+}

tests/kani/Intrinsics/Math/Rounding/truncf32.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `truncf32` is not supported until
+// https://github.com/model-checking/kani/issues/1025 is fixed
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = kani::any();
+    let x_trunc = unsafe { std::intrinsics::truncf32(x) };
+}

tests/kani/Intrinsics/Math/Rounding/truncf64.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `truncf64` is not supported until
+// https://github.com/model-checking/kani/issues/1025 is fixed
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = kani::any();
+    let x_trunc = unsafe { std::intrinsics::truncf64(x) };
+}