From 90cdad69b9511c3484c82765264704f03aa4f5ec Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 8 Apr 2022 20:44:48 +0000 Subject: [PATCH 1/3] Disable remaining rounding intrinsics --- .../codegen/intrinsic.rs | 24 ++++++++++++++----- .../Intrinsics/Math/Rounding/nearbyintf32.rs | 13 ++++++++++ .../Intrinsics/Math/Rounding/nearbyintf64.rs | 13 ++++++++++ .../kani/Intrinsics/Math/Rounding/rintf32.rs | 13 ++++++++++ .../kani/Intrinsics/Math/Rounding/rintf64.rs | 13 ++++++++++ .../kani/Intrinsics/Math/Rounding/truncf32.rs | 13 ++++++++++ .../kani/Intrinsics/Math/Rounding/truncf64.rs | 13 ++++++++++ 7 files changed, 96 insertions(+), 6 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Rounding/nearbyintf32.rs create mode 100644 tests/kani/Intrinsics/Math/Rounding/nearbyintf64.rs create mode 100644 tests/kani/Intrinsics/Math/Rounding/rintf32.rs create mode 100644 tests/kani/Intrinsics/Math/Rounding/rintf64.rs create mode 100644 tests/kani/Intrinsics/Math/Rounding/truncf32.rs create mode 100644 tests/kani/Intrinsics/Math/Rounding/truncf64.rs diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index f241951c28bb..88762633c383 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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" diff --git a/tests/kani/Intrinsics/Math/Rounding/nearbyintf32.rs b/tests/kani/Intrinsics/Math/Rounding/nearbyintf32.rs new file mode 100644 index 000000000000..f2f3fdc7a0e3 --- /dev/null +++ b/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) }; +} diff --git a/tests/kani/Intrinsics/Math/Rounding/nearbyintf64.rs b/tests/kani/Intrinsics/Math/Rounding/nearbyintf64.rs new file mode 100644 index 000000000000..4b1eb6585b0c --- /dev/null +++ b/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) }; +} diff --git a/tests/kani/Intrinsics/Math/Rounding/rintf32.rs b/tests/kani/Intrinsics/Math/Rounding/rintf32.rs new file mode 100644 index 000000000000..a2e21f85002b --- /dev/null +++ b/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) }; +} diff --git a/tests/kani/Intrinsics/Math/Rounding/rintf64.rs b/tests/kani/Intrinsics/Math/Rounding/rintf64.rs new file mode 100644 index 000000000000..aa46768060c4 --- /dev/null +++ b/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) }; +} diff --git a/tests/kani/Intrinsics/Math/Rounding/truncf32.rs b/tests/kani/Intrinsics/Math/Rounding/truncf32.rs new file mode 100644 index 000000000000..29ae436acd99 --- /dev/null +++ b/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) }; +} diff --git a/tests/kani/Intrinsics/Math/Rounding/truncf64.rs b/tests/kani/Intrinsics/Math/Rounding/truncf64.rs new file mode 100644 index 000000000000..0e22d3d855e6 --- /dev/null +++ b/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) }; +} From fc917da5d0e5fc6bd17cd8f8b38558ce74b85efc Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 8 Apr 2022 20:59:01 +0000 Subject: [PATCH 2/3] Update support table --- docs/src/rust-feature-support.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/docs/src/rust-feature-support.md b/docs/src/rust-feature-support.md index 18ebcb6c393f..0e1dcfe0befb 100644 --- a/docs/src/rust-feature-support.md +++ b/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 | | From 4d4b9aff29f5d65fb9a0e12a68cb3dd732399dcf Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 8 Apr 2022 21:20:48 +0000 Subject: [PATCH 3/3] Fix format --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 88762633c383..8f16512a0dc2 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -462,10 +462,10 @@ 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!( + "nearbyintf32" => codegen_unimplemented_intrinsic!( "https://github.com/model-checking/kani/issues/1025" ), - "nearbyintf64" => codegen_unimplemented_intrinsic!( + "nearbyintf64" => codegen_unimplemented_intrinsic!( "https://github.com/model-checking/kani/issues/1025" ), "needs_drop" => codegen_intrinsic_const!(), @@ -479,10 +479,10 @@ 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_unimplemented_intrinsic!( + "rintf32" => codegen_unimplemented_intrinsic!( "https://github.com/model-checking/kani/issues/1025" ), - "rintf64" => codegen_unimplemented_intrinsic!( + "rintf64" => codegen_unimplemented_intrinsic!( "https://github.com/model-checking/kani/issues/1025" ), "rotate_left" => codegen_intrinsic_binop!(rol), @@ -533,10 +533,10 @@ 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_unimplemented_intrinsic!( + "truncf32" => codegen_unimplemented_intrinsic!( "https://github.com/model-checking/kani/issues/1025" ), - "truncf64" => codegen_unimplemented_intrinsic!( + "truncf64" => codegen_unimplemented_intrinsic!( "https://github.com/model-checking/kani/issues/1025" ), "try" => {