From 37fca44d7e6f259945a4bf0df46a6b031a89a0dd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 8 Jul 2026 07:45:52 +0000 Subject: [PATCH 1/9] Upgrade Rust toolchain to 2025-12-16 Relevant upstream PR: - https://github.com/rust-lang/rust/pull/148602 (misc coercion cleanups and handle safety correctly) Resolves: #4623 --- kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- kani-compiler/src/kani_middle/reachability.rs | 2 +- kani-compiler/src/kani_middle/transform/internal_mir.rs | 4 ++-- rust-toolchain.toml | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index e3a30a8bf3f0..d2b69a36323d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1321,7 +1321,7 @@ impl GotocCtx<'_, '_> { ) -> Expr { debug!(cast=?coercion, op=?operand, ?loc, "codegen_pointer_cast"); match coercion { - PointerCoercion::ReifyFnPointer => match self.operand_ty_stable(operand).kind() { + PointerCoercion::ReifyFnPointer(_) => match self.operand_ty_stable(operand).kind() { TyKind::RigidTy(RigidTy::FnDef(def, args)) => { let instance = Instance::resolve(def, &args).unwrap(); // We need to handle this case in a special way because `codegen_operand_stable` compiles FnDefs to dummy structs. diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 5a7ac9cb44e1..421e4d651ee6 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -349,7 +349,7 @@ impl MirVisitor for MonoItemsFnCollector<'_, '_> { } } Rvalue::Cast( - CastKind::PointerCoercion(PointerCoercion::ReifyFnPointer), + CastKind::PointerCoercion(PointerCoercion::ReifyFnPointer(_)), ref operand, _, ) => { diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index edd016add17c..bd648824f61d 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -101,8 +101,8 @@ impl RustcInternalMir for PointerCoercion { fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { match self { - PointerCoercion::ReifyFnPointer => { - rustc_middle::ty::adjustment::PointerCoercion::ReifyFnPointer + PointerCoercion::ReifyFnPointer(safety) => { + rustc_middle::ty::adjustment::PointerCoercion::ReifyFnPointer(internal(tcx, safety)) } PointerCoercion::UnsafeFnPointer => { rustc_middle::ty::adjustment::PointerCoercion::UnsafeFnPointer diff --git a/rust-toolchain.toml b/rust-toolchain.toml index fc2945d6422c..c34160a74acf 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-12-05" +channel = "nightly-2025-12-16" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From c31896af4f3d278458a76f615628e9b828f03fc9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 8 Jul 2026 10:52:29 +0000 Subject: [PATCH 2/9] Keep crate-relative item names in output after rust-lang/rust#149401 rust-lang/rust#149401 fixed rustc_public's `Instance::name()` (and `CrateItem::name()`) to return the true absolute path, which now includes the crate name for *local* items too (e.g. `my_crate::my_fn` instead of `my_fn`, and `::m` instead of `::m`). Kani feeds these names into user-facing output ("Checking harness ...", "Verification failed for - ...", stubbing diagnostics) and into CBMC symbol pretty-names ("in function ..."), so the bump to nightly-2025-12-16 made ~160 `expected` tests fail on the newly crate-qualified names. Add `strip_local_crate_prefix` (and the `readable_name` wrapper) in kani_middle, which removes the local crate name at each path-component *qualifier* position (start, or after a delimiter such as `<`, `,`, ` `), while preserving continuation segments after `::` so a module/item that shares the crate's name (e.g. crate `main` with `fn main`) is not over-stripped. Non-local paths (`std::...`) are unaffected. Apply it at the harness pretty-name, function/static symbol pretty-name, current-function readable name, and the two stubbing diagnostics. Co-authored-by: Kiro --- .../codegen_cprover_gotoc/codegen/function.rs | 3 +- .../codegen/static_var.rs | 4 +- .../context/current_fn.rs | 2 +- kani-compiler/src/kani_middle/metadata.rs | 6 +- kani-compiler/src/kani_middle/mod.rs | 59 ++++++++++++++++++- kani-compiler/src/kani_middle/stubbing/mod.rs | 6 +- 6 files changed, 69 insertions(+), 11 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index a244d37366e2..8f4af7f06bd1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -5,6 +5,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder; +use crate::kani_middle::readable_name; use cbmc::InternString; use cbmc::InternedString; use cbmc::goto_program::{Expr, Stmt, Symbol}; @@ -220,7 +221,7 @@ impl GotocCtx<'_, '_> { &fname, self.fn_typ(instance, &body), None, - instance.name(), + readable_name(instance), self.codegen_span_stable(instance.def.span()), ); if !self.symbol_table.contains((&fname).into()) { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs index ab99c6e79c52..fa74a01b24b7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -4,7 +4,7 @@ //! This file contains functions related to codegenning MIR static variables into gotoc use crate::codegen_cprover_gotoc::GotocCtx; -use crate::kani_middle::is_interior_mut; +use crate::kani_middle::{is_interior_mut, readable_name}; use rustc_public::CrateDef; use rustc_public::mir::mono::{Instance, StaticDef}; use tracing::debug; @@ -34,7 +34,7 @@ impl GotocCtx<'_, '_> { // Unique mangled monomorphized name. let symbol_name = instance.mangled_name(); // Pretty name which may include function name. - let pretty_name = instance.name(); + let pretty_name = readable_name(instance); debug!(?def, ?symbol_name, ?pretty_name, "declare_static"); let typ = self.codegen_ty_stable(instance.ty()); diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs index 7a2be6b06c5a..4be054daf34f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -58,7 +58,7 @@ impl MirVisitor for AddressTakenLocalsCollector { impl<'tcx> CurrentFnCtx<'tcx> { pub fn new(instance: Instance, gcx: &GotocCtx<'tcx, '_>, body: &Body) -> Self { let instance_internal = rustc_internal::internal(gcx.tcx, instance); - let readable_name = instance.name(); + let readable_name = crate::kani_middle::readable_name(instance); let name = instance.mangled_name(); let locals = body.locals().to_vec(); let local_names = body diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index d4c395a2a1a3..d5fe8f595fb1 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -7,7 +7,7 @@ use std::collections::HashMap; use std::path::Path; use crate::kani_middle::codegen_units::Harness; -use crate::kani_middle::{KaniAttributes, SourceLocation}; +use crate::kani_middle::{KaniAttributes, SourceLocation, readable_name}; use kani_metadata::ContractedFunction; use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; use rustc_middle::ty::TyCtxt; @@ -20,7 +20,7 @@ use sha1_checked::Sha1; pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata { let def = instance.def; let kani_attributes = KaniAttributes::for_instance(tcx, instance); - let pretty_name = instance.name(); + let pretty_name = readable_name(instance); let mangled_name = instance.mangled_name(); // We get the body span to include the entire function definition. @@ -119,7 +119,7 @@ pub fn gen_automatic_proof_metadata( harness_mangled_name: String, ) -> HarnessMetadata { let def = fn_to_verify.def; - let pretty_name = fn_to_verify.name(); + let pretty_name = readable_name(*fn_to_verify); let mangled_name = fn_to_verify.mangled_name(); // Leave the concrete playback instrumentation for now, but this feature does not actually support concrete playback. diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 9e4d8026a055..2e3408908450 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -16,11 +16,68 @@ use rustc_public::ty::{ AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyKind, }; use rustc_public::visitor::{Visitable, Visitor as TyVisitor}; -use rustc_public::{CrateDef, DefId}; +use rustc_public::{CrateDef, DefId, local_crate}; use std::ops::ControlFlow; use self::attributes::KaniAttributes; +/// Return an item's name for user-facing output and CBMC symbol pretty-names. +/// +/// [`Instance::name`] returns the item's absolute path. As of +/// rust-lang/rust#149401 that path includes the crate name for *local* items +/// too (e.g. `my_crate::my_fn` instead of `my_fn`). Kani's user-facing output +/// ("Checking harness ...", "Verification failed for - ...") and the CBMC +/// symbol pretty-names ("in function ...") historically used the crate-relative +/// form, and tests and users rely on it, so strip the local crate prefix. +/// Non-local items (e.g. `std::...`) keep their fully-qualified names. +pub fn readable_name(instance: Instance) -> String { + strip_local_crate_prefix(instance.name()) +} + +/// Strip the local crate name from an absolute item path, restoring the +/// crate-relative form Kani used before rust-lang/rust#149401. That change made +/// `def_path_str` prefix the local crate name at *every* local path component, +/// so it appears not just at the start (`my_crate::f`) but also inside +/// qualifiers and generic args (`::m`, +/// `f::`). Remove `::` at each path-component boundary +/// (start of string or after a non-identifier char) so these become `f`, +/// `::m`, `f::`. Non-local paths (which begin with a different +/// crate name) are unaffected. +pub fn strip_local_crate_prefix(name: String) -> String { + let needle = format!("{}::", local_crate().name); + if !name.contains(&needle) { + return name; + } + let mut out = String::with_capacity(name.len()); + let mut rest = name.as_str(); + // The previous char in the input, used to decide whether a `::` here + // is a crate-root *qualifier* (droppable) or a path *continuation* segment + // (a module/item that happens to share the crate's name, which must be + // kept). A qualifier appears at the start or after a type/path delimiter + // (`<`, `,`, ` `, `&`, `*`, `(`, `[`, ...); a continuation appears after + // `::`. So drop `::` only when the previous char is neither part of + // an identifier nor `:`. After dropping, pretend the previous char is `:` + // so an immediately following same-named segment is treated as a + // continuation (e.g. `main::main::{closure#0}` -> `main::{closure#0}`). + let mut prev: Option = None; + loop { + let at_qualifier = match prev { + None => true, + Some(c) => !c.is_alphanumeric() && c != '_' && c != ':', + }; + if at_qualifier && rest.starts_with(&needle) { + rest = &rest[needle.len()..]; + prev = Some(':'); + continue; + } + let Some(ch) = rest.chars().next() else { break }; + out.push(ch); + prev = Some(ch); + rest = &rest[ch.len_utf8()..]; + } + out +} + pub mod abi; pub mod analysis; pub mod attributes; diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index f7d1794de5dd..27df6e7ef760 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -208,8 +208,8 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul if !diff.is_empty() { Err(format!( "Cannot stub `{}` by `{}`.\n - {}", - old_def.name(), - new_def.name(), + crate::kani_middle::strip_local_crate_prefix(old_def.name()), + crate::kani_middle::strip_local_crate_prefix(new_def.name()), diff.iter().join("\n - ") )) } else { @@ -291,7 +291,7 @@ impl MirVisitor for StubConstChecker<'_> { This is likely because `{}` is used as a stub but its \ generic bounds are not being met.", tcx.def_path_str(trait_), - self.source.name() + crate::kani_middle::strip_local_crate_prefix(self.source.name()) ); tcx.dcx().span_err(rustc_internal::internal(self.tcx, location.span()), msg); self.is_valid = false; From 4a6628b144be596582a64d45995cf77dd8bb8d0b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 8 Jul 2026 12:52:29 +0000 Subject: [PATCH 3/9] Update pointer_generator_error expected output for new macro diagnostics rust-lang/rust#148717 ("Point at span within local macros even when error happens in nested external macro") changed how macro-originated errors are rendered, so the E0080 const-eval error for `PointerGenerator::<0>` now points at different spans and adds a "this error originates in the macro ..." note. Replace the brittle consecutive-line block with the stable, essential lines (the E0080 message, the failing const, the instantiation note, and the offending call), which still assert the misuse fails to compile while being robust to future diagnostic reformatting. Co-authored-by: Kiro --- .../ptrs/pointer_generator_error.expected | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/tests/expected/arbitrary/ptrs/pointer_generator_error.expected b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected index 836af138165c..1c3ecb86b218 100644 --- a/tests/expected/arbitrary/ptrs/pointer_generator_error.expected +++ b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected @@ -1,12 +1,4 @@ -error[E0080]: evaluation panicked: PointerGenerator requires at least one byte.\ - -|\ -| kani_core::kani_lib!(kani);\ -| ^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation of `kani::PointerGenerator::<0>::VALID` failed here\ -|\ - -note: the above error was encountered while instantiating `fn kani::PointerGenerator::<0>::new`\ -pointer_generator_error.rs\ -|\ -| let _generator = PointerGenerator::<0>::new();\ -| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +error[E0080]: evaluation panicked: PointerGenerator requires at least one byte. +evaluation of `kani::PointerGenerator::<0>::VALID` failed here +note: the above error was encountered while instantiating `fn kani::PointerGenerator::<0>::new` +let _generator = PointerGenerator::<0>::new(); From 2f5f3a8ebf2cbe06384bfd50a6e694dcd2fb97d1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 8 Jul 2026 13:48:02 +0000 Subject: [PATCH 4/9] Strip crate prefix from recursion-tracker --nondet-static-exclude The contract-recursion tests (e.g. generic_infinity_recursion, gcd_rec_simple_pass) regressed on nightly-2025-12-16: the recursive-call precondition was spuriously falsifiable. Root cause is the same rust-lang/rust#149401 name change: `find_recursion_tracker` builds the `--nondet-static-exclude` value from `static_item.name()`, which is now crate-qualified (`t::foo::{closure#0}::REENTRY`). CBMC matches that value against the static's crate-relative pretty name, so the qualified value no longer matches, `REENTRY` is not excluded from `--nondet-static`, and the recursion tracker is havocked to a nondet value. With `REENTRY` nondet the top-level contract call can take the REPLACE path (which *asserts* the precondition) instead of the CHECK path (which *assumes* it), so the precondition fails on a nondet input. Strip the local crate prefix here too (matching `readable_name`), restoring the match. Verified: the full `expected` suite is green again. Co-authored-by: Kiro --- .../src/codegen_cprover_gotoc/codegen/contract.rs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index d5ce11ee4918..ceefcde12700 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -70,7 +70,14 @@ impl GotocCtx<'_, '_> { Some(format!( "{}:{}", loc.filename().expect("recursion location wrapper should have a file name"), - static_item.name(), + // The `--nondet-static-exclude` value must match the static's + // pretty name in the goto model. Since rust-lang/rust#149401, + // `name()` is crate-qualified for local items, but the pretty + // name is kept crate-relative (see `readable_name`), so strip + // the crate prefix here too; otherwise the recursion tracker + // `REENTRY` is not excluded from `--nondet-static` and gets + // havocked, breaking contract-recursion checking. + crate::kani_middle::strip_local_crate_prefix(static_item.name()), )) } else { None From afa61ca8599e14c3140cfeebb939db89c36f738e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 8 Jul 2026 14:49:40 +0000 Subject: [PATCH 5/9] Upgrade Rust toolchain to nightly-2025-12-31 Adapt kani-compiler to the rustc/rustc_public API changes in this window: - rust-lang/rust#148766 (mir-const-runtime-checks): `Rvalue::NullaryOp` and `NullOp` were removed; `SizeOf`/`AlignOf`/`OffsetOf` become `mir::ConstValue` and the `ub_checks`/`contract_checks`/`overflow_checks` flags move to a new `Operand::RuntimeChecks(RuntimeChecks)`. Drop the `NullaryOp` match arms and handle `Operand::RuntimeChecks` everywhere `Operand` is matched (codegen it to `false`, as the old `NullOp::RuntimeChecks` was; treat it as a no-op in the points-to / uninit / MIR-internalization visitors). - rust-lang/rust#150116: `FieldsShape::Arbitrary::memory_index` renamed to `in_memory_order` (Kani only uses its length). - New `ValueAbi::ScalableVector` variant handled in the valid-value analysis. - rust-lang/rust#6d6068f6c5b (stabilize annotate-snippet): `HumanReadableErrorType` became a struct `{ short, unicode }` instead of an enum with a `Default` variant. Main suites pass on 12-31: expected (458), ui (144), kani (589), 0 failures. Co-authored-by: Kiro --- .../codegen_cprover_gotoc/codegen/operand.rs | 5 +++ .../codegen_cprover_gotoc/codegen/rvalue.rs | 3 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 4 +-- kani-compiler/src/kani_middle/analysis.rs | 1 - .../points_to/points_to_analysis.rs | 7 +++- .../src/kani_middle/transform/body.rs | 1 - .../delayed_ub/initial_target_visitor.rs | 2 ++ .../check_uninit/relevant_instruction.rs | 4 +-- .../src/kani_middle/transform/check_values.rs | 2 +- .../src/kani_middle/transform/internal_mir.rs | 32 +++++++------------ kani-compiler/src/session.rs | 2 +- rust-toolchain.toml | 2 +- 12 files changed, 32 insertions(+), 33 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 07542322fa51..ca382c1fc080 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -56,6 +56,11 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { Operand::Constant(constant) => { self.codegen_const(&constant.const_, self.codegen_span_stable(constant.span)) } + // Runtime checks (`ub_checks()`, `contract_checks()`, `overflow_checks()`) were + // moved from `Rvalue::NullaryOp(NullOp::RuntimeChecks(..))` to `Operand::RuntimeChecks` + // by rust-lang/rust#148766. Kani does not enable these source-level checks (it inserts + // its own), so evaluate them to `false` as before. + Operand::RuntimeChecks(_) => Expr::c_false(), } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index d2b69a36323d..d5fdf85db63c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -23,7 +23,7 @@ use rustc_middle::ty::{TyCtxt, VtblEntry}; use rustc_public::abi::{Primitive, Scalar, ValueAbi}; use rustc_public::mir::mono::Instance; use rustc_public::mir::{ - AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp, + AggregateKind, BinOp, CastKind, Operand, Place, PointerCoercion, Rvalue, UnOp, }; use rustc_public::rustc_internal; use rustc_public::ty::{ @@ -824,7 +824,6 @@ impl GotocCtx<'_, '_> { Rvalue::CheckedBinaryOp(op, e1, e2) => { self.codegen_rvalue_checked_binary_op(op, e1, e2, res_ty) } - Rvalue::NullaryOp(NullOp::RuntimeChecks(_)) => Expr::c_false(), Rvalue::ShallowInitBox(operand, content_ty) => { // The behaviour of ShallowInitBox is simply transmuting *mut u8 to Box. // See https://github.com/rust-lang/compiler-team/issues/460 for more details. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index ce027e53da22..ca32a86a1169 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -771,9 +771,9 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { initial_offset: Size, ) -> Vec { match &layout.fields { - FieldsShape::Arbitrary { offsets, memory_index } => { + FieldsShape::Arbitrary { offsets, in_memory_order } => { assert_eq!(flds.len(), offsets.len()); - assert_eq!(offsets.len(), memory_index.len()); + assert_eq!(offsets.len(), in_memory_order.len()); let mut final_fields = Vec::with_capacity(flds.len()); let mut offset = initial_offset; for idx in layout.fields.index_by_increasing_offset() { diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index bccf143c09b4..6fc1326e33e2 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -168,7 +168,6 @@ impl From<&Rvalue> for Key { Rvalue::Cast(_, _, _) => Key("Cast"), Rvalue::BinaryOp(..) => Key("BinaryOp"), Rvalue::CheckedBinaryOp(..) => Key("CheckedBinaryOp"), - Rvalue::NullaryOp(_) => Key("NullaryOp"), Rvalue::UnaryOp(_, _) => Key("UnaryOp"), Rvalue::Discriminant(_) => Key("Discriminant"), Rvalue::Aggregate(_, _) => Key("Aggregate"), diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 7e752da9e471..c3735da81a76 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -402,6 +402,8 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { HashSet::new() } } + // Runtime-check operands (rust-lang/rust#148766) reference no place or static. + Operand::RuntimeChecks(..) => HashSet::new(), } } @@ -424,6 +426,8 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { HashSet::new() } } + // Runtime-check operands (rust-lang/rust#148766) reference no place or static. + Operand::RuntimeChecks(..) => HashSet::new(), } } @@ -452,6 +456,7 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { .join(&state.transitive_closure(state.resolve_place(place, self.instance))); } Operand::Constant(_) => {} + Operand::RuntimeChecks(_) => {} } } @@ -581,7 +586,7 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { // The same story from BinOp applies here, too. Need to track those things. self.successors_for_operand(state, operand) } - Rvalue::NullaryOp(..) | Rvalue::Discriminant(..) => { + Rvalue::Discriminant(..) => { // All of those should yield a constant. HashSet::new() } diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 277f49f8ed14..9d36caadcd73 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -632,7 +632,6 @@ pub trait MutMirVisitor { Rvalue::CopyForDeref(_) | Rvalue::Discriminant(_) | Rvalue::Len(_) => {} Rvalue::Ref(..) => {} Rvalue::ThreadLocalRef(_) => {} - Rvalue::NullaryOp(..) => {} } } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs index 1677b930c722..98bf834e74da 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs @@ -56,6 +56,8 @@ impl InitialTargetVisitor { } } } + // Runtime-check operands (rust-lang/rust#148766) carry no place or static. + Operand::RuntimeChecks(_) => {} } } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs index ed210e26c87a..d7468526e2af 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs @@ -121,7 +121,7 @@ impl MemoryInitOp { | MemoryInitOp::StoreArgument { operand, .. } => { let place = match operand { Operand::Copy(place) | Operand::Move(place) => place, - Operand::Constant(_) => unreachable!(), + Operand::Constant(_) | Operand::RuntimeChecks(_) => unreachable!(), }; let rvalue = Rvalue::AddressOf(RawPtrKind::Const, place.clone()); rvalue.ty(body.locals()).unwrap() @@ -269,7 +269,7 @@ fn mk_ref( let ref_local = { let place = match operand { Operand::Copy(place) | Operand::Move(place) => place, - Operand::Constant(_) => unreachable!(), + Operand::Constant(_) | Operand::RuntimeChecks(_) => unreachable!(), }; let rvalue = Rvalue::AddressOf(RawPtrKind::Const, place.clone()); let ret_ty = rvalue.ty(body.locals()).unwrap(); diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 0abec3891f90..9385cf5acc2d 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -214,6 +214,7 @@ impl ValidValueReq { ValueAbi::Scalar(_) | ValueAbi::ScalarPair(_, _) | ValueAbi::Vector { .. } + | ValueAbi::ScalableVector { .. } | ValueAbi::Aggregate { .. } => None, } } @@ -699,7 +700,6 @@ impl MirVisitor for CheckValueVisitor<'_, '_> { | Rvalue::Ref(_, _, _) | Rvalue::Repeat(_, _) | Rvalue::ThreadLocalRef(_) - | Rvalue::NullaryOp(_) | Rvalue::UnaryOp(_, _) | Rvalue::Use(_) => {} } diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index bd648824f61d..416fccdf2f3e 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -12,9 +12,9 @@ use rustc_middle::ty::{self as rustc_ty, TyCtxt}; use rustc_public::mir::{ AggregateKind, AssertMessage, Body, BorrowKind, CastKind, ConstOperand, CopyNonOverlapping, CoroutineDesugaring, CoroutineKind, CoroutineSource, FakeBorrowKind, FakeReadCause, LocalDecl, - MutBorrowKind, NonDivergingIntrinsic, NullOp, Operand, PointerCoercion, RetagKind, - RuntimeChecks, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, - UnwindAction, UserTypeProjection, Variance, + MutBorrowKind, NonDivergingIntrinsic, Operand, PointerCoercion, RetagKind, RuntimeChecks, + Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, UnwindAction, + UserTypeProjection, Variance, }; use rustc_public::rustc_internal::internal; @@ -92,6 +92,9 @@ impl RustcInternalMir for Operand { Operand::Constant(const_operand) => { rustc_middle::mir::Operand::Constant(Box::new(const_operand.internal_mir(tcx))) } + Operand::RuntimeChecks(runtime_checks) => { + rustc_middle::mir::Operand::RuntimeChecks(runtime_checks.internal_mir(tcx)) + } } } } @@ -190,24 +193,14 @@ impl RustcInternalMir for BorrowKind { } } -impl RustcInternalMir for NullOp { - type T<'tcx> = rustc_middle::mir::NullOp; +impl RustcInternalMir for RuntimeChecks { + type T<'tcx> = rustc_middle::mir::RuntimeChecks; fn internal_mir<'tcx>(&self, _tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { match self { - NullOp::RuntimeChecks(RuntimeChecks::UbChecks) => { - rustc_middle::mir::NullOp::RuntimeChecks(rustc_middle::mir::RuntimeChecks::UbChecks) - } - NullOp::RuntimeChecks(RuntimeChecks::ContractChecks) => { - rustc_middle::mir::NullOp::RuntimeChecks( - rustc_middle::mir::RuntimeChecks::ContractChecks, - ) - } - NullOp::RuntimeChecks(RuntimeChecks::OverflowChecks) => { - rustc_middle::mir::NullOp::RuntimeChecks( - rustc_middle::mir::RuntimeChecks::OverflowChecks, - ) - } + RuntimeChecks::UbChecks => rustc_middle::mir::RuntimeChecks::UbChecks, + RuntimeChecks::ContractChecks => rustc_middle::mir::RuntimeChecks::ContractChecks, + RuntimeChecks::OverflowChecks => rustc_middle::mir::RuntimeChecks::OverflowChecks, } } } @@ -264,9 +257,6 @@ impl RustcInternalMir for Rvalue { Rvalue::ThreadLocalRef(crate_item) => { rustc_middle::mir::Rvalue::ThreadLocalRef(internal(tcx, crate_item.0)) } - Rvalue::NullaryOp(null_op) => { - rustc_middle::mir::Rvalue::NullaryOp(null_op.internal_mir(tcx)) - } Rvalue::UnaryOp(un_op, operand) => { rustc_middle::mir::Rvalue::UnaryOp(internal(tcx, un_op), operand.internal_mir(tcx)) } diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 13c6d93b0bd9..386a54c020d6 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -59,7 +59,7 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + Some(Arc::new(SourceMap::new(FilePathMapping::empty()))), default_translator(), false, - HumanReadableErrorType::Default { short: false }, + HumanReadableErrorType { short: false, unicode: false }, ColorConfig::Never, ); let registry = ErrorRegistry::new(&[]); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c34160a74acf..195861087b3b 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-12-16" +channel = "nightly-2025-12-31" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 5f569e5634dfb7da4cdacde8e0deb7d199a95a09 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 8 Jul 2026 14:49:51 +0000 Subject: [PATCH 6/9] Strip crate prefix from remaining stubbing diagnostics Extend the rust-lang/rust#149401 crate-prefix stripping (`strip_local_crate_prefix` / `readable_name`) to the stubbing validation error messages that still emitted crate-qualified item names, which broke the `ui` stubbing tests: the arity- and generic-parameter-mismatch errors, the trait-mismatch ("cannot be stubbed by") error, the "does not have a body" resolution notes, and the "stub verified target ... does not have a corresponding proof_for_contract harness" error. The `ui` suite is green again (144 passed, 0 failed). Co-authored-by: Kiro --- kani-compiler/src/kani_middle/attributes.rs | 4 ++-- kani-compiler/src/kani_middle/mod.rs | 2 +- kani-compiler/src/kani_middle/stubbing/mod.rs | 8 ++++---- kani-compiler/src/kani_middle/transform/stubs.rs | 6 +++--- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 66ffa8d27782..d350f2a6c6ef 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -833,7 +833,7 @@ impl<'tcx> KaniAttributes<'tcx> { rustc_internal::internal(self.tcx, original_res.span()), format!( "`{}` does not have a body", - original_res.name() + crate::kani_middle::strip_local_crate_prefix(original_res.name()) )); } if r_bad { @@ -841,7 +841,7 @@ impl<'tcx> KaniAttributes<'tcx> { rustc_internal::internal(self.tcx, replace_res.span()), format!( "`{}` does not have a body", - replace_res.name() + crate::kani_middle::strip_local_crate_prefix(replace_res.name()) )); } err = err.with_help( diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 2e3408908450..2f7aedf59663 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -131,7 +131,7 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { span, format!( "stub verified target `{}` does not have a corresponding `#[proof_for_contract]` harness", - stub_verified_target.name() + strip_local_crate_prefix(stub_verified_target.name()) ), ).with_help("verified stubs are meant to be sound abstractions for a function's behavior, so Kani enforces that proofs exist for the stub's contract") .emit(); diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 27df6e7ef760..e037f6c907c3 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -84,9 +84,9 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul if old_body.arg_locals().len() != new_body.arg_locals().len() { let msg = format!( "arity mismatch: original function/method `{}` takes {} argument(s), stub `{}` takes {}", - old_def.name(), + crate::kani_middle::strip_local_crate_prefix(old_def.name()), old_body.arg_locals().len(), - new_def.name(), + crate::kani_middle::strip_local_crate_prefix(new_def.name()), new_body.arg_locals().len(), ); return Err(msg); @@ -110,9 +110,9 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul if old_args_len != new_args_len { let msg = format!( "mismatch in the number of generic parameters: original function/method `{}` takes {} generic parameters(s), stub `{}` takes {}", - old_def.name(), + crate::kani_middle::strip_local_crate_prefix(old_def.name()), old_args_len, - new_def.name(), + crate::kani_middle::strip_local_crate_prefix(new_def.name()), new_args_len, ); return Err(msg); diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index 1c033b0d6ad8..f8e4a656199d 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -163,7 +163,7 @@ impl MirVisitor for FnStubValidator<'_, '_> { && Instance::resolve(def, &args).is_err() { self.is_valid = false; - let callee = def.name(); + let callee = crate::kani_middle::strip_local_crate_prefix(def.name()); let receiver_ty = args.0[0].expect_ty(); let sep = callee.rfind("::").unwrap(); let trait_ = &callee[..sep]; @@ -173,8 +173,8 @@ impl MirVisitor for FnStubValidator<'_, '_> { "type `{receiver_ty}` doesn't implement trait `{trait_}`, \ so `{}` cannot be stubbed by `{}`. \ All trait bounds of the stub must be satisfied by the original's call sites.", - self.stub.0.name(), - self.stub.1.name(), + crate::kani_middle::strip_local_crate_prefix(self.stub.0.name()), + crate::kani_middle::strip_local_crate_prefix(self.stub.1.name()), ), ); } From 17b187031451b4b1a34b60f9e865fb1c357fbe71 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 8 Jul 2026 20:11:59 +0000 Subject: [PATCH 7/9] Fix 12-31 CI: clippy, LLBC backend, and stub-cycle diagnostic Three follow-ups from the nightly-2025-12-31 bump surfaced by CI: - clippy `result_large_err` on `ensure_non_empty_span`: the `Err` type is rustc's `SpanSnippetError`, which grew and now trips the lint. `#[allow]` it (we can't shrink an upstream type). - LLBC backend (`--features llbc`, not built in the default job): its `translate_operand` needs an arm for the new `Operand::RuntimeChecks` (rust-lang/rust#148766); left as `todo!()` like the backend's other unmodeled cases. - The stub-cycle error ("Stub configuration for harness `..` has a cycle") also embedded a crate-qualified harness name (rust-lang/rust#149401); strip it, fixing cargo-kani/stubbing-double-extern-path. Co-authored-by: Kiro --- kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 3 +++ .../src/codegen_cprover_gotoc/codegen/source_region.rs | 3 +++ kani-compiler/src/kani_middle/codegen_units.rs | 2 +- 3 files changed, 7 insertions(+), 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 22800b2e3b67..b912e91097f0 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 @@ -1708,6 +1708,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> { Operand::Constant(constant) => CharonOperand::Const(self.translate_constant(constant)), Operand::Copy(place) => CharonOperand::Copy(self.translate_place(&place)), Operand::Move(place) => CharonOperand::Move(self.translate_place(&place)), + // `Operand::RuntimeChecks` (rust-lang/rust#148766) is not yet modeled by the + // experimental LLBC backend. + Operand::RuntimeChecks(_) => todo!(), } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs index 19cb2a7aeb01..39cf8281f733 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs @@ -26,6 +26,9 @@ impl Debug for SourceRegion { } } +// The `Err` type of `span_to_source`'s callback is rustc's `SpanSnippetError`, +// which clippy now flags as large; we cannot shrink it, so allow the lint. +#[allow(clippy::result_large_err)] fn ensure_non_empty_span(source_map: &SourceMap, span: Span) -> Option { if !span.is_empty() { return Some(span); diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 6686c2b219de..aadbaca8b4fe 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -301,7 +301,7 @@ fn apply_transitivity(tcx: TyCtxt, harness: Harness, stubs: Stubs) -> Stubs { format!( "Cannot stub `{}`. Stub configuration for harness `{}` has a cycle", orig.name(), - harness.def.name(), + crate::kani_middle::strip_local_crate_prefix(harness.def.name()), ), ); break; From 53422c152d4474920e19202745e1fce2a615379c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 9 Jul 2026 08:09:06 +0000 Subject: [PATCH 8/9] Fix 12-31 autoharness/list diagnostics for crate-qualified names rust-lang/rust#149401 made `name()` crate-qualify local items, which broke the autoharness and `list` features: - metadata.rs: the automatic-contract-harness lookup matched the (now crate-relative) harness `target_fn` against the fully-qualified `ContractedFunction.function`, panicking on the `.unwrap()`. Store all contract/harness names crate-relative so display and lookup are consistent. - codegen_units.rs: strip the crate prefix from the autoharness `chosen` and `skipped` function names (the `Selected Function` list column), and from the autoharness filter name, which #149401 had made doubly crate-qualified (`crate::crate::fn`). Fixes the script-based-pre autoharness/list/autoderive regression tests. Co-authored-by: Kiro --- kani-compiler/src/kani_middle/codegen_units.rs | 14 +++++++++++--- kani-compiler/src/kani_middle/metadata.rs | 18 +++++++++++------- 2 files changed, 22 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index aadbaca8b4fe..4b9236c5d45c 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -106,7 +106,10 @@ impl CodegenUnits { ); AUTOHARNESS_MD .set(AutoHarnessMetadata { - chosen: chosen.iter().map(|func| func.name()).collect::>(), + chosen: chosen + .iter() + .map(|func| crate::kani_middle::strip_local_crate_prefix(func.name())) + .collect::>(), skipped, }) .expect("Initializing the autoharness metadata failed"); @@ -452,7 +455,12 @@ fn automatic_harness_partition( } // Preprend the crate name so that users can filter out entire crates using the existing function filter flags. - let name = format!("{crate_name}::{}", instance.name()); + // `instance.name()` is already crate-qualified for local items (rust-lang/rust#149401), + // so strip that prefix first to avoid double-qualifying (`crate::crate::fn`). + let name = format!( + "{crate_name}::{}", + crate::kani_middle::strip_local_crate_prefix(instance.name()) + ); let body = instance.body().unwrap(); if is_proof_harness(tcx, instance) @@ -503,7 +511,7 @@ fn automatic_harness_partition( for func in crate_fns { if let Some(reason) = skip_reason(func) { - skipped.insert(func.name(), reason); + skipped.insert(crate::kani_middle::strip_local_crate_prefix(func.name()), reason); } else { chosen.push(Instance::try_from(func).unwrap()); } diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index d5fe8f595fb1..d2348ab7b132 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -7,7 +7,7 @@ use std::collections::HashMap; use std::path::Path; use crate::kani_middle::codegen_units::Harness; -use crate::kani_middle::{KaniAttributes, SourceLocation, readable_name}; +use crate::kani_middle::{KaniAttributes, SourceLocation, readable_name, strip_local_crate_prefix}; use kani_metadata::ContractedFunction; use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; use rustc_middle::ty::TyCtxt; @@ -59,7 +59,10 @@ pub fn gen_contracts_metadata( let mut fn_to_data: HashMap = HashMap::new(); for item in crate_items { - let function = item.name(); + // Use crate-relative names (rust-lang/rust#149401 made `name()` crate-qualified for + // local items); the list output and the automatic-contract-harness lookup below both + // compare/display these names in crate-relative form. + let function = strip_local_crate_prefix(item.name()); let file = SourceLocation::new(item.span()).filename; let attributes = KaniAttributes::for_def_id(tcx, item.def_id()); @@ -75,9 +78,10 @@ pub fn gen_contracts_metadata( fn_to_data.insert( target_def_id, ContractedFunction { - // Note that we use the item's fully qualified-name, rather than the target name specified in the attribute. + // Note that we use the item's (crate-relative) name, rather than the + // target name specified in the attribute. // This is necessary for the automatic contract harness lookup, see below. - function: item.name(), + function: strip_local_crate_prefix(item.name()), file, harnesses: vec![function], }, @@ -94,13 +98,13 @@ pub fn gen_contracts_metadata( if let HarnessKind::ProofForContract { target_fn } = &metadata.attributes.kind { // FIXME: This is a bit hacky. We can't resolve the target_fn to a DefId because we need somewhere to start the name resolution from. // For a manual harness, we could just start from the harness, but since automatic harnesses are Kani intrinsics, we can't resolve the target starting from them. - // Instead, we rely on the fact that the ContractedFunction objects store the function's fully qualified name, - // and that `gen_automatic_proof_metadata` uses the fully qualified name as well. + // Instead, we rely on the fact that the ContractedFunction objects store the function's crate-relative name, + // and that `gen_automatic_proof_metadata` uses the crate-relative name as well. // Once we implement multiple automatic harnesses for a single function, we will have to revise the HarnessMetadata anyway, // and then we can revisit the idea of storing the target_fn's DefId somewhere. let (_, target_cf) = fn_to_data.iter_mut().find(|(_, cf)| &cf.function == target_fn).unwrap(); - target_cf.harnesses.push(harness.name()); + target_cf.harnesses.push(strip_local_crate_prefix(harness.name())); } } From a4994093136b9627c2d190bb192643e98859af0f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 9 Jul 2026 09:20:49 +0000 Subject: [PATCH 9/9] Support unsized-by-value function arguments (unsized_fn_params) The updated std (nightly-2025-12-31) exercises `unsized_fn_params` in alloc, e.g. `impl SpecExtendStr for [&str] { fn spec_extend_into(self, ...) }`, which takes an unsized `self: [&str]` by value. Kani codegened such arguments as their bare unsized type, which lowers to an incomplete `FlexibleArray`; that cannot be a function parameter (`as_parameter` asserts `can_be_lvalue`) and drops the length/vtable metadata, causing an ICE while codegenning the standard library. Represent unsized-by-value arguments as fat pointers instead (matching the ABI): - fn_typ: parameter type is the fat pointer (`codegen_ty_ref_stable`). - codegen_declare_variables + codegen_local: declare/emit the arg local as a fat pointer, keyed off the new `is_unsized_by_value_arg` helper (which uses the `arg_count` now tracked in `CurrentFnCtx`). - codegen_place_stable: model the base local as `*(&local)` by applying a `Deref` projection, reusing the existing fat-pointer projection logic so reads, indexing, and `&self` recover the data pointer and metadata. - codegen_place_ref_stable: `&self` returns the fat pointer directly. - codegen_operand_stable: pass the fat pointer for slice/str/dyn operands so callers forward the metadata too. Adds tests/kani/UnsizedFnParams/unsized_by_value_args.rs covering slice and str by-value self. Fixes the script-based-pre std_codegen regression. Co-authored-by: Kiro --- .../codegen_cprover_gotoc/codegen/function.rs | 8 +++- .../codegen_cprover_gotoc/codegen/operand.rs | 12 ++--- .../codegen_cprover_gotoc/codegen/place.rs | 47 ++++++++++++++++--- .../src/codegen_cprover_gotoc/codegen/typ.rs | 12 +++-- .../context/current_fn.rs | 10 ++++ .../UnsizedFnParams/unsized_by_value_args.rs | 44 +++++++++++++++++ 6 files changed, 117 insertions(+), 16 deletions(-) create mode 100644 tests/kani/UnsizedFnParams/unsized_by_value_args.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 8f4af7f06bd1..bc45256d804a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -33,7 +33,13 @@ impl GotocCtx<'_, '_> { } let base_name = self.codegen_var_base_name(&lc); let name = self.codegen_var_name(&lc); - let var_type = self.codegen_ty_stable(ldata.ty); + // Unsized-by-value arguments (`unsized_fn_params`) are represented as fat pointers, + // consistent with `fn_typ` and `codegen_local`. + let var_type = if self.is_unsized_by_value_arg(lc) { + self.codegen_ty_ref_stable(ldata.ty) + } else { + self.codegen_ty_stable(ldata.ty) + }; let loc = self.codegen_span_stable(ldata.span); // Indices [1, N] represent the function parameters where N is the number of parameters. // Except that ZST fields are not included as parameters. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index ca382c1fc080..624c4d6db19c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -43,13 +43,13 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { self, self.codegen_place_stable(place, Location::none()) ); - // If the operand itself is a Dynamic (like when passing a boxed closure), - // we need to pull off the fat pointer. In that case, the rustc kind() on - // both the operand and the inner type are Dynamic. - // Consider moving this check elsewhere in: - // https://github.com/model-checking/kani/issues/277 + // If the operand is itself an unsized value passed by value (a `Dynamic` boxed + // closure, or a slice/`str` via `unsized_fn_params`), the value is the fat + // pointer, so pull it off the projection rather than the (pointee) goto_expr. match self.operand_ty_stable(operand).kind() { - TyKind::RigidTy(RigidTy::Dynamic(..)) => projection.fat_ptr_goto_expr.unwrap(), + TyKind::RigidTy(RigidTy::Dynamic(..)) + | TyKind::RigidTy(RigidTy::Slice(..)) + | TyKind::RigidTy(RigidTy::Str) => projection.fat_ptr_goto_expr.unwrap(), _ => projection.goto_expr, } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 49cb15a18def..0ea6e2254038 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -397,7 +397,27 @@ impl GotocCtx<'_, '_> { // Otherwise, simply look up the local by the var name. let vname = self.codegen_var_name(&l); - Expr::symbol_expression(vname, self.codegen_ty_stable(local_ty)) + // Unsized-by-value arguments (`unsized_fn_params`, e.g. `fn f(self: [T])`) are + // represented as fat pointers rather than as the (incomplete) unsized type itself. + // See `fn_typ` and `codegen_declare_variables`. + let typ = if self.is_unsized_by_value_arg(l) { + self.codegen_ty_ref_stable(local_ty) + } else { + self.codegen_ty_stable(local_ty) + }; + Expr::symbol_expression(vname, typ) + } + + /// Returns true if `local` is a by-value function argument of an unsized type + /// (via the `unsized_fn_params` feature, e.g. `fn f(self: [T])` or `fn f(self: str)`). + /// + /// Such arguments cannot be represented directly (the unsized type codegens to an + /// incomplete `FlexibleArray`, which cannot be a function parameter or carry the + /// length/vtable metadata), so Kani represents them as fat pointers. + pub fn is_unsized_by_value_arg(&self, local: Local) -> bool { + local >= 1 + && local <= self.current_fn().arg_count() + && self.is_unsized(rustc_internal::internal(self.tcx, self.local_ty_stable(local))) } /// A projection is an operation that translates an lvalue to another lvalue. @@ -684,7 +704,11 @@ impl GotocCtx<'_, '_> { // Just return the address of the place dereferenced. address_of } - } else if place_ty == pointee_type(self.local_ty_stable(place.local)).unwrap() { + } else if self.is_unsized_by_value_arg(place.local) && place.projection.is_empty() { + // `&self` where `self` is an unsized-by-value argument: the reference is the + // fat pointer that the argument is represented by (see `codegen_place_stable`). + projection.fat_ptr_goto_expr.unwrap() + } else if pointee_type(self.local_ty_stable(place.local)).is_some_and(|p| place_ty == p) { // Just return the fat pointer if this is a simple &(*local). projection.fat_ptr_goto_expr.unwrap() } else { @@ -716,10 +740,21 @@ impl GotocCtx<'_, '_> { ) -> Result> { debug!(?place, "codegen_place"); let initial_expr = self.codegen_local(place.local, loc); - let initial_typ = TypeOrVariant::Type(self.local_ty_stable(place.local)); - debug!(?initial_typ, ?initial_expr, "codegen_place"); - let initial_projection = - ProjectedPlace::try_new(initial_expr, initial_typ, None, None, self); + let local_ty = self.local_ty_stable(place.local); + let initial_projection = if self.is_unsized_by_value_arg(place.local) { + // The local holds a fat pointer to the unsized value (see `codegen_local`). + // Model the place as the pointee of that fat pointer, i.e. `*(&local)`, by + // treating the local as a value of pointer type and applying a `Deref` + // projection. This reuses the existing fat-pointer projection logic so that + // reads, indexing, and `&self` recover the data pointer and length/vtable. + let ptr_ty = Ty::new_ptr(local_ty, Mutability::Not); + let base = ProjectedPlace::try_from_ty(initial_expr, ptr_ty, self); + self.codegen_projection(base, &ProjectionElem::Deref, loc) + } else { + let initial_typ = TypeOrVariant::Type(local_ty); + ProjectedPlace::try_new(initial_expr, initial_typ, None, None, self) + }; + debug!(?local_ty, ?initial_projection, "codegen_place"); let result = place .projection .iter() diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index ca32a86a1169..4b535d3ae9f0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1591,10 +1591,16 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { let (name, _) = self.codegen_spread_arg_name(&lc); ident = name; } - Some( + // Unsized-by-value arguments (`unsized_fn_params`, e.g. `fn f(self: [T])`) + // cannot be a parameter of their (incomplete) unsized type, and the length / + // vtable metadata must be carried somewhere, so represent them as fat pointers. + // `codegen_local` / `codegen_place_stable` recover the pointee accordingly. + let param_ty = if self.is_unsized(rustc_internal::internal(self.tcx, ty)) { + self.codegen_ty_ref_stable(ty) + } else { self.codegen_ty_stable(ty) - .as_parameter(Some(ident.clone().into()), Some(ident.into())), - ) + }; + Some(param_ty.as_parameter(Some(ident.clone().into()), Some(ident.into()))) } }) .collect(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs index 4be054daf34f..fbb7fecb63db 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -24,6 +24,8 @@ pub struct CurrentFnCtx<'tcx> { instance_internal: InstanceInternal<'tcx>, /// A list of local declarations used to retrieve MIR component types. locals: Vec, + /// The number of formal arguments of the current function (locals `1..=arg_count`). + arg_count: usize, /// A list of pretty names for locals that corrspond to user variables. local_names: HashMap, /// Collection of variables that are used in a reference or address-of expression. @@ -61,6 +63,7 @@ impl<'tcx> CurrentFnCtx<'tcx> { let readable_name = crate::kani_middle::readable_name(instance); let name = instance.mangled_name(); let locals = body.locals().to_vec(); + let arg_count = body.arg_locals().len(); let local_names = body .var_debug_info .iter() @@ -74,6 +77,7 @@ impl<'tcx> CurrentFnCtx<'tcx> { instance_internal, krate: instance.def.krate().name, locals, + arg_count, local_names, address_taken_locals: visitor.address_taken_locals, name, @@ -126,6 +130,12 @@ impl<'tcx> CurrentFnCtx<'tcx> { &self.locals } + /// The number of formal arguments of the current function; locals `1..=arg_count()` + /// are the arguments. + pub fn arg_count(&self) -> usize { + self.arg_count + } + pub fn local_name(&self, local: Local) -> Option { self.local_names.get(&local).copied() } diff --git a/tests/kani/UnsizedFnParams/unsized_by_value_args.rs b/tests/kani/UnsizedFnParams/unsized_by_value_args.rs new file mode 100644 index 000000000000..c8a6cf0e0ecf --- /dev/null +++ b/tests/kani/UnsizedFnParams/unsized_by_value_args.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that Kani can codegen and verify functions that take an unsized argument +//! *by value* via the `unsized_fn_params` feature (e.g. `fn f(self: [T])` and +//! `fn f(self: str)`). Such arguments are passed as fat pointers, so both the +//! length/metadata (`self.len()`, `self.as_bytes()`) and the data (`self[i]`) +//! must be recovered correctly. + +#![feature(unsized_fn_params)] + +trait SumSlice { + fn sum(self) -> u32; +} + +impl SumSlice for [u32] { + fn sum(self) -> u32 { + // `len()` exercises the fat-pointer metadata; indexing exercises the data pointer. + assert_eq!(self.len(), 3); + self[0] + self[1] + self[2] + } +} + +trait FirstByte { + fn first_byte(self) -> u8; +} + +impl FirstByte for str { + fn first_byte(self) -> u8 { + self.as_bytes()[0] + } +} + +#[kani::proof] +fn check_unsized_slice_arg() { + let boxed: Box<[u32]> = Box::new([1u32, 2, 3]); + assert_eq!((*boxed).sum(), 6); +} + +#[kani::proof] +fn check_unsized_str_arg() { + let boxed: Box = String::from("hi").into_boxed_str(); + assert_eq!((*boxed).first_byte(), b'h'); +}