Skip to content

Commit daee4b4

Browse files
zhassan-awszhassan-aws
committed
Revert "Update toolchain to 2025-03-02 (model-checking#3911)"
This reverts commit 9ea1f38.
1 parent 1eeade5 commit daee4b4

File tree

28 files changed

+353
-137
lines changed

28 files changed

+353
-137
lines changed

‎cprover_bindings/src/goto_program/builtin.rs‎

Lines changed: 1 addition & 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, PartialEq)]
9+
#[derive(Debug, Clone, Copy)]
1010
pub enum BuiltinFn {
1111
Abort,
1212
Assert,

‎cprover_bindings/src/machine_model.rs‎

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

5150
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,6 +180,8 @@ minnumf32 | Yes | |
180180
minnumf64 | Yes | |
181181
move_val_init | No | |
182182
mul_with_overflow | Yes | |
183+
nearbyintf32 | Yes | |
184+
nearbyintf64 | Yes | |
183185
needs_drop | Yes | |
184186
nontemporal_store | No | |
185187
offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) |
@@ -196,10 +198,8 @@ ptr_guaranteed_eq | Yes | |
196198
ptr_guaranteed_ne | Yes | |
197199
ptr_offset_from | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-4) |
198200
raw_eq | Partial | Cannot detect [uninitialized memory](#uninitialized-memory) |
199-
round_ties_even_f16 | No | |
200-
round_ties_even_f32 | Yes | |
201-
round_ties_even_f64 | Yes | |
202-
round_ties_even_f128 | No | |
201+
rintf32 | Yes | |
202+
rintf64 | Yes | |
203203
rotate_left | Yes | |
204204
rotate_right | Yes | |
205205
roundf32 | Yes | |

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,9 @@ 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.tool_attrs(&["kanitool".into(), "recursion_tracker".into()]).is_empty()
66+
if !static_item
67+
.attrs_by_path(&["kanitool".into(), "recursion_tracker".into()])
68+
.is_empty()
6769
{
6870
let span = static_item.span();
6971
let loc = self.codegen_span_stable(span);

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -414,6 +414,8 @@ 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),
417419
Intrinsic::NeedsDrop => codegen_intrinsic_const!(),
418420
Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf),
419421
Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow),
@@ -423,6 +425,8 @@ impl GotocCtx<'_> {
423425
Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc),
424426
Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
425427
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),
426430
Intrinsic::RotateLeft => codegen_intrinsic_binop!(rol),
427431
Intrinsic::RotateRight => codegen_intrinsic_binop!(ror),
428432
Intrinsic::RoundF32 => codegen_simple_intrinsic!(Roundf),

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

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1002,10 +1002,8 @@ 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: rustc_abi::Size = match &layout.fields {
1006-
FieldsShape::Arbitrary { offsets, .. } => {
1007-
offsets[rustc_abi::FieldIdx::from_usize(0)]
1008-
}
1005+
let offset = match &layout.fields {
1006+
FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
10091007
_ => unreachable!("niche encoding must have arbitrary fields"),
10101008
};
10111009

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

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ 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;
1110
use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
1211
use rustc_middle::ty::layout::LayoutOf;
1312
use rustc_middle::ty::{List, TypingEnv};
@@ -351,10 +350,8 @@ impl GotocCtx<'_> {
351350
}
352351
TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
353352
if *untagged_variant != variant_index_internal {
354-
let offset: Size = match &layout.fields {
355-
FieldsShape::Arbitrary { offsets, .. } => {
356-
offsets[rustc_abi::FieldIdx::from_usize(0)]
357-
}
353+
let offset = match &layout.fields {
354+
FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
358355
_ => unreachable!("niche encoding must have arbitrary fields"),
359356
};
360357
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[rustc_abi::FieldIdx::from(idx)];
721+
let fld_offset = offsets[idx.into()];
722722
let (fld_name, fld_ty) = &flds[idx];
723723
if let Some(padding) =
724724
self.codegen_struct_padding(offset, fld_offset, final_fields.len())
@@ -1556,9 +1556,9 @@ impl<'tcx> GotocCtx<'tcx> {
15561556
let components = fields_shape
15571557
.index_by_increasing_offset()
15581558
.map(|idx| {
1559-
let fidx = FieldIdx::from(idx);
1560-
let name = fields[fidx].name.to_string().intern();
1561-
let field_ty = fields[fidx].ty(ctx.tcx, adt_args);
1559+
let idx = idx.into();
1560+
let name = fields[idx].name.to_string().intern();
1561+
let field_ty = fields[idx].ty(ctx.tcx, adt_args);
15621562
let typ = if !ctx.is_zst(field_ty) {
15631563
last_type.clone()
15641564
} else {

‎kani-compiler/src/intrinsics.rs‎

Lines changed: 20 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,8 @@ pub enum Intrinsic {
8686
MinNumF32,
8787
MinNumF64,
8888
MulWithOverflow,
89+
NearbyIntF32,
90+
NearbyIntF64,
8991
NeedsDrop,
9092
PowF32,
9193
PowF64,
@@ -97,12 +99,12 @@ pub enum Intrinsic {
9799
PtrOffsetFromUnsigned,
98100
RawEq,
99101
RetagBoxToRaw,
102+
RintF32,
103+
RintF64,
100104
RotateLeft,
101105
RotateRight,
102106
RoundF32,
103107
RoundF64,
104-
RoundTiesEvenF32,
105-
RoundTiesEvenF64,
106108
SaturatingAdd,
107109
SaturatingSub,
108110
SinF32,
@@ -674,6 +676,10 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option<Intrinsic> {
674676
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
675677
Some(Intrinsic::MinNumF32)
676678
}
679+
"nearbyintf32" => {
680+
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
681+
Some(Intrinsic::NearbyIntF32)
682+
}
677683
"powf32" => {
678684
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
679685
Some(Intrinsic::PowF32)
@@ -682,13 +688,13 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option<Intrinsic> {
682688
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F32));
683689
Some(Intrinsic::PowIF32)
684690
}
685-
"roundf32" => {
691+
"rintf32" => {
686692
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
687-
Some(Intrinsic::RoundF32)
693+
Some(Intrinsic::RintF32)
688694
}
689-
"round_ties_even_f32" => {
695+
"roundf32" => {
690696
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
691-
Some(Intrinsic::RoundTiesEvenF32)
697+
Some(Intrinsic::RoundF32)
692698
}
693699
"sinf32" => {
694700
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
@@ -764,6 +770,10 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option<Intrinsic> {
764770
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
765771
Some(Intrinsic::MinNumF64)
766772
}
773+
"nearbyintf64" => {
774+
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
775+
Some(Intrinsic::NearbyIntF64)
776+
}
767777
"powf64" => {
768778
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
769779
Some(Intrinsic::PowF64)
@@ -772,13 +782,13 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option<Intrinsic> {
772782
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F64));
773783
Some(Intrinsic::PowIF64)
774784
}
775-
"roundf64" => {
785+
"rintf64" => {
776786
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
777-
Some(Intrinsic::RoundF64)
787+
Some(Intrinsic::RintF64)
778788
}
779-
"round_ties_even_f64" => {
789+
"roundf64" => {
780790
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
781-
Some(Intrinsic::RoundTiesEvenF64)
791+
Some(Intrinsic::RoundF64)
782792
}
783793
"sinf64" => {
784794
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));

0 commit comments

Comments
 (0)