Update toolchain to 2025-03-02 (#3911)

Changes to attribute parsing and representation rust-lang/rust#135726 Map methods moved to `TyCtx` rust-lang/rust#137162 rust-lang/rust#137397 Remove `BackendRepr::Unihabited` rust-lang/rust#136985 Intrinsics rint, roundeven, nearbyint replaced by `round_ties_even`. rust-lang/rust#136543. Use `__sort_of_CPROVER_round_to_integral` to model `round_ties_even`. Rename `sub_ptr` to `offset_from_unsigned`. The feature gate is still `ptr_sub_ptr`. rust-lang/rust#137483. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Remi Delmas <delmasrd@amazon.com>
model-checking · Mar 5, 2025 · 9ea1f38 · 9ea1f38
1 parent b93e591
commit 9ea1f38
Show file tree

Hide file tree

Showing 28 changed files with 183 additions and 353 deletions.
diff --git 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
@@ -45,6 +45,7 @@ pub enum RoundingMode {
     Downward = 1,
     Upward = 2,
     TowardsZero = 3,
+    ToAway = 4,
 }
 
 impl From<RoundingMode> for BigInt {

diff --git 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/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
@@ -63,9 +63,7 @@ impl GotocCtx<'_> {
         // Return item tagged with `#[kanitool::recursion_tracker]`
         let mut recursion_trackers = items.iter().filter_map(|item| {
             let MonoItem::Static(static_item) = item else { return None };
-            if !static_item
-                .attrs_by_path(&["kanitool".into(), "recursion_tracker".into()])
-                .is_empty()
+            if !static_item.tool_attrs(&["kanitool".into(), "recursion_tracker".into()]).is_empty()
             {
                 let span = static_item.span();
                 let loc = self.codegen_span_stable(span);

diff --git 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<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,

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -1002,8 +1002,10 @@ impl GotocCtx<'_> {
                     // https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247
                     // See also the cranelift backend:
                     // https://github.com/rust-lang/rust/blob/05d22212e89588e7c443cc6b9bc0e4e02fdfbc8d/compiler/rustc_codegen_cranelift/src/discriminant.rs#L116
-                    let offset = match &layout.fields {
-                        FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
+                    let offset: rustc_abi::Size = match &layout.fields {
+                        FieldsShape::Arbitrary { offsets, .. } => {
+                            offsets[rustc_abi::FieldIdx::from_usize(0)]
+                        }
                         _ => unreachable!("niche encoding must have arbitrary fields"),
                     };
 

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -7,6 +7,7 @@ use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_cov
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
+use rustc_abi::Size;
 use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{List, TypingEnv};
@@ -350,8 +351,10 @@ impl GotocCtx<'_> {
                 }
                 TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
                     if *untagged_variant != variant_index_internal {
-                        let offset = match &layout.fields {
-                            FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
+                        let offset: Size = match &layout.fields {
+                            FieldsShape::Arbitrary { offsets, .. } => {
+                                offsets[rustc_abi::FieldIdx::from_usize(0)]
+                            }
                             _ => unreachable!("niche encoding must have arbitrary fields"),
                         };
                         let discr_ty = self.codegen_enum_discr_typ(dest_ty_internal);

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -718,7 +718,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let mut final_fields = Vec::with_capacity(flds.len());
                 let mut offset = initial_offset;
                 for idx in layout.fields.index_by_increasing_offset() {
-                    let fld_offset = offsets[idx.into()];
+                    let fld_offset = offsets[rustc_abi::FieldIdx::from(idx)];
                     let (fld_name, fld_ty) = &flds[idx];
                     if let Some(padding) =
                         self.codegen_struct_padding(offset, fld_offset, final_fields.len())
@@ -1557,9 +1557,9 @@ impl<'tcx> GotocCtx<'tcx> {
                     let components = fields_shape
                         .index_by_increasing_offset()
                         .map(|idx| {
-                            let idx = idx.into();
-                            let name = fields[idx].name.to_string().intern();
-                            let field_ty = fields[idx].ty(ctx.tcx, adt_args);
+                            let fidx = FieldIdx::from(idx);
+                            let name = fields[fidx].name.to_string().intern();
+                            let field_ty = fields[fidx].ty(ctx.tcx, adt_args);
                             let typ = if !ctx.is_zst(field_ty) {
                                 last_type.clone()
                             } else {

diff --git 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<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)