From 252c1ce11a8bf772c5a41795a322662da0b1bd0a Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Tue, 14 Jun 2022 11:52:29 -0400 Subject: [PATCH] Audit for `rintf*` and `nearbyintf*` intrinsics (#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] --- .../codegen/intrinsic.rs | 16 +-- .../Math/Rounding/NearbyInt/nearbyintf32.rs | 99 +++++++++++++++++ .../Math/Rounding/NearbyInt/nearbyintf64.rs | 99 +++++++++++++++++ .../Intrinsics/Math/Rounding/RInt/rintf32.rs | 104 ++++++++++++++++++ .../Intrinsics/Math/Rounding/RInt/rintf64.rs | 104 ++++++++++++++++++ .../Math/Rounding/Round/roundf32.rs | 2 +- .../Math/Rounding/Round/roundf64.rs | 2 +- .../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 --- 11 files changed, 412 insertions(+), 66 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs create mode 100644 tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs create mode 100644 tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs create mode 100644 tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs delete mode 100644 tests/kani/Intrinsics/Math/Rounding/nearbyintf32.rs delete mode 100644 tests/kani/Intrinsics/Math/Rounding/nearbyintf64.rs delete mode 100644 tests/kani/Intrinsics/Math/Rounding/rintf32.rs delete mode 100644 tests/kani/Intrinsics/Math/Rounding/rintf64.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 918dcb1cfabd..29c64f519152 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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), diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs new file mode 100644 index 000000000000..25e02f45a943 --- /dev/null +++ b/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); +} diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs new file mode 100644 index 000000000000..589a44a4d1ac --- /dev/null +++ b/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); +} diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs new file mode 100644 index 000000000000..79a0a4f9be2c --- /dev/null +++ b/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); +} diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs new file mode 100644 index 000000000000..8c8ea583a2d5 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs @@ -0,0 +1,104 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `rintf64` 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 +// +// `rintf64` works like `nearbyintf64`, 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, `rintf64` and `nearbyintf64` work the same way. +#![feature(core_intrinsics)] +use std::intrinsics::rintf64; + +#[kani::proof] +fn test_one() { + let one = 1.0; + let result = unsafe { rintf64(one) }; + assert!(result == 1.0); +} + +#[kani::proof] +fn test_one_frac() { + let one_frac = 1.9; + let result = unsafe { rintf64(one_frac) }; + assert!(result == 2.0); +} + +#[kani::proof] +fn test_half_down() { + let one_frac = 2.5; + let result = unsafe { rintf64(one_frac) }; + assert!(result == 2.0); +} + +#[kani::proof] +fn test_half_up() { + let one_frac = 3.5; + let result = unsafe { rintf64(one_frac) }; + assert!(result == 4.0); +} + +#[kani::proof] +fn test_conc() { + let conc = -42.6; + let result = unsafe { rintf64(conc) }; + assert!(result == -43.0); +} + +#[kani::proof] +fn test_conc_sci() { + let conc = 5.4e-2; + let result = unsafe { rintf64(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 { rintf64(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 { rintf64(x) }; + let diff = (x - result).abs(); + assert!(diff <= 0.5); + assert!(diff >= 0.0); +} diff --git a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs index d88c7fb0aac2..8a8780878925 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs @@ -61,7 +61,7 @@ fn test_towards_closer() { } #[kani::proof] -fn test_diff_one() { +fn test_diff_half_one() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); kani::assume(!x.is_infinite()); diff --git a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs index 7f084f08dc94..ddafc45a2e9e 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs @@ -61,7 +61,7 @@ fn test_towards_closer() { } #[kani::proof] -fn test_diff_one() { +fn test_diff_half_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); kani::assume(!x.is_infinite()); diff --git a/tests/kani/Intrinsics/Math/Rounding/nearbyintf32.rs b/tests/kani/Intrinsics/Math/Rounding/nearbyintf32.rs deleted file mode 100644 index b65f138276bb..000000000000 --- a/tests/kani/Intrinsics/Math/Rounding/nearbyintf32.rs +++ /dev/null @@ -1,13 +0,0 @@ -// Copyright Kani Contributors -// 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 deleted file mode 100644 index 51ad5d5f59c5..000000000000 --- a/tests/kani/Intrinsics/Math/Rounding/nearbyintf64.rs +++ /dev/null @@ -1,13 +0,0 @@ -// Copyright Kani Contributors -// 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 deleted file mode 100644 index a39573080cd4..000000000000 --- a/tests/kani/Intrinsics/Math/Rounding/rintf32.rs +++ /dev/null @@ -1,13 +0,0 @@ -// Copyright Kani Contributors -// 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 deleted file mode 100644 index b39ee126085b..000000000000 --- a/tests/kani/Intrinsics/Math/Rounding/rintf64.rs +++ /dev/null @@ -1,13 +0,0 @@ -// Copyright Kani Contributors -// 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) }; -}