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/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 diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index a244d37366e2..bc45256d804a 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}; @@ -32,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. @@ -220,7 +227,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/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 07542322fa51..624c4d6db19c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -43,19 +43,24 @@ 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, } } 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/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/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index e3a30a8bf3f0..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. @@ -1321,7 +1320,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/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/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/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index ce027e53da22..4b535d3ae9f0 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() { @@ -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 7a2be6b06c5a..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. @@ -58,9 +60,10 @@ 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 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/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/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/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 6686c2b219de..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"); @@ -301,7 +304,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; @@ -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 d4c395a2a1a3..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}; +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; @@ -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. @@ -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())); } } @@ -119,7 +123,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..2f7aedf59663 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; @@ -74,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/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/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/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index f7d1794de5dd..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); @@ -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; 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 edd016add17c..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)) + } } } } @@ -101,8 +104,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 @@ -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/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()), ), ); } 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 fc2945d6422c..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-05" +channel = "nightly-2025-12-31" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] 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(); 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'); +}