Skip to content

Commit 1eeade5

Browse files
zhassan-awszhassan-aws
committed
Revert "Update toolchain to 2025-03-04 (model-checking#3927)"
This reverts commit 9ee764f.
1 parent fbcb759 commit 1eeade5

File tree

6 files changed

+65
-43
lines changed

6 files changed

+65
-43
lines changed

‎cprover_bindings/src/irep/goto_binary_serde.rs‎

Lines changed: 45 additions & 23 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, Read, Write};
87+
use std::io::{BufWriter, Bytes, Error, ErrorKind, 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<BufReader<R>>,
560+
bytes: Bytes<R>,
561561

562562
/// Numbering for ireps
563563
numbering: IrepNumbering,
@@ -584,9 +584,8 @@ 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);
588587
GotoBinaryDeserializer {
589-
bytes: buffered_reader.bytes(),
588+
bytes: reader.bytes(),
590589
numbering: IrepNumbering::new(),
591590
string_count: Vec::new(),
592591
string_map: Vec::new(),
@@ -598,9 +597,12 @@ where
598597
/// Returns Err if the found value is not the expected value.
599598
fn expect<T: Eq + std::fmt::Display>(found: T, expected: T) -> io::Result<T> {
600599
if found != expected {
601-
return Err(Error::other(format!(
602-
"Invalid goto binary input: expected {expected} in byte stream, found {found} instead)"
603-
)));
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+
));
604606
}
605607
Ok(found)
606608
}
@@ -658,7 +660,10 @@ where
658660
match self.bytes.next() {
659661
Some(Ok(u)) => Ok(u),
660662
Some(Err(error)) => Err(error),
661-
None => Err(Error::other("Invalid goto binary input: unexpected end of input")),
663+
None => Err(Error::new(
664+
ErrorKind::Other,
665+
"Invalid goto binary input: unexpected end of input",
666+
)),
662667
}
663668
}
664669

@@ -672,7 +677,8 @@ where
672677
match self.bytes.next() {
673678
Some(Ok(u)) => {
674679
if shift >= max_shift {
675-
return Err(Error::other(
680+
return Err(Error::new(
681+
ErrorKind::Other,
676682
"Invalid goto binary input: serialized value is too large to fit in usize",
677683
));
678684
};
@@ -686,7 +692,10 @@ where
686692
return Err(error);
687693
}
688694
None => {
689-
return Err(Error::other("Invalid goto binary input: unexpected end of input"));
695+
return Err(Error::new(
696+
ErrorKind::Other,
697+
"Invalid goto binary input: unexpected end of input",
698+
));
690699
}
691700
}
692701
}
@@ -712,7 +721,10 @@ where
712721
return Ok(numbered);
713722
}
714723
Err(error) => {
715-
return Err(Error::other(error.to_string()));
724+
return Err(Error::new(
725+
ErrorKind::Other,
726+
error.to_string(),
727+
));
716728
}
717729
}
718730
}
@@ -726,7 +738,8 @@ where
726738
return Err(error);
727739
}
728740
None => {
729-
return Err(Error::other(
741+
return Err(Error::new(
742+
ErrorKind::Other,
730743
"Invalid goto binary input: unexpected end of input",
731744
));
732745
}
@@ -744,7 +757,8 @@ where
744757
}
745758
None => {
746759
// No more bytes left
747-
return Err(Error::other(
760+
return Err(Error::new(
761+
ErrorKind::Other,
748762
"Invalid goto binary input: unexpected end of input",
749763
));
750764
}
@@ -775,7 +789,8 @@ where
775789
match c {
776790
b'S' => {
777791
if sub_done {
778-
return Err(Error::other(
792+
return Err(Error::new(
793+
ErrorKind::Other,
779794
"Invalid goto binary input: incorrect binary structure",
780795
));
781796
}
@@ -801,10 +816,13 @@ where
801816
return Ok(numbered);
802817
}
803818
other => {
804-
return Err(Error::other(format!(
805-
"Invalid goto binary input: unexpected character in input stream {}",
806-
other as char
807-
)));
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+
));
808826
}
809827
}
810828
}
@@ -859,7 +877,8 @@ where
859877
let shifted_flags = flags >> 16;
860878

861879
if shifted_flags != 0 {
862-
return Err(Error::other(
880+
return Err(Error::new(
881+
ErrorKind::Other,
863882
"incorrect binary format: true bits remain in decoded symbol flags",
864883
));
865884
}
@@ -897,10 +916,13 @@ where
897916
// Read goto binary version
898917
let goto_binary_version = self.read_usize_varenc()?;
899918
if goto_binary_version != 6 {
900-
return Err(Error::other(format!(
901-
"Unsupported GOTO binary version: {}. Supported version: {}",
902-
goto_binary_version, 6
903-
)));
919+
return Err(Error::new(
920+
ErrorKind::Other,
921+
format!(
922+
"Unsupported GOTO binary version: {}. Supported version: {}",
923+
goto_binary_version, 6
924+
),
925+
));
904926
}
905927
Ok(())
906928
}

‎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, Box<UnimplementedData>> {
153+
) -> Result<Self, 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, Box<UnimplementedData>> {
163+
) -> Result<Self, 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(Box::new(UnimplementedData::new(
186+
return Err(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, Box<UnimplementedData>> {
239+
) -> Result<Expr, 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(Box::new(UnimplementedData::new(
289+
Err(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, Box<UnimplementedData>>,
417+
before: Result<ProjectedPlace, UnimplementedData>,
418418
proj: &ProjectionElem,
419419
loc: Location,
420-
) -> Result<ProjectedPlace, Box<UnimplementedData>> {
420+
) -> Result<ProjectedPlace, 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(Box::new(UnimplementedData::new(
553+
Err(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, Box<UnimplementedData>> {
725+
) -> Result<ProjectedPlace, 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(Box::new(UnimplementedData::new(
737+
Err(data) => Err(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, Box<UnimplementedData>> {
773+
) -> Result<ProjectedPlace, 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::SimdVector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size,
8+
BackendRepr::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size,
99
TagEncoding, TyAndLayout, VariantIdx, Variants,
1010
};
1111
use rustc_ast::ast::Mutability;
@@ -1472,7 +1472,7 @@ impl<'tcx> GotocCtx<'tcx> {
14721472
debug! {"handling simd with layout {:?}", layout};
14731473

14741474
let (element, size) = match layout {
1475-
SimdVector { element, count } => (element, count),
1475+
Vector { element, count } => (element, count),
14761476
_ => unreachable!(),
14771477
};
14781478

‎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.contains(&CrateType::Rlib) {
423+
if requested_crate_types.iter().any(|crate_type| *crate_type == 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.contains(&ProjectionElem::Deref) };
471+
{ place.projection.iter().any(|elem| *elem == 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-05"
5+
channel = "nightly-2025-03-02"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)