Skip to content

Commit 9ee764f

Browse files
qinhepingqinheping
authored
Update toolchain to 2025-03-04 (model-checking#3927)
Resolves: model-checking#3924 Related commits: rust-lang/rust@aac65f562b rename BackendRepr::Vector → SimdVector By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent fcc5c4b commit 9ee764f

File tree

6 files changed

+43
-65
lines changed

6 files changed

+43
-65
lines changed

‎cprover_bindings/src/irep/goto_binary_serde.rs

Lines changed: 23 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ use std::collections::HashMap;
8484
use std::fs::File;
8585
use std::hash::Hash;
8686
use std::io::{self, BufReader};
87-
use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write};
87+
use std::io::{BufWriter, Bytes, Error, Read, Write};
8888
use std::path::Path;
8989

9090
/// Writes a symbol table to a file in goto binary format in version 6.
@@ -557,7 +557,7 @@ where
557557
R: Read,
558558
{
559559
/// Stream of bytes from which GOTO objects are read.
560-
bytes: Bytes<R>,
560+
bytes: Bytes<BufReader<R>>,
561561

562562
/// Numbering for ireps
563563
numbering: IrepNumbering,
@@ -584,8 +584,9 @@ where
584584
/// Constructor. The reader is moved into this object and cannot be used
585585
/// afterwards.
586586
fn new(reader: R) -> Self {
587+
let buffered_reader = BufReader::new(reader);
587588
GotoBinaryDeserializer {
588-
bytes: reader.bytes(),
589+
bytes: buffered_reader.bytes(),
589590
numbering: IrepNumbering::new(),
590591
string_count: Vec::new(),
591592
string_map: Vec::new(),
@@ -597,12 +598,9 @@ where
597598
/// Returns Err if the found value is not the expected value.
598599
fn expect<T: Eq + std::fmt::Display>(found: T, expected: T) -> io::Result<T> {
599600
if found != expected {
600-
return Err(Error::new(
601-
ErrorKind::Other,
602-
format!(
603-
"Invalid goto binary input: expected {expected} in byte stream, found {found} instead)"
604-
),
605-
));
601+
return Err(Error::other(format!(
602+
"Invalid goto binary input: expected {expected} in byte stream, found {found} instead)"
603+
)));
606604
}
607605
Ok(found)
608606
}
@@ -660,10 +658,7 @@ where
660658
match self.bytes.next() {
661659
Some(Ok(u)) => Ok(u),
662660
Some(Err(error)) => Err(error),
663-
None => Err(Error::new(
664-
ErrorKind::Other,
665-
"Invalid goto binary input: unexpected end of input",
666-
)),
661+
None => Err(Error::other("Invalid goto binary input: unexpected end of input")),
667662
}
668663
}
669664

@@ -677,8 +672,7 @@ where
677672
match self.bytes.next() {
678673
Some(Ok(u)) => {
679674
if shift >= max_shift {
680-
return Err(Error::new(
681-
ErrorKind::Other,
675+
return Err(Error::other(
682676
"Invalid goto binary input: serialized value is too large to fit in usize",
683677
));
684678
};
@@ -692,10 +686,7 @@ where
692686
return Err(error);
693687
}
694688
None => {
695-
return Err(Error::new(
696-
ErrorKind::Other,
697-
"Invalid goto binary input: unexpected end of input",
698-
));
689+
return Err(Error::other("Invalid goto binary input: unexpected end of input"));
699690
}
700691
}
701692
}
@@ -721,10 +712,7 @@ where
721712
return Ok(numbered);
722713
}
723714
Err(error) => {
724-
return Err(Error::new(
725-
ErrorKind::Other,
726-
error.to_string(),
727-
));
715+
return Err(Error::other(error.to_string()));
728716
}
729717
}
730718
}
@@ -738,8 +726,7 @@ where
738726
return Err(error);
739727
}
740728
None => {
741-
return Err(Error::new(
742-
ErrorKind::Other,
729+
return Err(Error::other(
743730
"Invalid goto binary input: unexpected end of input",
744731
));
745732
}
@@ -757,8 +744,7 @@ where
757744
}
758745
None => {
759746
// No more bytes left
760-
return Err(Error::new(
761-
ErrorKind::Other,
747+
return Err(Error::other(
762748
"Invalid goto binary input: unexpected end of input",
763749
));
764750
}
@@ -789,8 +775,7 @@ where
789775
match c {
790776
b'S' => {
791777
if sub_done {
792-
return Err(Error::new(
793-
ErrorKind::Other,
778+
return Err(Error::other(
794779
"Invalid goto binary input: incorrect binary structure",
795780
));
796781
}
@@ -816,13 +801,10 @@ where
816801
return Ok(numbered);
817802
}
818803
other => {
819-
return Err(Error::new(
820-
ErrorKind::Other,
821-
format!(
822-
"Invalid goto binary input: unexpected character in input stream {}",
823-
other as char
824-
),
825-
));
804+
return Err(Error::other(format!(
805+
"Invalid goto binary input: unexpected character in input stream {}",
806+
other as char
807+
)));
826808
}
827809
}
828810
}
@@ -877,8 +859,7 @@ where
877859
let shifted_flags = flags >> 16;
878860

879861
if shifted_flags != 0 {
880-
return Err(Error::new(
881-
ErrorKind::Other,
862+
return Err(Error::other(
882863
"incorrect binary format: true bits remain in decoded symbol flags",
883864
));
884865
}
@@ -916,13 +897,10 @@ where
916897
// Read goto binary version
917898
let goto_binary_version = self.read_usize_varenc()?;
918899
if goto_binary_version != 6 {
919-
return Err(Error::new(
920-
ErrorKind::Other,
921-
format!(
922-
"Unsupported GOTO binary version: {}. Supported version: {}",
923-
goto_binary_version, 6
924-
),
925-
));
900+
return Err(Error::other(format!(
901+
"Unsupported GOTO binary version: {}. Supported version: {}",
902+
goto_binary_version, 6
903+
)));
926904
}
927905
Ok(())
928906
}

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

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -150,7 +150,7 @@ impl ProjectedPlace {
150150
goto_expr: Expr,
151151
ty: Ty,
152152
ctx: &mut GotocCtx,
153-
) -> Result<Self, UnimplementedData> {
153+
) -> Result<Self, Box<UnimplementedData>> {
154154
Self::try_new(goto_expr, TypeOrVariant::Type(ty), None, None, ctx)
155155
}
156156

@@ -160,7 +160,7 @@ impl ProjectedPlace {
160160
fat_ptr_goto_expr: Option<Expr>,
161161
fat_ptr_mir_typ: Option<Ty>,
162162
ctx: &mut GotocCtx,
163-
) -> Result<Self, UnimplementedData> {
163+
) -> Result<Self, Box<UnimplementedData>> {
164164
if let Some(fat_ptr) = &fat_ptr_goto_expr {
165165
assert!(
166166
fat_ptr.typ().is_rust_fat_ptr(&ctx.symbol_table),
@@ -183,12 +183,12 @@ impl ProjectedPlace {
183183
if !(expr_ty.is_integer() && ty_from_mir.is_struct_tag()) {
184184
debug_assert!(false, "{}", msg);
185185
}
186-
return Err(UnimplementedData::new(
186+
return Err(Box::new(UnimplementedData::new(
187187
"Projection mismatch",
188188
"https://github.com/model-checking/kani/issues/277",
189189
ty_from_mir,
190190
*goto_expr.location(),
191-
));
191+
)));
192192
}
193193

194194
assert!(
@@ -236,7 +236,7 @@ impl GotocCtx<'_> {
236236
parent_ty_or_var: TypeOrVariant,
237237
field_idx: FieldIdx,
238238
field_ty_or_var: TypeOrVariant,
239-
) -> Result<Expr, UnimplementedData> {
239+
) -> Result<Expr, Box<UnimplementedData>> {
240240
match parent_ty_or_var {
241241
TypeOrVariant::Type(parent_ty) => {
242242
match parent_ty.kind() {
@@ -286,12 +286,12 @@ impl GotocCtx<'_> {
286286
TyKind::RigidTy(RigidTy::CoroutineClosure(def, args)) => {
287287
let typ = Ty::new_coroutine_closure(def, args);
288288
let goto_typ = self.codegen_ty_stable(typ);
289-
Err(UnimplementedData::new(
289+
Err(Box::new(UnimplementedData::new(
290290
"Coroutine closures",
291291
"https://github.com/model-checking/kani/issues/3783",
292292
goto_typ,
293293
*parent_expr.location(),
294-
))
294+
)))
295295
}
296296
TyKind::RigidTy(RigidTy::Str)
297297
| TyKind::RigidTy(RigidTy::Array(_, _))
@@ -414,10 +414,10 @@ impl GotocCtx<'_> {
414414
/// the return value is the expression after.
415415
fn codegen_projection(
416416
&mut self,
417-
before: Result<ProjectedPlace, UnimplementedData>,
417+
before: Result<ProjectedPlace, Box<UnimplementedData>>,
418418
proj: &ProjectionElem,
419419
loc: Location,
420-
) -> Result<ProjectedPlace, UnimplementedData> {
420+
) -> Result<ProjectedPlace, Box<UnimplementedData>> {
421421
let before = before?;
422422
trace!(?before, ?proj, "codegen_projection");
423423
match proj {
@@ -550,12 +550,12 @@ impl GotocCtx<'_> {
550550
let typ = Ty::try_new_array(ty, subarray_len).unwrap();
551551
let goto_typ = self.codegen_ty_stable(typ);
552552
// unimplemented
553-
Err(UnimplementedData::new(
553+
Err(Box::new(UnimplementedData::new(
554554
"Sub-array binding",
555555
"https://github.com/model-checking/kani/issues/707",
556556
goto_typ,
557557
*before.goto_expr.location(),
558-
))
558+
)))
559559
}
560560
TyKind::RigidTy(RigidTy::Slice(_)) => {
561561
let len = if *from_end {
@@ -722,7 +722,7 @@ impl GotocCtx<'_> {
722722
&mut self,
723723
place: &Place,
724724
loc: Location,
725-
) -> Result<ProjectedPlace, UnimplementedData> {
725+
) -> Result<ProjectedPlace, Box<UnimplementedData>> {
726726
debug!(?place, "codegen_place");
727727
let initial_expr = self.codegen_local(place.local, loc);
728728
let initial_typ = TypeOrVariant::Type(self.local_ty_stable(place.local));
@@ -734,12 +734,12 @@ impl GotocCtx<'_> {
734734
.iter()
735735
.fold(initial_projection, |accum, proj| self.codegen_projection(accum, proj, loc));
736736
match result {
737-
Err(data) => Err(UnimplementedData::new(
737+
Err(data) => Err(Box::new(UnimplementedData::new(
738738
&data.operation,
739739
&data.bug_url,
740740
self.codegen_ty_stable(self.place_ty_stable(place)),
741741
data.loc,
742-
)),
742+
))),
743743
_ => result,
744744
}
745745
}
@@ -770,7 +770,7 @@ impl GotocCtx<'_> {
770770
offset: u64,
771771
min_length: u64,
772772
from_end: bool,
773-
) -> Result<ProjectedPlace, UnimplementedData> {
773+
) -> Result<ProjectedPlace, Box<UnimplementedData>> {
774774
match before.mir_typ().kind() {
775775
//TODO, ask on zulip if we can ever have from_end here?
776776
TyKind::RigidTy(RigidTy::Array(elemt, length)) => {

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ use cbmc::goto_program::{DatatypeComponent, Expr, Location, Parameter, Symbol, S
55
use cbmc::utils::aggr_tag;
66
use cbmc::{InternString, InternedString};
77
use rustc_abi::{
8-
BackendRepr::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size,
8+
BackendRepr::SimdVector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size,
99
TagEncoding, TyAndLayout, VariantIdx, Variants,
1010
};
1111
use rustc_ast::ast::Mutability;
@@ -1473,7 +1473,7 @@ impl<'tcx> GotocCtx<'tcx> {
14731473
debug! {"handling simd with layout {:?}", layout};
14741474

14751475
let (element, size) = match layout {
1476-
Vector { element, count } => (element, count),
1476+
SimdVector { element, count } => (element, count),
14771477
_ => unreachable!(),
14781478
};
14791479

‎kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -420,7 +420,7 @@ impl CodegenBackend for GotocCodegenBackend {
420420
let requested_crate_types = &codegen_results.crate_info.crate_types.clone();
421421
let local_crate_name = codegen_results.crate_info.local_crate_name;
422422
// Create the rlib if one was requested.
423-
if requested_crate_types.iter().any(|crate_type| *crate_type == CrateType::Rlib) {
423+
if requested_crate_types.contains(&CrateType::Rlib) {
424424
link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs);
425425
}
426426

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -468,7 +468,7 @@ impl MirVisitor for CheckUninitVisitor {
468468
&& !ptx.is_mutating()
469469
{
470470
let contains_deref_projection =
471-
{ place.projection.iter().any(|elem| *elem == ProjectionElem::Deref) };
471+
{ place.projection.contains(&ProjectionElem::Deref) };
472472
if contains_deref_projection {
473473
// We do not currently support having a deref projection in the same
474474
// place as union field access.

‎rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2025-03-02"
5+
channel = "nightly-2025-03-04"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)