Skip to content

Commit 9ea1f38

Browse files
remi-delmas-3000Remi Delmas
remi-delmas-3000
and
Remi Delmas
authored
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 <[email protected]>
1 parent b93e591 commit 9ea1f38

File tree

28 files changed

+183
-353
lines changed

28 files changed

+183
-353
lines changed

‎cprover_bindings/src/goto_program/builtin.rs

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use super::{Expr, Location, Symbol, Type};
66

77
use std::fmt::Display;
88

9-
#[derive(Debug, Clone, Copy)]
9+
#[derive(Debug, Clone, Copy, PartialEq)]
1010
pub enum BuiltinFn {
1111
Abort,
1212
Assert,
@@ -59,6 +59,8 @@ pub enum BuiltinFn {
5959
Rintf,
6060
Round,
6161
Roundf,
62+
RoundToIntegralF,
63+
RoundToIntegral,
6264
Sin,
6365
Sinf,
6466
Sqrt,
@@ -123,6 +125,9 @@ impl Display for BuiltinFn {
123125
Rintf => "rintf",
124126
Round => "round",
125127
Roundf => "roundf",
128+
// TODO remove the sort_of prefix once we move up from CBMC 6.4.1
129+
RoundToIntegralF => "__sort_of_CPROVER_round_to_integralf",
130+
RoundToIntegral => "__sort_of_CPROVER_round_to_integral",
126131
Sin => "sin",
127132
Sinf => "sinf",
128133
Sqrt => "sqrt",
@@ -188,6 +193,8 @@ impl BuiltinFn {
188193
Rintf => vec![Type::float()],
189194
Round => vec![Type::double()],
190195
Roundf => vec![Type::float()],
196+
RoundToIntegralF => vec![Type::c_int(), Type::float()],
197+
RoundToIntegral => vec![Type::c_int(), Type::double()],
191198
Sin => vec![Type::double()],
192199
Sinf => vec![Type::float()],
193200
Sqrt => vec![Type::double()],
@@ -252,6 +259,8 @@ impl BuiltinFn {
252259
Rintf => Type::float(),
253260
Round => Type::double(),
254261
Roundf => Type::float(),
262+
RoundToIntegralF => Type::float(),
263+
RoundToIntegral => Type::double(),
255264
Sin => Type::double(),
256265
Sinf => Type::float(),
257266
Sqrt => Type::double(),
@@ -316,6 +325,8 @@ impl BuiltinFn {
316325
Rintf,
317326
Round,
318327
Roundf,
328+
RoundToIntegralF,
329+
RoundToIntegral,
319330
Sin,
320331
Sinf,
321332
Sqrt,

‎cprover_bindings/src/machine_model.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ pub enum RoundingMode {
4545
Downward = 1,
4646
Upward = 2,
4747
TowardsZero = 3,
48+
ToAway = 4,
4849
}
4950

5051
impl From<RoundingMode> for BigInt {

‎docs/src/rust-feature-support/intrinsics.md

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -180,8 +180,6 @@ minnumf32 | Yes | |
180180
minnumf64 | Yes | |
181181
move_val_init | No | |
182182
mul_with_overflow | Yes | |
183-
nearbyintf32 | Yes | |
184-
nearbyintf64 | Yes | |
185183
needs_drop | Yes | |
186184
nontemporal_store | No | |
187185
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 | |
198196
ptr_guaranteed_ne | Yes | |
199197
ptr_offset_from | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-4) |
200198
raw_eq | Partial | Cannot detect [uninitialized memory](#uninitialized-memory) |
201-
rintf32 | Yes | |
202-
rintf64 | Yes | |
199+
round_ties_even_f16 | No | |
200+
round_ties_even_f32 | Yes | |
201+
round_ties_even_f64 | Yes | |
202+
round_ties_even_f128 | No | |
203203
rotate_left | Yes | |
204204
rotate_right | Yes | |
205205
roundf32 | Yes | |

‎kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -63,9 +63,7 @@ impl GotocCtx<'_> {
6363
// Return item tagged with `#[kanitool::recursion_tracker]`
6464
let mut recursion_trackers = items.iter().filter_map(|item| {
6565
let MonoItem::Static(static_item) = item else { return None };
66-
if !static_item
67-
.attrs_by_path(&["kanitool".into(), "recursion_tracker".into()])
68-
.is_empty()
66+
if !static_item.tool_attrs(&["kanitool".into(), "recursion_tracker".into()]).is_empty()
6967
{
7068
let span = static_item.span();
7169
let loc = self.codegen_span_stable(span);

‎kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Lines changed: 35 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -414,8 +414,6 @@ impl GotocCtx<'_> {
414414
Intrinsic::MulWithOverflow => {
415415
self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, place, loc)
416416
}
417-
Intrinsic::NearbyIntF32 => codegen_simple_intrinsic!(Nearbyintf),
418-
Intrinsic::NearbyIntF64 => codegen_simple_intrinsic!(Nearbyint),
419417
Intrinsic::NeedsDrop => codegen_intrinsic_const!(),
420418
Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf),
421419
Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow),
@@ -425,12 +423,24 @@ impl GotocCtx<'_> {
425423
Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc),
426424
Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
427425
Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc),
428-
Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf),
429-
Intrinsic::RintF64 => codegen_simple_intrinsic!(Rint),
430426
Intrinsic::RotateLeft => codegen_intrinsic_binop!(rol),
431427
Intrinsic::RotateRight => codegen_intrinsic_binop!(ror),
432428
Intrinsic::RoundF32 => codegen_simple_intrinsic!(Roundf),
433429
Intrinsic::RoundF64 => codegen_simple_intrinsic!(Round),
430+
Intrinsic::RoundTiesEvenF32 => self.codegen_round_to_integral(
431+
BuiltinFn::RoundToIntegralF,
432+
cbmc::RoundingMode::ToNearest,
433+
fargs,
434+
place,
435+
loc,
436+
),
437+
Intrinsic::RoundTiesEvenF64 => self.codegen_round_to_integral(
438+
BuiltinFn::RoundToIntegral,
439+
cbmc::RoundingMode::ToNearest,
440+
fargs,
441+
place,
442+
loc,
443+
),
434444
Intrinsic::SaturatingAdd => codegen_intrinsic_binop_with_mm!(saturating_add),
435445
Intrinsic::SaturatingSub => codegen_intrinsic_binop_with_mm!(saturating_sub),
436446
Intrinsic::SinF32 => codegen_simple_intrinsic!(Sinf),
@@ -638,6 +648,27 @@ impl GotocCtx<'_> {
638648
dividend_is_int_min.and(divisor_is_minus_one).not()
639649
}
640650

651+
// Builds a call to the round_to_integral CPROVER function with specified cbmc::RoundingMode.
652+
fn codegen_round_to_integral(
653+
&mut self,
654+
function: BuiltinFn,
655+
rounding_mode: cbmc::RoundingMode,
656+
mut fargs: Vec<Expr>,
657+
place: &Place,
658+
loc: Location,
659+
) -> Stmt {
660+
assert!(function == BuiltinFn::RoundToIntegralF || function == BuiltinFn::RoundToIntegral);
661+
let mm = self.symbol_table.machine_model();
662+
fargs.insert(0, Expr::int_constant(rounding_mode, Type::c_int()));
663+
let casted_fargs = Expr::cast_arguments_to_target_equivalent_function_parameter_types(
664+
&function.as_expr(),
665+
fargs,
666+
mm,
667+
);
668+
let expr = function.call(casted_fargs, loc);
669+
self.codegen_expr_to_place_stable(place, expr, loc)
670+
}
671+
641672
/// Intrinsics of the form *_with_overflow
642673
fn codegen_op_with_overflow(
643674
&mut self,

‎kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1002,8 +1002,10 @@ impl GotocCtx<'_> {
10021002
// https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247
10031003
// See also the cranelift backend:
10041004
// https://github.com/rust-lang/rust/blob/05d22212e89588e7c443cc6b9bc0e4e02fdfbc8d/compiler/rustc_codegen_cranelift/src/discriminant.rs#L116
1005-
let offset = match &layout.fields {
1006-
FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
1005+
let offset: rustc_abi::Size = match &layout.fields {
1006+
FieldsShape::Arbitrary { offsets, .. } => {
1007+
offsets[rustc_abi::FieldIdx::from_usize(0)]
1008+
}
10071009
_ => unreachable!("niche encoding must have arbitrary fields"),
10081010
};
10091011

‎kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_cov
77
use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
88
use crate::unwrap_or_return_codegen_unimplemented_stmt;
99
use cbmc::goto_program::{Expr, Location, Stmt, Type};
10+
use rustc_abi::Size;
1011
use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
1112
use rustc_middle::ty::layout::LayoutOf;
1213
use rustc_middle::ty::{List, TypingEnv};
@@ -350,8 +351,10 @@ impl GotocCtx<'_> {
350351
}
351352
TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
352353
if *untagged_variant != variant_index_internal {
353-
let offset = match &layout.fields {
354-
FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
354+
let offset: Size = match &layout.fields {
355+
FieldsShape::Arbitrary { offsets, .. } => {
356+
offsets[rustc_abi::FieldIdx::from_usize(0)]
357+
}
355358
_ => unreachable!("niche encoding must have arbitrary fields"),
356359
};
357360
let discr_ty = self.codegen_enum_discr_typ(dest_ty_internal);

‎kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -718,7 +718,7 @@ impl<'tcx> GotocCtx<'tcx> {
718718
let mut final_fields = Vec::with_capacity(flds.len());
719719
let mut offset = initial_offset;
720720
for idx in layout.fields.index_by_increasing_offset() {
721-
let fld_offset = offsets[idx.into()];
721+
let fld_offset = offsets[rustc_abi::FieldIdx::from(idx)];
722722
let (fld_name, fld_ty) = &flds[idx];
723723
if let Some(padding) =
724724
self.codegen_struct_padding(offset, fld_offset, final_fields.len())
@@ -1557,9 +1557,9 @@ impl<'tcx> GotocCtx<'tcx> {
15571557
let components = fields_shape
15581558
.index_by_increasing_offset()
15591559
.map(|idx| {
1560-
let idx = idx.into();
1561-
let name = fields[idx].name.to_string().intern();
1562-
let field_ty = fields[idx].ty(ctx.tcx, adt_args);
1560+
let fidx = FieldIdx::from(idx);
1561+
let name = fields[fidx].name.to_string().intern();
1562+
let field_ty = fields[fidx].ty(ctx.tcx, adt_args);
15631563
let typ = if !ctx.is_zst(field_ty) {
15641564
last_type.clone()
15651565
} else {

‎kani-compiler/src/intrinsics.rs

Lines changed: 10 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -86,8 +86,6 @@ pub enum Intrinsic {
8686
MinNumF32,
8787
MinNumF64,
8888
MulWithOverflow,
89-
NearbyIntF32,
90-
NearbyIntF64,
9189
NeedsDrop,
9290
PowF32,
9391
PowF64,
@@ -99,12 +97,12 @@ pub enum Intrinsic {
9997
PtrOffsetFromUnsigned,
10098
RawEq,
10199
RetagBoxToRaw,
102-
RintF32,
103-
RintF64,
104100
RotateLeft,
105101
RotateRight,
106102
RoundF32,
107103
RoundF64,
104+
RoundTiesEvenF32,
105+
RoundTiesEvenF64,
108106
SaturatingAdd,
109107
SaturatingSub,
110108
SinF32,
@@ -676,10 +674,6 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option<Intrinsic> {
676674
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
677675
Some(Intrinsic::MinNumF32)
678676
}
679-
"nearbyintf32" => {
680-
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
681-
Some(Intrinsic::NearbyIntF32)
682-
}
683677
"powf32" => {
684678
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
685679
Some(Intrinsic::PowF32)
@@ -688,14 +682,14 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option<Intrinsic> {
688682
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F32));
689683
Some(Intrinsic::PowIF32)
690684
}
691-
"rintf32" => {
692-
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
693-
Some(Intrinsic::RintF32)
694-
}
695685
"roundf32" => {
696686
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
697687
Some(Intrinsic::RoundF32)
698688
}
689+
"round_ties_even_f32" => {
690+
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
691+
Some(Intrinsic::RoundTiesEvenF32)
692+
}
699693
"sinf32" => {
700694
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
701695
Some(Intrinsic::SinF32)
@@ -770,10 +764,6 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option<Intrinsic> {
770764
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
771765
Some(Intrinsic::MinNumF64)
772766
}
773-
"nearbyintf64" => {
774-
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
775-
Some(Intrinsic::NearbyIntF64)
776-
}
777767
"powf64" => {
778768
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
779769
Some(Intrinsic::PowF64)
@@ -782,14 +772,14 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option<Intrinsic> {
782772
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F64));
783773
Some(Intrinsic::PowIF64)
784774
}
785-
"rintf64" => {
786-
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
787-
Some(Intrinsic::RintF64)
788-
}
789775
"roundf64" => {
790776
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
791777
Some(Intrinsic::RoundF64)
792778
}
779+
"round_ties_even_f64" => {
780+
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
781+
Some(Intrinsic::RoundTiesEvenF64)
782+
}
793783
"sinf64" => {
794784
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
795785
Some(Intrinsic::SinF64)

0 commit comments

Comments
 (0)