Skip to content

Update toolchain to 2025-03-04 #3927

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 7 commits into from
Mar 11, 2025
Merged

Update toolchain to 2025-03-04 #3927

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
ddf6fe5
Update toolchain to 2025-03-03
qinheping Mar 10, 2025
d2256c9
Fix clippy
qinheping Mar 10, 2025
501d154
FIx clippy
qinheping Mar 10, 2025
66bd2a6
Update toolchain to 2025-03-04
qinheping Mar 10, 2025
06baf0b
Fix clippy
qinheping Mar 10, 2025
5564444
Fix clippy error
qinheping Mar 10, 2025
c7b2b47
Merge branch 'main' into toolchain
qinheping Mar 10, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
68 changes: 23 additions & 45 deletions cprover_bindings/src/irep/goto_binary_serde.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ use std::collections::HashMap;
use std::fs::File;
use std::hash::Hash;
use std::io::{self, BufReader};
use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write};
use std::io::{BufWriter, Bytes, Error, Read, Write};
use std::path::Path;

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

/// Numbering for ireps
numbering: IrepNumbering,
Expand All @@ -584,8 +584,9 @@ where
/// Constructor. The reader is moved into this object and cannot be used
/// afterwards.
fn new(reader: R) -> Self {
let buffered_reader = BufReader::new(reader);
GotoBinaryDeserializer {
bytes: reader.bytes(),
bytes: buffered_reader.bytes(),
numbering: IrepNumbering::new(),
string_count: Vec::new(),
string_map: Vec::new(),
Expand All @@ -597,12 +598,9 @@ where
/// Returns Err if the found value is not the expected value.
fn expect<T: Eq + std::fmt::Display>(found: T, expected: T) -> io::Result<T> {
if found != expected {
return Err(Error::new(
ErrorKind::Other,
format!(
"Invalid goto binary input: expected {expected} in byte stream, found {found} instead)"
),
));
return Err(Error::other(format!(
"Invalid goto binary input: expected {expected} in byte stream, found {found} instead)"
)));
}
Ok(found)
}
Expand Down Expand Up @@ -660,10 +658,7 @@ where
match self.bytes.next() {
Some(Ok(u)) => Ok(u),
Some(Err(error)) => Err(error),
None => Err(Error::new(
ErrorKind::Other,
"Invalid goto binary input: unexpected end of input",
)),
None => Err(Error::other("Invalid goto binary input: unexpected end of input")),
}
}

Expand All @@ -677,8 +672,7 @@ where
match self.bytes.next() {
Some(Ok(u)) => {
if shift >= max_shift {
return Err(Error::new(
ErrorKind::Other,
return Err(Error::other(
"Invalid goto binary input: serialized value is too large to fit in usize",
));
};
Expand All @@ -692,10 +686,7 @@ where
return Err(error);
}
None => {
return Err(Error::new(
ErrorKind::Other,
"Invalid goto binary input: unexpected end of input",
));
return Err(Error::other("Invalid goto binary input: unexpected end of input"));
}
}
}
Expand All @@ -721,10 +712,7 @@ where
return Ok(numbered);
}
Err(error) => {
return Err(Error::new(
ErrorKind::Other,
error.to_string(),
));
return Err(Error::other(error.to_string()));
}
}
}
Expand All @@ -738,8 +726,7 @@ where
return Err(error);
}
None => {
return Err(Error::new(
ErrorKind::Other,
return Err(Error::other(
"Invalid goto binary input: unexpected end of input",
));
}
Expand All @@ -757,8 +744,7 @@ where
}
None => {
// No more bytes left
return Err(Error::new(
ErrorKind::Other,
return Err(Error::other(
"Invalid goto binary input: unexpected end of input",
));
}
Expand Down Expand Up @@ -789,8 +775,7 @@ where
match c {
b'S' => {
if sub_done {
return Err(Error::new(
ErrorKind::Other,
return Err(Error::other(
"Invalid goto binary input: incorrect binary structure",
));
}
Expand All @@ -816,13 +801,10 @@ where
return Ok(numbered);
}
other => {
return Err(Error::new(
ErrorKind::Other,
format!(
"Invalid goto binary input: unexpected character in input stream {}",
other as char
),
));
return Err(Error::other(format!(
"Invalid goto binary input: unexpected character in input stream {}",
other as char
)));
}
}
}
Expand Down Expand Up @@ -877,8 +859,7 @@ where
let shifted_flags = flags >> 16;

if shifted_flags != 0 {
return Err(Error::new(
ErrorKind::Other,
return Err(Error::other(
"incorrect binary format: true bits remain in decoded symbol flags",
));
}
Expand Down Expand Up @@ -916,13 +897,10 @@ where
// Read goto binary version
let goto_binary_version = self.read_usize_varenc()?;
if goto_binary_version != 6 {
return Err(Error::new(
ErrorKind::Other,
format!(
"Unsupported GOTO binary version: {}. Supported version: {}",
goto_binary_version, 6
),
));
return Err(Error::other(format!(
"Unsupported GOTO binary version: {}. Supported version: {}",
goto_binary_version, 6
)));
}
Ok(())
}
Expand Down
30 changes: 15 additions & 15 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ impl ProjectedPlace {
goto_expr: Expr,
ty: Ty,
ctx: &mut GotocCtx,
) -> Result<Self, UnimplementedData> {
) -> Result<Self, Box<UnimplementedData>> {
Self::try_new(goto_expr, TypeOrVariant::Type(ty), None, None, ctx)
}

Expand All @@ -160,7 +160,7 @@ impl ProjectedPlace {
fat_ptr_goto_expr: Option<Expr>,
fat_ptr_mir_typ: Option<Ty>,
ctx: &mut GotocCtx,
) -> Result<Self, UnimplementedData> {
) -> Result<Self, Box<UnimplementedData>> {
if let Some(fat_ptr) = &fat_ptr_goto_expr {
assert!(
fat_ptr.typ().is_rust_fat_ptr(&ctx.symbol_table),
Expand All @@ -183,12 +183,12 @@ impl ProjectedPlace {
if !(expr_ty.is_integer() && ty_from_mir.is_struct_tag()) {
debug_assert!(false, "{}", msg);
}
return Err(UnimplementedData::new(
return Err(Box::new(UnimplementedData::new(
"Projection mismatch",
"https://github.com/model-checking/kani/issues/277",
ty_from_mir,
*goto_expr.location(),
));
)));
}

assert!(
Expand Down Expand Up @@ -236,7 +236,7 @@ impl GotocCtx<'_> {
parent_ty_or_var: TypeOrVariant,
field_idx: FieldIdx,
field_ty_or_var: TypeOrVariant,
) -> Result<Expr, UnimplementedData> {
) -> Result<Expr, Box<UnimplementedData>> {
match parent_ty_or_var {
TypeOrVariant::Type(parent_ty) => {
match parent_ty.kind() {
Expand Down Expand Up @@ -286,12 +286,12 @@ impl GotocCtx<'_> {
TyKind::RigidTy(RigidTy::CoroutineClosure(def, args)) => {
let typ = Ty::new_coroutine_closure(def, args);
let goto_typ = self.codegen_ty_stable(typ);
Err(UnimplementedData::new(
Err(Box::new(UnimplementedData::new(
"Coroutine closures",
"https://github.com/model-checking/kani/issues/3783",
goto_typ,
*parent_expr.location(),
))
)))
}
TyKind::RigidTy(RigidTy::Str)
| TyKind::RigidTy(RigidTy::Array(_, _))
Expand Down Expand Up @@ -414,10 +414,10 @@ impl GotocCtx<'_> {
/// the return value is the expression after.
fn codegen_projection(
&mut self,
before: Result<ProjectedPlace, UnimplementedData>,
before: Result<ProjectedPlace, Box<UnimplementedData>>,
proj: &ProjectionElem,
loc: Location,
) -> Result<ProjectedPlace, UnimplementedData> {
) -> Result<ProjectedPlace, Box<UnimplementedData>> {
let before = before?;
trace!(?before, ?proj, "codegen_projection");
match proj {
Expand Down Expand Up @@ -550,12 +550,12 @@ impl GotocCtx<'_> {
let typ = Ty::try_new_array(ty, subarray_len).unwrap();
let goto_typ = self.codegen_ty_stable(typ);
// unimplemented
Err(UnimplementedData::new(
Err(Box::new(UnimplementedData::new(
"Sub-array binding",
"https://github.com/model-checking/kani/issues/707",
goto_typ,
*before.goto_expr.location(),
))
)))
}
TyKind::RigidTy(RigidTy::Slice(_)) => {
let len = if *from_end {
Expand Down Expand Up @@ -722,7 +722,7 @@ impl GotocCtx<'_> {
&mut self,
place: &Place,
loc: Location,
) -> Result<ProjectedPlace, UnimplementedData> {
) -> Result<ProjectedPlace, Box<UnimplementedData>> {
debug!(?place, "codegen_place");
let initial_expr = self.codegen_local(place.local, loc);
let initial_typ = TypeOrVariant::Type(self.local_ty_stable(place.local));
Expand All @@ -734,12 +734,12 @@ impl GotocCtx<'_> {
.iter()
.fold(initial_projection, |accum, proj| self.codegen_projection(accum, proj, loc));
match result {
Err(data) => Err(UnimplementedData::new(
Err(data) => Err(Box::new(UnimplementedData::new(
&data.operation,
&data.bug_url,
self.codegen_ty_stable(self.place_ty_stable(place)),
data.loc,
)),
))),
_ => result,
}
}
Expand Down Expand Up @@ -770,7 +770,7 @@ impl GotocCtx<'_> {
offset: u64,
min_length: u64,
from_end: bool,
) -> Result<ProjectedPlace, UnimplementedData> {
) -> Result<ProjectedPlace, Box<UnimplementedData>> {
match before.mir_typ().kind() {
//TODO, ask on zulip if we can ever have from_end here?
TyKind::RigidTy(RigidTy::Array(elemt, length)) => {
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ use cbmc::goto_program::{DatatypeComponent, Expr, Location, Parameter, Symbol, S
use cbmc::utils::aggr_tag;
use cbmc::{InternString, InternedString};
use rustc_abi::{
BackendRepr::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size,
BackendRepr::SimdVector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size,
TagEncoding, TyAndLayout, VariantIdx, Variants,
};
use rustc_ast::ast::Mutability;
Expand Down Expand Up @@ -1473,7 +1473,7 @@ impl<'tcx> GotocCtx<'tcx> {
debug! {"handling simd with layout {:?}", layout};

let (element, size) = match layout {
Vector { element, count } => (element, count),
SimdVector { element, count } => (element, count),
_ => unreachable!(),
};

Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -420,7 +420,7 @@ impl CodegenBackend for GotocCodegenBackend {
let requested_crate_types = &codegen_results.crate_info.crate_types.clone();
let local_crate_name = codegen_results.crate_info.local_crate_name;
// Create the rlib if one was requested.
if requested_crate_types.iter().any(|crate_type| *crate_type == CrateType::Rlib) {
if requested_crate_types.contains(&CrateType::Rlib) {
link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs);
}

Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -468,7 +468,7 @@ impl MirVisitor for CheckUninitVisitor {
&& !ptx.is_mutating()
{
let contains_deref_projection =
{ place.projection.iter().any(|elem| *elem == ProjectionElem::Deref) };
{ place.projection.contains(&ProjectionElem::Deref) };
if contains_deref_projection {
// We do not currently support having a deref projection in the same
// place as union field access.
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

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