Skip to content

Commit cd4a8aa

Browse files
Upgrade Rust toolchain to 2025-09-19 (#4369)
Relevant upstream PRs: - rust-lang/rust#146664 (Clean up `ty::Dynamic`) - rust-lang/rust#146728 (Clippy subtree update) Resolves: #4368 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: Zyad Hassan <[email protected]>
1 parent 86b37e8 commit cd4a8aa

File tree

8 files changed

+16
-20
lines changed

8 files changed

+16
-20
lines changed

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1437,7 +1437,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
14371437
};
14381438
CharonTy::new(CharonTyKind::Arrow(rb))
14391439
}
1440-
RigidTy::Dynamic(_, _, _) => {
1440+
RigidTy::Dynamic(_, _) => {
14411441
CharonTy::new(CharonTyKind::DynTrait(CharonExistentialPredicate))
14421442
}
14431443
_ => todo!("Not yet implemented RigidTy: {:?}", rigid_ty),

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1145,7 +1145,7 @@ impl GotocCtx<'_, '_> {
11451145
match dst_subt.kind() {
11461146
TyKind::RigidTy(RigidTy::Slice(_))
11471147
| TyKind::RigidTy(RigidTy::Str)
1148-
| TyKind::RigidTy(RigidTy::Dynamic(_, _, _)) => {
1148+
| TyKind::RigidTy(RigidTy::Dynamic(_, _)) => {
11491149
//TODO: this does the wrong thing on Strings/fixme_boxed_str.rs
11501150
// if we cast to slice or string, then we know the source is also a slice or string,
11511151
// so there shouldn't be anything to do

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ use rustc_public::mir::Body;
2525
use rustc_public::mir::mono::Instance as InstanceStable;
2626
use rustc_public::rustc_internal;
2727
use rustc_public::ty::{
28-
Binder, DynKind, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy,
28+
Binder, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy,
2929
Ty as StableTy,
3030
};
3131
use rustc_span::def_id::DefId;
@@ -301,8 +301,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
301301
predictates.extend(
302302
projections.into_iter().map(|proj| proj.map_bound(ExistentialPredicate::Projection)),
303303
);
304-
let rigid =
305-
RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased }, DynKind::Dyn);
304+
let rigid = RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased });
306305

307306
rustc_public::ty::Ty::from_rigid_kind(rigid)
308307
}
@@ -419,7 +418,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
419418
/// We follow the order from the `TyCtxt::COMMON_VTABLE_ENTRIES`.
420419
fn trait_vtable_field_types(&mut self, t: ty::Ty<'tcx>) -> Vec<DatatypeComponent> {
421420
let mut vtable_base = common_vtable_fields(self.trait_vtable_drop_type(t));
422-
if let ty::Dynamic(binder, _, _) = t.kind() {
421+
if let ty::Dynamic(binder, _) = t.kind() {
423422
// The virtual methods on the trait ref. Some auto traits have no methods.
424423
if let Some(principal) = binder.principal() {
425424
let poly = principal.with_self_ty(self.tcx, t);

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
@@ -418,7 +418,7 @@ impl MirVisitor for CheckUninitVisitor {
418418
.rigid()
419419
.expect("should be working with monomorphized code")
420420
{
421-
RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => {
421+
RigidTy::Adt(..) | RigidTy::Dynamic(_, _) => {
422422
self.push_target(MemoryInitOp::SetRef {
423423
operand: Operand::Copy(place.clone()),
424424
value: true,

kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -398,7 +398,7 @@ fn data_bytes_for_ty(
398398
| RigidTy::CoroutineClosure(_, _)
399399
| RigidTy::CoroutineWitness(_, _)
400400
| RigidTy::Foreign(_)
401-
| RigidTy::Dynamic(_, _, _) => Err(LayoutComputationError::UnsupportedType(ty)),
401+
| RigidTy::Dynamic(_, _) => Err(LayoutComputationError::UnsupportedType(ty)),
402402
}
403403
}
404404
FieldsShape::Union(_) => Err(LayoutComputationError::UnionAsField(ty)),

kani-compiler/src/kani_middle/transform/check_values.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1061,7 +1061,7 @@ pub fn ty_validity_per_offset(
10611061
| RigidTy::CoroutineClosure(_, _)
10621062
| RigidTy::CoroutineWitness(_, _)
10631063
| RigidTy::Foreign(_)
1064-
| RigidTy::Dynamic(_, _, _) => Err(format!("Unsupported {ty:?}")),
1064+
| RigidTy::Dynamic(_, _) => Err(format!("Unsupported {ty:?}")),
10651065
}
10661066
}
10671067
FieldsShape::Union(_) | FieldsShape::Array { .. } => {

kani-driver/src/call_cbmc.rs

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -145,27 +145,24 @@ impl KaniSession {
145145
.await)
146146
};
147147

148-
let verification_results = if res.is_err() {
148+
if let Ok(output) = res {
149+
// The timeout wasn't reached
150+
Ok(VerificationResult::from(output?, harness.attributes.should_panic, start_time))
151+
} else {
149152
// An error occurs if the timeout was reached
150153

151154
// Kill the process
152155
cbmc_process.kill().await?;
153156

154-
VerificationResult {
157+
Ok(VerificationResult {
155158
status: VerificationStatus::Failure,
156159
failed_properties: FailedProperties::None,
157160
results: Err(ExitStatus::Timeout),
158161
runtime: start_time.elapsed(),
159162
generated_concrete_test: false,
160163
coverage_results: None,
161-
}
162-
} else {
163-
// The timeout wasn't reached
164-
let output = res.unwrap()?;
165-
VerificationResult::from(output, harness.attributes.should_panic, start_time)
166-
};
167-
168-
Ok(verification_results)
164+
})
165+
}
169166
}
170167

171168
/// "Internal," but also used by call_cbmc_viewer

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-09-18"
5+
channel = "nightly-2025-09-19"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)