From c132b1609ccfa1a4ec5ebb7c15fd0445dd8c3925 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 19 Sep 2025 08:10:25 +0000 Subject: [PATCH 1/4] Upgrade Rust toolchain to 2025-09-19 Relevant upstream PRs: - https://github.com/rust-lang/rust/pull/146664 (Clean up `ty::Dynamic`) - https://github.com/rust-lang/rust/pull/146728 (Clippy subtree update) Resolves: #4368 --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 7 +++---- .../check_uninit/ptr_uninit/uninit_visitor.rs | 2 +- .../transform/check_uninit/ty_layout.rs | 2 +- .../src/kani_middle/transform/check_values.rs | 2 +- kani-driver/src/call_cbmc.rs | 21 ++++++++++--------- rust-toolchain.toml | 2 +- 7 files changed, 19 insertions(+), 19 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 91f99042ccfa..e9b1fe86f54a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1145,7 +1145,7 @@ impl GotocCtx<'_, '_> { match dst_subt.kind() { TyKind::RigidTy(RigidTy::Slice(_)) | TyKind::RigidTy(RigidTy::Str) - | TyKind::RigidTy(RigidTy::Dynamic(_, _, _)) => { + | TyKind::RigidTy(RigidTy::Dynamic(_, _)) => { //TODO: this does the wrong thing on Strings/fixme_boxed_str.rs // if we cast to slice or string, then we know the source is also a slice or string, // so there shouldn't be anything to do diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index cd94168d0244..22c7fe469020 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -25,7 +25,7 @@ use rustc_public::mir::Body; use rustc_public::mir::mono::Instance as InstanceStable; use rustc_public::rustc_internal; use rustc_public::ty::{ - Binder, DynKind, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy, + Binder, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy, Ty as StableTy, }; use rustc_span::def_id::DefId; @@ -301,8 +301,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { predictates.extend( projections.into_iter().map(|proj| proj.map_bound(ExistentialPredicate::Projection)), ); - let rigid = - RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased }, DynKind::Dyn); + let rigid = RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased }); rustc_public::ty::Ty::from_rigid_kind(rigid) } @@ -419,7 +418,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { /// We follow the order from the `TyCtxt::COMMON_VTABLE_ENTRIES`. fn trait_vtable_field_types(&mut self, t: ty::Ty<'tcx>) -> Vec { let mut vtable_base = common_vtable_fields(self.trait_vtable_drop_type(t)); - if let ty::Dynamic(binder, _, _) = t.kind() { + if let ty::Dynamic(binder, _) = t.kind() { // The virtual methods on the trait ref. Some auto traits have no methods. if let Some(principal) = binder.principal() { let poly = principal.with_self_ty(self.tcx, t); diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index af48b0428666..79270d326f18 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -418,7 +418,7 @@ impl MirVisitor for CheckUninitVisitor { .rigid() .expect("should be working with monomorphized code") { - RigidTy::Adt(..) | RigidTy::Dynamic(_, _, _) => { + RigidTy::Adt(..) | RigidTy::Dynamic(_, _) => { self.push_target(MemoryInitOp::SetRef { operand: Operand::Copy(place.clone()), value: true, diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs index ee219114f714..e0b06472a7f1 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs @@ -398,7 +398,7 @@ fn data_bytes_for_ty( | RigidTy::CoroutineClosure(_, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) - | RigidTy::Dynamic(_, _, _) => Err(LayoutComputationError::UnsupportedType(ty)), + | RigidTy::Dynamic(_, _) => Err(LayoutComputationError::UnsupportedType(ty)), } } FieldsShape::Union(_) => Err(LayoutComputationError::UnionAsField(ty)), diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index d992f2749df4..f4652dcb27cd 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -1061,7 +1061,7 @@ pub fn ty_validity_per_offset( | RigidTy::CoroutineClosure(_, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) - | RigidTy::Dynamic(_, _, _) => Err(format!("Unsupported {ty:?}")), + | RigidTy::Dynamic(_, _) => Err(format!("Unsupported {ty:?}")), } } FieldsShape::Union(_) | FieldsShape::Array { .. } => { diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 27f2f3fed725..b336459da455 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -145,27 +145,28 @@ impl KaniSession { .await) }; - let verification_results = if res.is_err() { + if let Ok(output) = res { + // The timeout wasn't reached + Ok(VerificationResult::from( + output.unwrap(), + harness.attributes.should_panic, + start_time, + )) + } else { // An error occurs if the timeout was reached // Kill the process cbmc_process.kill().await?; - VerificationResult { + Ok(VerificationResult { status: VerificationStatus::Failure, failed_properties: FailedProperties::None, results: Err(ExitStatus::Timeout), runtime: start_time.elapsed(), generated_concrete_test: false, coverage_results: None, - } - } else { - // The timeout wasn't reached - let output = res.unwrap()?; - VerificationResult::from(output, harness.attributes.should_panic, start_time) - }; - - Ok(verification_results) + }) + } } /// "Internal," but also used by call_cbmc_viewer diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 5377a788846f..079ec6a9fb30 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-09-18" +channel = "nightly-2025-09-19" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From aabfe5ed816cc3102537c08d80e7eab416477af7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 19 Sep 2025 10:35:50 +0000 Subject: [PATCH 2/4] LLBC back-end --- kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index 60f2e0f6a101..147bc17eda6a 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -1437,7 +1437,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { }; CharonTy::new(CharonTyKind::Arrow(rb)) } - RigidTy::Dynamic(_, _, _) => { + RigidTy::Dynamic(_, _) => { CharonTy::new(CharonTyKind::DynTrait(CharonExistentialPredicate)) } _ => todo!("Not yet implemented RigidTy: {:?}", rigid_ty), From 9e92871aeebe9ac3c7760aa401b56dbf27ee3d42 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 20 Sep 2025 07:38:07 +0200 Subject: [PATCH 3/4] Update kani-driver/src/call_cbmc.rs Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- kani-driver/src/call_cbmc.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index b336459da455..4a8c0d7857a9 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -148,7 +148,7 @@ impl KaniSession { if let Ok(output) = res { // The timeout wasn't reached Ok(VerificationResult::from( - output.unwrap(), + output?, harness.attributes.should_panic, start_time, )) From 45b8c38cbdd8bc3b5a1aa90d6ee6d9eacf08fa4d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 20 Sep 2025 19:43:20 +0000 Subject: [PATCH 4/4] fmt --- kani-driver/src/call_cbmc.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 4a8c0d7857a9..3eeede9f68e4 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -147,11 +147,7 @@ impl KaniSession { if let Ok(output) = res { // The timeout wasn't reached - Ok(VerificationResult::from( - output?, - harness.attributes.should_panic, - start_time, - )) + Ok(VerificationResult::from(output?, harness.attributes.should_panic, start_time)) } else { // An error occurs if the timeout was reached