From d9ad6e17d6cef2e6f49161ab70e327a96525fb13 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 27 Feb 2025 12:51:01 -0500 Subject: [PATCH] Intrinsics `rint`, `roundeven`, `nearbyint` replaced by `round_ties_even`. Propagate changes from https://github.com/rust-lang/rust/pull/136543 Use `__sort_of_CPROVER_round_to_integral` to model `round_ties_even`. Update tests. --- cprover_bindings/src/goto_program/builtin.rs | 13 ++- cprover_bindings/src/machine_model.rs | 1 + docs/src/rust-feature-support/intrinsics.md | 8 +- .../codegen/intrinsic.rs | 39 ++++++- kani-compiler/src/intrinsics.rs | 30 ++--- .../points_to/points_to_analysis.rs | 4 - .../check_uninit/ptr_uninit/uninit_visitor.rs | 4 - .../Intrinsics/Math/Rounding/RInt/rintf32.rs | 104 ------------------ .../Intrinsics/Math/Rounding/RInt/rintf64.rs | 104 ------------------ .../round_ties_even_f32.rs} | 20 ++-- .../round_ties_even_f64.rs} | 20 ++-- 11 files changed, 82 insertions(+), 265 deletions(-) delete mode 100644 tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs delete mode 100644 tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs rename tests/kani/Intrinsics/Math/Rounding/{NearbyInt/nearbyintf32.rs => RoundTiesEven/round_ties_even_f32.rs} (79%) rename tests/kani/Intrinsics/Math/Rounding/{NearbyInt/nearbyintf64.rs => RoundTiesEven/round_ties_even_f64.rs} (79%) diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index a0c1f211b5e2..0ff2296a1024 100644 --- a/cprover_bindings/src/goto_program/builtin.rs +++ b/cprover_bindings/src/goto_program/builtin.rs @@ -6,7 +6,7 @@ use super::{Expr, Location, Symbol, Type}; use std::fmt::Display; -#[derive(Debug, Clone, Copy)] +#[derive(Debug, Clone, Copy, PartialEq)] pub enum BuiltinFn { Abort, Assert, @@ -59,6 +59,8 @@ pub enum BuiltinFn { Rintf, Round, Roundf, + RoundToIntegralF, + RoundToIntegral, Sin, Sinf, Sqrt, @@ -123,6 +125,9 @@ impl Display for BuiltinFn { Rintf => "rintf", Round => "round", Roundf => "roundf", + // TODO remove the sort_of prefix once we move up from CBMC 6.4.1 + RoundToIntegralF => "__sort_of_CPROVER_round_to_integralf", + RoundToIntegral => "__sort_of_CPROVER_round_to_integral", Sin => "sin", Sinf => "sinf", Sqrt => "sqrt", @@ -188,6 +193,8 @@ impl BuiltinFn { Rintf => vec![Type::float()], Round => vec![Type::double()], Roundf => vec![Type::float()], + RoundToIntegralF => vec![Type::c_int(), Type::float()], + RoundToIntegral => vec![Type::c_int(), Type::double()], Sin => vec![Type::double()], Sinf => vec![Type::float()], Sqrt => vec![Type::double()], @@ -252,6 +259,8 @@ impl BuiltinFn { Rintf => Type::float(), Round => Type::double(), Roundf => Type::float(), + RoundToIntegralF => Type::float(), + RoundToIntegral => Type::double(), Sin => Type::double(), Sinf => Type::float(), Sqrt => Type::double(), @@ -316,6 +325,8 @@ impl BuiltinFn { Rintf, Round, Roundf, + RoundToIntegralF, + RoundToIntegral, Sin, Sinf, Sqrt, diff --git a/cprover_bindings/src/machine_model.rs b/cprover_bindings/src/machine_model.rs index 31427a83a629..463fe8f047e6 100644 --- a/cprover_bindings/src/machine_model.rs +++ b/cprover_bindings/src/machine_model.rs @@ -45,6 +45,7 @@ pub enum RoundingMode { Downward = 1, Upward = 2, TowardsZero = 3, + ToAway = 4, } impl From for BigInt { diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 9f3495da0adc..2fa8b54094fc 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -180,8 +180,6 @@ minnumf32 | Yes | | minnumf64 | Yes | | move_val_init | No | | mul_with_overflow | Yes | | -nearbyintf32 | Yes | | -nearbyintf64 | Yes | | needs_drop | Yes | | nontemporal_store | No | | offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) | @@ -198,8 +196,10 @@ ptr_guaranteed_eq | Yes | | ptr_guaranteed_ne | Yes | | ptr_offset_from | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-4) | raw_eq | Partial | Cannot detect [uninitialized memory](#uninitialized-memory) | -rintf32 | Yes | | -rintf64 | Yes | | +round_ties_even_f16 | No | | +round_ties_even_f32 | Yes | | +round_ties_even_f64 | Yes | | +round_ties_even_f128 | No | | rotate_left | Yes | | rotate_right | Yes | | roundf32 | Yes | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index bbdc0be7910a..ac5b44ec4163 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -414,8 +414,6 @@ impl GotocCtx<'_> { Intrinsic::MulWithOverflow => { self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, place, loc) } - Intrinsic::NearbyIntF32 => codegen_simple_intrinsic!(Nearbyintf), - Intrinsic::NearbyIntF64 => codegen_simple_intrinsic!(Nearbyint), Intrinsic::NeedsDrop => codegen_intrinsic_const!(), Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf), Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow), @@ -425,12 +423,24 @@ impl GotocCtx<'_> { Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc), - Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf), - Intrinsic::RintF64 => codegen_simple_intrinsic!(Rint), Intrinsic::RotateLeft => codegen_intrinsic_binop!(rol), Intrinsic::RotateRight => codegen_intrinsic_binop!(ror), Intrinsic::RoundF32 => codegen_simple_intrinsic!(Roundf), Intrinsic::RoundF64 => codegen_simple_intrinsic!(Round), + Intrinsic::RoundTiesEvenF32 => self.codegen_round_to_integral( + BuiltinFn::RoundToIntegralF, + cbmc::RoundingMode::ToNearest, + fargs, + place, + loc, + ), + Intrinsic::RoundTiesEvenF64 => self.codegen_round_to_integral( + BuiltinFn::RoundToIntegral, + cbmc::RoundingMode::ToNearest, + fargs, + place, + loc, + ), Intrinsic::SaturatingAdd => codegen_intrinsic_binop_with_mm!(saturating_add), Intrinsic::SaturatingSub => codegen_intrinsic_binop_with_mm!(saturating_sub), Intrinsic::SinF32 => codegen_simple_intrinsic!(Sinf), @@ -638,6 +648,27 @@ impl GotocCtx<'_> { dividend_is_int_min.and(divisor_is_minus_one).not() } + // Builds a call to the round_to_integral CPROVER function with specified cbmc::RoundingMode. + fn codegen_round_to_integral( + &mut self, + function: BuiltinFn, + rounding_mode: cbmc::RoundingMode, + mut fargs: Vec, + place: &Place, + loc: Location, + ) -> Stmt { + assert!(function == BuiltinFn::RoundToIntegralF || function == BuiltinFn::RoundToIntegral); + let mm = self.symbol_table.machine_model(); + fargs.insert(0, Expr::int_constant(rounding_mode, Type::c_int())); + let casted_fargs = Expr::cast_arguments_to_target_equivalent_function_parameter_types( + &function.as_expr(), + fargs, + mm, + ); + let expr = function.call(casted_fargs, loc); + self.codegen_expr_to_place_stable(place, expr, loc) + } + /// Intrinsics of the form *_with_overflow fn codegen_op_with_overflow( &mut self, diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index f58a40bf8cb6..5d9ab8221453 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -86,8 +86,6 @@ pub enum Intrinsic { MinNumF32, MinNumF64, MulWithOverflow, - NearbyIntF32, - NearbyIntF64, NeedsDrop, PowF32, PowF64, @@ -99,12 +97,12 @@ pub enum Intrinsic { PtrOffsetFromUnsigned, RawEq, RetagBoxToRaw, - RintF32, - RintF64, RotateLeft, RotateRight, RoundF32, RoundF64, + RoundTiesEvenF32, + RoundTiesEvenF64, SaturatingAdd, SaturatingSub, SinF32, @@ -676,10 +674,6 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::MinNumF32) } - "nearbyintf32" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); - Some(Intrinsic::NearbyIntF32) - } "powf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::PowF32) @@ -688,14 +682,14 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::PowIF32) } - "rintf32" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); - Some(Intrinsic::RintF32) - } "roundf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::RoundF32) } + "round_ties_even_f32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::RoundTiesEvenF32) + } "sinf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::SinF32) @@ -770,10 +764,6 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::MinNumF64) } - "nearbyintf64" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); - Some(Intrinsic::NearbyIntF64) - } "powf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::PowF64) @@ -782,14 +772,14 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::PowIF64) } - "rintf64" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); - Some(Intrinsic::RintF64) - } "roundf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::RoundF64) } + "round_ties_even_f64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::RoundTiesEvenF64) + } "sinf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::SinF64) diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index a89baf963e7f..591d8c3574ff 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -664,8 +664,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::MinNumF32 | Intrinsic::MinNumF64 | Intrinsic::MulWithOverflow - | Intrinsic::NearbyIntF32 - | Intrinsic::NearbyIntF64 | Intrinsic::NeedsDrop | Intrinsic::PowF32 | Intrinsic::PowF64 @@ -677,8 +675,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::PtrOffsetFromUnsigned | Intrinsic::RawEq | Intrinsic::RetagBoxToRaw - | Intrinsic::RintF32 - | Intrinsic::RintF64 | Intrinsic::RotateLeft | Intrinsic::RotateRight | Intrinsic::RoundF32 diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 20f4538453b5..02d928eff75e 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -625,8 +625,6 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::MinNumF32 | Intrinsic::MinNumF64 | Intrinsic::MulWithOverflow - | Intrinsic::NearbyIntF32 - | Intrinsic::NearbyIntF64 | Intrinsic::NeedsDrop | Intrinsic::PowF32 | Intrinsic::PowF64 @@ -634,8 +632,6 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::PowIF64 | Intrinsic::PrefAlignOf | Intrinsic::RawEq - | Intrinsic::RintF32 - | Intrinsic::RintF64 | Intrinsic::RotateLeft | Intrinsic::RotateRight | Intrinsic::RoundF32 diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs deleted file mode 100644 index 79a0a4f9be2c..000000000000 --- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs +++ /dev/null @@ -1,104 +0,0 @@ -// 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 deleted file mode 100644 index 8c8ea583a2d5..000000000000 --- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs +++ /dev/null @@ -1,104 +0,0 @@ -// 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/NearbyInt/nearbyintf32.rs b/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f32.rs similarity index 79% rename from tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs rename to tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f32.rs index 25e02f45a943..057483b3b0cc 100644 --- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f32.rs @@ -1,51 +1,51 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Checks that `nearbyintf32` returns the nearest integer to the argument. The +// Checks that `round_ties_even_f32` 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; +use std::intrinsics::round_ties_even_f32; #[kani::proof] fn test_one() { let one = 1.0; - let result = unsafe { nearbyintf32(one) }; + let result = round_ties_even_f32(one); assert!(result == 1.0); } #[kani::proof] fn test_one_frac() { let one_frac = 1.9; - let result = unsafe { nearbyintf32(one_frac) }; + let result = round_ties_even_f32(one_frac); assert!(result == 2.0); } #[kani::proof] fn test_half_down() { let one_frac = 2.5; - let result = unsafe { nearbyintf32(one_frac) }; + let result = round_ties_even_f32(one_frac); assert!(result == 2.0); } #[kani::proof] fn test_half_up() { let one_frac = 3.5; - let result = unsafe { nearbyintf32(one_frac) }; + let result = round_ties_even_f32(one_frac); assert!(result == 4.0); } #[kani::proof] fn test_conc() { let conc = -42.6; - let result = unsafe { nearbyintf32(conc) }; + let result = round_ties_even_f32(conc); assert!(result == -43.0); } #[kani::proof] fn test_conc_sci() { let conc = 5.4e-2; - let result = unsafe { nearbyintf32(conc) }; + let result = round_ties_even_f32(conc); assert!(result == 0.0); } @@ -54,7 +54,7 @@ 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 result = round_ties_even_f32(x); let frac = x.fract().abs(); if x.is_sign_positive() { if frac > 0.5 { @@ -92,7 +92,7 @@ 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 result = round_ties_even_f32(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/RoundTiesEven/round_ties_even_f64.rs similarity index 79% rename from tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs rename to tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f64.rs index 589a44a4d1ac..c7c1a9611bae 100644 --- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f64.rs @@ -1,51 +1,51 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Checks that `nearbyintf64` returns the nearest integer to the argument. The +// Checks that `round_ties_even_f64` 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; +use std::intrinsics::round_ties_even_f64; #[kani::proof] fn test_one() { let one = 1.0; - let result = unsafe { nearbyintf64(one) }; + let result = round_ties_even_f64(one); assert!(result == 1.0); } #[kani::proof] fn test_one_frac() { let one_frac = 1.9; - let result = unsafe { nearbyintf64(one_frac) }; + let result = round_ties_even_f64(one_frac); assert!(result == 2.0); } #[kani::proof] fn test_half_down() { let one_frac = 2.5; - let result = unsafe { nearbyintf64(one_frac) }; + let result = round_ties_even_f64(one_frac); assert!(result == 2.0); } #[kani::proof] fn test_half_up() { let one_frac = 3.5; - let result = unsafe { nearbyintf64(one_frac) }; + let result = round_ties_even_f64(one_frac); assert!(result == 4.0); } #[kani::proof] fn test_conc() { let conc = -42.6; - let result = unsafe { nearbyintf64(conc) }; + let result = round_ties_even_f64(conc); assert!(result == -43.0); } #[kani::proof] fn test_conc_sci() { let conc = 5.4e-2; - let result = unsafe { nearbyintf64(conc) }; + let result = round_ties_even_f64(conc); assert!(result == 0.0); } @@ -54,7 +54,7 @@ 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 result = round_ties_even_f64(x); let frac = x.fract().abs(); if x.is_sign_positive() { if frac > 0.5 { @@ -92,7 +92,7 @@ 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 result = round_ties_even_f64(x); let diff = (x - result).abs(); assert!(diff <= 0.5); assert!(diff >= 0.0);