Intrinsics rint, roundeven, nearbyint replaced by `round_ties_e…

…ven`.

Propagate changes from rust-lang/rust#136543
Use `__sort_of_CPROVER_round_to_integral` to model `round_ties_even`.
Update tests.

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,

cprover_bindings/src/machine_model.rs

@@ -45,6 +45,7 @@ pub enum RoundingMode {
     Downward = 1,
     Upward = 2,
     TowardsZero = 3,
+    ToAway = 4,
 }
 
 impl From<RoundingMode> for BigInt {

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 | |

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<Expr>,
+        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,

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<Intrinsic> {
             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<Intrinsic> {
             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<Intrinsic> {
             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<Intrinsic> {
             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)

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

kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs

@@ -625,17 +625,13 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
         | Intrinsic::MinNumF32
         | Intrinsic::MinNumF64
         | Intrinsic::MulWithOverflow
-        | Intrinsic::NearbyIntF32
-        | Intrinsic::NearbyIntF64
         | Intrinsic::NeedsDrop
         | Intrinsic::PowF32
         | Intrinsic::PowF64
         | Intrinsic::PowIF32
         | Intrinsic::PowIF64
         | Intrinsic::PrefAlignOf
         | Intrinsic::RawEq
-        | Intrinsic::RintF32
-        | Intrinsic::RintF64
         | Intrinsic::RotateLeft
         | Intrinsic::RotateRight
         | Intrinsic::RoundF32