Disable rounding intrinsics (#1026)

* Disable rounding intrinsics

* Use `codegen_unimplemented_intrinsic`

docs/src/rust-feature-support.md

@@ -309,8 +309,8 @@ bitreverse | Yes | |
 breakpoint | Yes | |
 bswap | Yes | |
 caller_location | No | |
-ceilf32 | Yes | |
-ceilf64 | Yes | |
+ceilf32 | No | |
+ceilf64 | No | |
 copy_nonoverlapping | Yes | |
 copysignf32 | Yes | |
 copysignf64 | Yes | |
@@ -333,8 +333,8 @@ fabsf64 | Yes | |
 fadd_fast | Yes | |
 fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
 float_to_int_unchecked | No | |
-floorf32 | Yes | |
-floorf64 | Yes | |
+floorf32 | No | |
+floorf64 | No | |
 fmaf32 | Yes | |
 fmaf64 | Yes | |
 fmul_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
@@ -378,8 +378,8 @@ rintf32 | Yes | |
 rintf64 | Yes | |
 rotate_left | Yes | |
 rotate_right | Yes | |
-roundf32 | Yes | |
-roundf64 | Yes | |
+roundf32 | No | |
+roundf64 | No | |
 rustc_peek | No | |
 saturating_add | Yes | |
 saturating_sub | Yes | |

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

@@ -390,8 +390,12 @@ impl<'tcx> GotocCtx<'tcx> {
                     "https://github.com/model-checking/kani/issues/374"
                 )
             }
-            "ceilf32" => codegen_simple_intrinsic!(Ceilf),
-            "ceilf64" => codegen_simple_intrinsic!(Ceil),
+            "ceilf32" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
+            "ceilf64" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
             "copy" => codegen_intrinsic_copy!(Memmove),
             "copy_nonoverlapping" => codegen_intrinsic_copy!(Memcpy),
             "copysignf32" => codegen_simple_intrinsic!(Copysignf),
@@ -425,8 +429,12 @@ impl<'tcx> GotocCtx<'tcx> {
                 let binop_stmt = codegen_intrinsic_binop!(div);
                 self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
             }
-            "floorf32" => codegen_simple_intrinsic!(Floorf),
-            "floorf64" => codegen_simple_intrinsic!(Floor),
+            "floorf32" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
+            "floorf64" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
             "fmaf32" => codegen_simple_intrinsic!(Fmaf),
             "fmaf64" => codegen_simple_intrinsic!(Fma),
             "fmul_fast" => {
@@ -471,8 +479,12 @@ impl<'tcx> GotocCtx<'tcx> {
             "rintf64" => codegen_simple_intrinsic!(Rint),
             "rotate_left" => codegen_intrinsic_binop!(rol),
             "rotate_right" => codegen_intrinsic_binop!(ror),
-            "roundf32" => codegen_simple_intrinsic!(Roundf),
-            "roundf64" => codegen_simple_intrinsic!(Round),
+            "roundf32" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
+            "roundf64" => codegen_unimplemented_intrinsic!(
+                "https://github.com/model-checking/kani/issues/1025"
+            ),
             "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/ceilf32.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 `ceilf32` 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_ceil = unsafe { std::intrinsics::ceilf32(x) };
+}

tests/kani/Intrinsics/Math/Rounding/ceilf64.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 `ceilf64` 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_ceil = unsafe { std::intrinsics::ceilf64(x) };
+}

tests/kani/Intrinsics/Math/Rounding/floorf32.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 `floorf32` 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_floor = unsafe { std::intrinsics::floorf32(x) };
+}

tests/kani/Intrinsics/Math/Rounding/floorf64.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 `floorf64` 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_floor = unsafe { std::intrinsics::floorf64(x) };
+}

tests/kani/Intrinsics/Math/Rounding/roundf32.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 `roundf32` 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_round = unsafe { std::intrinsics::roundf32(x) };
+}

tests/kani/Intrinsics/Math/Rounding/roundf64.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 `roundf64` 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_round = unsafe { std::intrinsics::roundf64(x) };
+}