From 1388508cff5ffb1d9fe3e87c32570adf5302ccd6 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 13 Aug 2026 17:59:52 -0400 Subject: [PATCH 1/3] Upgrade Rust toolchain to nightly-2026-04-01 Advance from nightly-2026-03-01 to nightly-2026-04-01. Several source changes are required to track rustc and rustc_public API changes. **Codegen backend interface.** `CodegenResults` is gone: rustc now keeps the compiled modules and the crate info apart. `codegen_crate` receives a `&CrateInfo` instead of the backend building one, `join_codegen` returns `CompiledModules`, `link` takes the modules and the crate info separately, `link_binary` gained a matching parameter, and `target_cpu` became a required method, implemented as cranelift does so that `-C target-cpu` is honoured. The backend factory closure now takes only the session. **`rustc_span` re-exports.** `respan`, `Spanned` and `dummy_spanned` are no longer public under `rustc_span::source_map`; import them from the root. **Allocation shim signatures.** These changed twice over, and between them broke every test that allocates -- 128 of them: - `align` is now `core::mem::Alignment` rather than `core::ptr::Alignment`. Kani already maps that type to `size_t` for FFI so the shims link against the `size_t` definitions in `kani_lib.c`, but the detection matched the old path only. - `__rust_dealloc` and `__rust_realloc` now take `NonNull` rather than `*mut u8`. `NonNull` is `repr(transparent)` over `*const T`, so it holds the same address, but its goto type is a struct and would not match the pointer-typed C definitions. The `NonNull` change reached the uninitialized-memory checks two ways, which is why `-Z uninit-checks` crashed with `Should only build checks for raw pointers, std::ptr::NonNull encountered`: the pointee type has to be resolved through the wrapper, and the argument handed to the shadow-memory model has to be the inner pointer, obtained by projecting `NonNull`'s single field. The `nonnull_pointee` helper lives in `kani_middle` since both the FFI signatures and the instrumentation need it. **Float intrinsics.** `fabsf16`/`fabsf32`/`fabsf64`/`fabsf128` were replaced by a single generic `fabs`, so the width is recovered from the signature and codegen keeps using the width-specific CBMC builtins; the four unmatchable arms are removed. `maxnumf32`/`maxnumf64` and `minnumf32`/`minnumf64` became `maximum_number_nsz_*` and `minimum_number_nsz_*`, the same semantics `f32::max`/`f32::min` use. Tests calling these by name are updated. **Stale feature gates.** `unused_features` now fires on gates a crate does not use, which caught five. `proc_macro_diagnostic` is only needed by `kani_macros`'s `#[cfg(kani_sysroot)]` module, so it is declared with `cfg_attr`, while `proc_macro_span` is not used at all -- the span APIs in `loop_contracts` come from `syn`/`proc-macro2`. `layout_for_ptr` is only reached by the `concrete_playback` paths of the `kani_core` memory models, so it is tied to that feature. `kani_core`'s `f16`/`f128` appear only inside macro bodies that expand in downstream crates, which declare the gates themselves. `more_qualified_paths` and `exit_status_error` are unused. Verified locally: the `kani` suite passes 600/600, both clippy passes and the format check are clean, and the per-package unit tests pass. The `shadow/unsupported_num_objects` expected test counts CBMC object IDs and my local CBMC suite is inconsistent (cbmc 6.10.0 with goto-synthesizer 6.8.0), so the remaining suites are left to CI. Upstream range: 38c0de8dcb14d42290042521be9958d37f3fa390...48cc71ee88cd0f11217eced958b9930970da998b --- .../codegen/foreign_function.rs | 19 ++++++-- .../compiler_interface.rs | 48 +++++++++++-------- .../codegen_cprover_gotoc/context/goto_ctx.rs | 2 +- kani-compiler/src/intrinsics.rs | 34 ++++++------- kani-compiler/src/kani_compiler.rs | 2 +- kani-compiler/src/kani_middle/intrinsics.rs | 2 +- kani-compiler/src/kani_middle/mod.rs | 17 +++++++ .../points_to/points_to_analysis.rs | 2 +- .../kani_middle/transform/check_uninit/mod.rs | 15 ++++-- .../check_uninit/ptr_uninit/uninit_visitor.rs | 27 +++++++++-- .../src/kani_middle/transform/internal_mir.rs | 4 +- kani-compiler/src/main.rs | 1 - library/kani/src/lib.rs | 4 +- library/kani_core/src/lib.rs | 2 - library/kani_macros/src/lib.rs | 5 +- rust-toolchain.toml | 2 +- tests/kani/Intrinsics/Math/fabsf128.rs | 4 +- tests/kani/Intrinsics/Math/fabsf16.rs | 4 +- tests/kani/Intrinsics/Math/fabsf32.rs | 4 +- tests/kani/Intrinsics/Math/fabsf64.rs | 4 +- tests/kani/Intrinsics/MaxNum/maxnumf32.rs | 6 +-- tests/kani/Intrinsics/MaxNum/maxnumf64.rs | 6 +-- tests/kani/Intrinsics/MinNum/minnumf32.rs | 6 +-- tests/kani/Intrinsics/MinNum/minnumf64.rs | 6 +-- tools/compile-timer/src/compile-timer.rs | 2 - 25 files changed, 139 insertions(+), 89 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 76f20eadbcc2..86390fc5867f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -11,6 +11,7 @@ use std::collections::HashSet; use crate::codegen_cprover_gotoc::GotocCtx; use crate::codegen_cprover_gotoc::codegen::PropertyClass; +use crate::kani_middle::nonnull_pointee; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type}; use cbmc::{InternString, InternedString}; @@ -168,7 +169,7 @@ impl GotocCtx<'_, '_> { .map(|(idx, arg)| { let arg_name = format!("{fn_name}::param_{idx}"); let base_name = format!("param_{idx}"); - // `core::ptr::Alignment` is `repr(transparent)` over a `repr(usize)` + // `core::mem::Alignment` is `repr(transparent)` over a `repr(usize)` // enum (ABI-identical to `usize`). As of nightly-2026-02-16 the Rust // allocation shims (`__rust_alloc` etc.) take their alignment argument // as `Alignment` rather than `usize`. Its goto type is not `size_t`, @@ -176,8 +177,10 @@ impl GotocCtx<'_, '_> { // `kani_lib.c` at link time, leaving the allocator body unlinked (so it // havocs and may "fail", making the OOM path reachable). Represent it as // `size_t` for FFI so the definitions link. - let arg_type = if is_ptr_alignment(arg.ty) { + let arg_type = if is_alignment(arg.ty) { Type::size_t() + } else if let Some(pointee) = nonnull_pointee(arg.ty) { + self.codegen_ty_stable(pointee).to_pointer() } else { self.codegen_ty_stable(arg.ty) }; @@ -230,10 +233,18 @@ impl GotocCtx<'_, '_> { /// ABI-identical to `usize`, but its goto type is not `size_t`. We treat it as /// `size_t` in foreign (FFI) signatures so that Rust's allocation shims match the /// `size_t`-typed definitions in `kani_lib.c`. -fn is_ptr_alignment(ty: rustc_public::ty::Ty) -> bool { +fn is_alignment(ty: rustc_public::ty::Ty) -> bool { matches!( ty.kind(), TyKind::RigidTy(RigidTy::Adt(def, _)) - if matches!(def.name().as_str(), "core::ptr::Alignment" | "std::ptr::Alignment") + if matches!( + def.name().as_str(), + // The type moved from `ptr` to `mem` in nightly-2026-03-21; both paths are matched + // so that this keeps working across the move. + "core::mem::Alignment" + | "std::mem::Alignment" + | "core::ptr::Alignment" + | "std::ptr::Alignment" + ) ) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index f167108127b4..0eb888e775e1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -27,7 +27,7 @@ use rustc_codegen_ssa::back::archive::{ }; use rustc_codegen_ssa::back::link::link_binary; use rustc_codegen_ssa::traits::CodegenBackend; -use rustc_codegen_ssa::{CodegenResults, CrateInfo, TargetConfig}; +use rustc_codegen_ssa::{CompiledModules, CrateInfo, TargetConfig}; use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; use rustc_metadata::EncodedMetadata; @@ -325,7 +325,15 @@ impl CodegenBackend for GotocCodegenBackend { } } - fn codegen_crate(&self, tcx: TyCtxt) -> Box { + fn target_cpu(&self, sess: &Session) -> String { + match sess.opts.cg.target_cpu { + Some(ref name) => name, + None => sess.target.cpu.as_ref(), + } + .to_owned() + } + + fn codegen_crate<'tcx>(&self, tcx: TyCtxt<'tcx>, _crate_info: &CrateInfo) -> Box { let ret_val = rustc_internal::run(tcx, || { super::utils::init(); @@ -372,7 +380,7 @@ impl CodegenBackend for GotocCodegenBackend { // If reachability is None, just return early as we'll do no codegen. if reachability == ReachabilityType::None { - return codegen_results(tcx, &results.machine_model); + return codegen_results(); } // Create an empty thread pool. We will set the size later once we @@ -484,7 +492,7 @@ impl CodegenBackend for GotocCodegenBackend { ); } } - codegen_results(tcx, &results.machine_model) + codegen_results() }); ret_val.unwrap() } @@ -494,8 +502,9 @@ impl CodegenBackend for GotocCodegenBackend { ongoing_codegen: Box, _sess: &Session, _filenames: &OutputFilenames, - ) -> (CodegenResults, FxIndexMap) { - match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() + ) -> (CompiledModules, FxIndexMap) { + match ongoing_codegen + .downcast::<(CompiledModules, FxIndexMap)>() { Ok(val) => *val, Err(val) => panic!("unexpected error: {:?}", (*val).type_id()), @@ -513,18 +522,20 @@ impl CodegenBackend for GotocCodegenBackend { fn link( &self, sess: &Session, - codegen_results: CodegenResults, + compiled_modules: CompiledModules, + crate_info: CrateInfo, rustc_metadata: EncodedMetadata, outputs: &OutputFilenames, ) { - let requested_crate_types = &codegen_results.crate_info.crate_types.clone(); - let local_crate_name = codegen_results.crate_info.local_crate_name; + let requested_crate_types = crate_info.crate_types.clone(); + let local_crate_name = crate_info.local_crate_name; // Create the rlib if one was requested. if requested_crate_types.contains(&CrateType::Rlib) { link_binary( sess, &ArArchiveBuilderBuilder, - codegen_results, + compiled_modules, + crate_info, rustc_metadata, outputs, self.name(), @@ -534,7 +545,7 @@ impl CodegenBackend for GotocCodegenBackend { // But override all the other outputs. // Note: Do this after `link_binary` call, since it may write to the object files // and override the json we are creating. - for crate_type in requested_crate_types { + for crate_type in &requested_crate_types { let out_fname = out_filename(sess, *crate_type, outputs, local_crate_name); let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); @@ -624,16 +635,13 @@ fn check_options(session: &Session) { } /// Return a struct that contains information about the codegen results as expected by `rustc`. -fn codegen_results(tcx: TyCtxt, machine: &MachineModel) -> Box { +/// +/// Kani produces no object files, so the module lists are empty. `rustc` now builds the `CrateInfo` +/// itself and passes it to `codegen_crate` and `link`, so there is nothing crate-specific to report +/// here. +fn codegen_results() -> Box { let work_products = FxIndexMap::::default(); - Box::new(( - CodegenResults { - modules: vec![], - allocator_module: None, - crate_info: CrateInfo::new(tcx, machine.architecture.clone()), - }, - work_products, - )) + Box::new((CompiledModules { modules: vec![], allocator_module: None }, work_products)) } pub fn write_file(base_path: &Path, file_type: ArtifactType, source: &T, pretty: bool) diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index d66a182fd206..e5d1a50a7bda 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -39,7 +39,7 @@ use rustc_public::mir::Body; use rustc_public::mir::mono::Instance; use rustc_public::ty::Allocation; use rustc_span::Span; -use rustc_span::source_map::respan; +use rustc_span::respan; use rustc_target::callconv::FnAbi; use std::collections::{BTreeMap, HashMap, HashSet}; use std::fmt::Debug; diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index f73685cd42f3..5ce02ff7c045 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -462,6 +462,16 @@ impl Intrinsic { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::Uint(UintTy::U8), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_)); Self::WriteBytes } + // `fabs` is generic over the float type as of nightly-2026-03-21, where it used to be + // one intrinsic per width (`fabsf32` and friends). Recover the width from the signature + // so that codegen can keep using the width-specific CBMC builtins. + "fabs" => match sig.inputs()[0].kind() { + TyKind::RigidTy(RigidTy::Float(FloatTy::F16)) => Self::FabsF16, + TyKind::RigidTy(RigidTy::Float(FloatTy::F32)) => Self::FabsF32, + TyKind::RigidTy(RigidTy::Float(FloatTy::F64)) => Self::FabsF64, + TyKind::RigidTy(RigidTy::Float(FloatTy::F128)) => Self::FabsF128, + other => unreachable!("Unexpected `fabs` argument type: {other:?}"), + }, _ => try_match_atomic(intrinsic_instance) .or_else(|| try_match_simd(intrinsic_instance)) .or_else(|| try_match_f32(intrinsic_instance)) @@ -675,14 +685,6 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::ExpF32) } - "fabsf16" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F16) => RigidTy::Float(FloatTy::F16)); - Some(Intrinsic::FabsF16) - } - "fabsf32" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); - Some(Intrinsic::FabsF32) - } "floorf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::FloorF32) @@ -703,11 +705,11 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::LogF32) } - "maxnumf32" => { + "maximum_number_nsz_f32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::MaxNumF32) } - "minnumf32" => { + "minimum_number_nsz_f32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::MinNumF32) } @@ -769,14 +771,6 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::ExpF64) } - "fabsf64" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); - Some(Intrinsic::FabsF64) - } - "fabsf128" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F128) => RigidTy::Float(FloatTy::F128)); - Some(Intrinsic::FabsF128) - } "floorf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::FloorF64) @@ -797,11 +791,11 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::LogF64) } - "maxnumf64" => { + "maximum_number_nsz_f64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::MaxNumF64) } - "minnumf64" => { + "minimum_number_nsz_f64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::MinNumF64) } diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 94510e244279..cc0dcc7c3ae1 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -131,7 +131,7 @@ impl Callbacks for KaniCompiler { // (potentially on a different thread). config.make_codegen_backend = Some(Box::new({ let args = args.clone(); - move |_cfg, _| backend(args) + move |_sess| backend(args) })); } diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index 7013feaf34d9..27c18c97af36 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -10,7 +10,7 @@ use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, Terminator use rustc_middle::mir::{Local, LocalDecl}; use rustc_middle::ty::{self, Ty, TyCtxt}; use rustc_middle::ty::{Const, GenericArgsRef, IntrinsicDef}; -use rustc_span::source_map::Spanned; +use rustc_span::Spanned; use rustc_span::symbol::{Symbol, sym}; use tracing::{debug, trace}; diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 2f7aedf59663..a7bc08fedb35 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -30,6 +30,23 @@ use self::attributes::KaniAttributes; /// 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. +/// If `ty` is `NonNull`, return `T`. +/// +/// `NonNull` is `repr(transparent)` over `*const T`, so it holds exactly the same address. The +/// Rust allocation shims (`__rust_dealloc`, `__rust_realloc`) took their pointer arguments as +/// `*mut u8` until nightly-2026-03-21 and as `NonNull` afterwards, so code that reasons about +/// those arguments as pointers has to see through the wrapper. +pub fn nonnull_pointee(ty: Ty) -> Option { + let TyKind::RigidTy(RigidTy::Adt(def, args)) = ty.kind() else { return None }; + if !matches!(def.name().as_str(), "core::ptr::NonNull" | "std::ptr::NonNull") { + return None; + } + args.0.first().and_then(|arg| match arg { + GenericArgKind::Type(ty) => Some(*ty), + _ => None, + }) +} + pub fn readable_name(instance: Instance) -> String { strip_local_crate_prefix(instance.name()) } 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 4ee27ecc9a1e..1d028a934220 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 @@ -43,7 +43,7 @@ use rustc_middle::{ use rustc_mir_dataflow::{Analysis, Forward, JoinSemiLattice}; use rustc_public::mir::{Body as StableBody, mono::Instance as StableInstance}; use rustc_public::rustc_internal; -use rustc_span::{DUMMY_SP, source_map::Spanned}; +use rustc_span::{DUMMY_SP, Spanned}; use std::collections::HashSet; /// Main points-to analysis object. diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 364c4edaf6b7..f9ff48a29495 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -4,6 +4,7 @@ //! Module containing multiple transformation passes that instrument the code to detect possible UB //! due to the accesses to uninitialized memory. +use crate::kani_middle::nonnull_pointee; use crate::kani_middle::transform::body::{ CheckType, InsertPosition, MutableBody, SourceInstruction, }; @@ -149,14 +150,18 @@ impl<'a> UninitInstrumenter<'a> { // Sanity check: since CBMC memory object primitives only accept pointers, need to // ensure the correct type. let ptr_operand_ty = operation.operand_ty(body); - let pointee_ty = match ptr_operand_ty.kind() { - TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) => pointee_ty, - _ => { + let pointee_ty = + if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ptr_operand_ty.kind() { + pointee_ty + } else if let Some(pointee_ty) = nonnull_pointee(ptr_operand_ty) { + // The allocation shims hand us a `NonNull`, which holds the same address as the + // `*mut u8` they used to take. + pointee_ty + } else { unreachable!( "Should only build checks for raw pointers, `{ptr_operand_ty}` encountered." ) - } - }; + }; // Calculate pointee layout for byte-by-byte memory initialization checks. match PointeeInfo::from_ty(pointee_ty) { Ok(type_info) => type_info, diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 7e5d604b3319..acfb116611e6 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -5,6 +5,7 @@ use crate::{ intrinsics::Intrinsic, + kani_middle::nonnull_pointee, kani_middle::transform::{ body::{InsertPosition, MutableBody, SourceInstruction}, check_uninit::{ @@ -16,14 +17,14 @@ use crate::{ }; use rustc_public::{ mir::{ - AggregateKind, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, - PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, + AggregateKind, CastKind, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic, Operand, + Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, alloc::GlobalAlloc, mono::{Instance, InstanceKind}, visit::{Location, PlaceContext}, }, - ty::{AdtKind, ConstantKind, RigidTy, TyKind}, + ty::{AdtKind, ConstantKind, RigidTy, Ty, TyKind}, }; pub struct CheckUninitVisitor { @@ -371,7 +372,7 @@ impl MirVisitor for CheckUninitVisitor { "alloc::alloc::__rust_dealloc" => { /* Memory is uninitialized here, need to update shadow memory. */ self.push_target(MemoryInitOp::SetSliceChunk { - operand: args[0].clone(), + operand: raw_ptr_arg(&args[0], self.locals.as_slice()), count: args[1].clone(), value: false, position: InsertPosition::After, @@ -709,3 +710,21 @@ fn try_resolve_instance(locals: &[LocalDecl], func: &Operand) -> Result` as of nightly-2026-03-21, where they previously took `*mut u8`. +/// `NonNull` is `repr(transparent)` over a single `*const T` field, so projecting that field +/// yields the same address with the pointer type the shadow-memory models expect. Operands that are +/// already raw pointers, and any shape we cannot project, are passed through unchanged. +fn raw_ptr_arg(arg: &Operand, locals: &[LocalDecl]) -> Operand { + let Ok(arg_ty) = arg.ty(locals) else { return arg.clone() }; + let Some(pointee) = nonnull_pointee(arg_ty) else { return arg.clone() }; + let place = match arg { + Operand::Copy(place) | Operand::Move(place) => place, + Operand::Constant(_) | Operand::RuntimeChecks(_) => return arg.clone(), + }; + let mut projection = place.projection.clone(); + projection.push(ProjectionElem::Field(0, Ty::new_ptr(pointee, Mutability::Not))); + Operand::Copy(Place { local: place.local, projection }) +} diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index e943746db671..974bb1272c39 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -567,9 +567,7 @@ impl RustcInternalMir for TerminatorKind { rustc_middle::mir::TerminatorKind::Call { func: func.internal_mir(tcx), args: Box::from_iter( - args.iter().map(|arg| { - rustc_span::source_map::dummy_spanned(arg.internal_mir(tcx)) - }), + args.iter().map(|arg| rustc_span::dummy_spanned(arg.internal_mir(tcx))), ), destination: internal(tcx, destination), target: target.map(|basic_block_idx| { diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index cf00140c348c..e4348fdc7a10 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -10,7 +10,6 @@ #![recursion_limit = "256"] #![feature(box_patterns)] #![feature(rustc_private)] -#![feature(more_qualified_paths)] #![feature(iter_intersperse)] #![feature(f128)] #![feature(f16)] diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 7a5f68031b9b..30bab3ab3abe 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -16,7 +16,9 @@ // Required for `rustc_diagnostic_item` and `core_intrinsics` #![allow(internal_features)] // Required for implementing memory predicates. -#![feature(layout_for_ptr)] +// `core::mem::{size_of,align_of}_val_raw` are only reached by the `concrete_playback` paths of +// the `kani_core` memory models this crate expands. +#![cfg_attr(feature = "concrete_playback", feature(layout_for_ptr))] #![feature(ptr_metadata)] #![feature(f16)] #![feature(f128)] diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index b3dbc80e25a1..f21accc11591 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -17,8 +17,6 @@ #![feature(no_core)] #![no_core] -#![feature(f16)] -#![feature(f128)] mod arbitrary; mod bounded_arbitrary; diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 80ae350a056b..f58504ec0f92 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -7,8 +7,9 @@ // downstream crates to enable these features as well. // So we have to enable this on the commandline (see kani-rustc) with: // RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)" -#![feature(proc_macro_diagnostic)] -#![feature(proc_macro_span)] +// Only the `sysroot` module uses these, and it is `#[cfg(kani_sysroot)]`, so declaring them +// unconditionally makes the ordinary build trip `unused_features`. +#![cfg_attr(kani_sysroot, feature(proc_macro_diagnostic))] mod derive; mod derive_bounded; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index bf68329885c9..775b8b99d414 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2026-03-01" +channel = "nightly-2026-04-01" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Intrinsics/Math/fabsf128.rs b/tests/kani/Intrinsics/Math/fabsf128.rs index 14d5f013ceb0..aae2b6e1f22d 100644 --- a/tests/kani/Intrinsics/Math/fabsf128.rs +++ b/tests/kani/Intrinsics/Math/fabsf128.rs @@ -10,7 +10,7 @@ fn test_abs_finite() { let x: f128 = kani::any(); kani::assume(!x.is_nan()); - let abs_x = unsafe { std::intrinsics::fabsf128(x) }; + let abs_x = unsafe { std::intrinsics::fabs(x) }; if x < 0.0 { assert!(-x == abs_x); } else { @@ -22,6 +22,6 @@ fn test_abs_finite() { fn test_abs_nan() { let x: f128 = kani::any(); kani::assume(x.is_nan()); - let abs_x = unsafe { std::intrinsics::fabsf128(x) }; + let abs_x = unsafe { std::intrinsics::fabs(x) }; assert!(abs_x.is_nan()); } diff --git a/tests/kani/Intrinsics/Math/fabsf16.rs b/tests/kani/Intrinsics/Math/fabsf16.rs index a26b7790a59d..6cb156b0721a 100644 --- a/tests/kani/Intrinsics/Math/fabsf16.rs +++ b/tests/kani/Intrinsics/Math/fabsf16.rs @@ -10,7 +10,7 @@ fn test_abs_finite() { let x: f16 = kani::any(); kani::assume(!x.is_nan()); - let abs_x = unsafe { std::intrinsics::fabsf16(x) }; + let abs_x = unsafe { std::intrinsics::fabs(x) }; if x < 0.0 { assert!(-x == abs_x); } else { @@ -22,6 +22,6 @@ fn test_abs_finite() { fn test_abs_nan() { let x: f16 = kani::any(); kani::assume(x.is_nan()); - let abs_x = unsafe { std::intrinsics::fabsf16(x) }; + let abs_x = unsafe { std::intrinsics::fabs(x) }; assert!(abs_x.is_nan()); } diff --git a/tests/kani/Intrinsics/Math/fabsf32.rs b/tests/kani/Intrinsics/Math/fabsf32.rs index 63ecc08db9c3..5e8901367a56 100644 --- a/tests/kani/Intrinsics/Math/fabsf32.rs +++ b/tests/kani/Intrinsics/Math/fabsf32.rs @@ -9,7 +9,7 @@ fn test_abs_finite() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); - let abs_x = unsafe { std::intrinsics::fabsf32(x) }; + let abs_x = unsafe { std::intrinsics::fabs(x) }; if x < 0.0 { assert!(-x == abs_x); } else { @@ -21,6 +21,6 @@ fn test_abs_finite() { fn test_abs_nan() { let x: f32 = kani::any(); kani::assume(x.is_nan()); - let abs_x = unsafe { std::intrinsics::fabsf32(x) }; + let abs_x = unsafe { std::intrinsics::fabs(x) }; assert!(abs_x.is_nan()); } diff --git a/tests/kani/Intrinsics/Math/fabsf64.rs b/tests/kani/Intrinsics/Math/fabsf64.rs index 6f08b7717805..4e8ae31a2a8a 100644 --- a/tests/kani/Intrinsics/Math/fabsf64.rs +++ b/tests/kani/Intrinsics/Math/fabsf64.rs @@ -9,7 +9,7 @@ fn test_abs_finite() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); - let abs_x = unsafe { std::intrinsics::fabsf64(x) }; + let abs_x = unsafe { std::intrinsics::fabs(x) }; if x < 0.0 { assert!(-x == abs_x); } else { @@ -21,6 +21,6 @@ fn test_abs_finite() { fn test_abs_nan() { let x: f64 = kani::any(); kani::assume(x.is_nan()); - let abs_x = unsafe { std::intrinsics::fabsf64(x) }; + let abs_x = unsafe { std::intrinsics::fabs(x) }; assert!(abs_x.is_nan()); } diff --git a/tests/kani/Intrinsics/MaxNum/maxnumf32.rs b/tests/kani/Intrinsics/MaxNum/maxnumf32.rs index e2636a665452..f4ae96668445 100644 --- a/tests/kani/Intrinsics/MaxNum/maxnumf32.rs +++ b/tests/kani/Intrinsics/MaxNum/maxnumf32.rs @@ -12,7 +12,7 @@ fn test_general() { let x: f32 = kani::any(); let y: f32 = kani::any(); kani::assume(!x.is_nan() && !y.is_nan()); - let res = std::intrinsics::maxnumf32(x, y); + let res = std::intrinsics::maximum_number_nsz_f32(x, y); if x > y { assert!(res == x); } else { @@ -25,7 +25,7 @@ fn test_one_nan() { let x: f32 = kani::any(); let y: f32 = kani::any(); kani::assume((x.is_nan() && !y.is_nan()) || (!x.is_nan() && y.is_nan())); - let res = std::intrinsics::maxnumf32(x, y); + let res = std::intrinsics::maximum_number_nsz_f32(x, y); if x.is_nan() { assert!(res == y); } else { @@ -38,6 +38,6 @@ fn test_both_nan() { let x: f32 = kani::any(); let y: f32 = kani::any(); kani::assume(x.is_nan() && y.is_nan()); - let res = std::intrinsics::maxnumf32(x, y); + let res = std::intrinsics::maximum_number_nsz_f32(x, y); assert!(res.is_nan()); } diff --git a/tests/kani/Intrinsics/MaxNum/maxnumf64.rs b/tests/kani/Intrinsics/MaxNum/maxnumf64.rs index a986b3cf5319..7e889fab586e 100644 --- a/tests/kani/Intrinsics/MaxNum/maxnumf64.rs +++ b/tests/kani/Intrinsics/MaxNum/maxnumf64.rs @@ -12,7 +12,7 @@ fn test_general() { let x: f64 = kani::any(); let y: f64 = kani::any(); kani::assume(!x.is_nan() && !y.is_nan()); - let res = std::intrinsics::maxnumf64(x, y); + let res = std::intrinsics::maximum_number_nsz_f64(x, y); if x > y { assert!(res == x); } else { @@ -25,7 +25,7 @@ fn test_one_nan() { let x: f64 = kani::any(); let y: f64 = kani::any(); kani::assume((x.is_nan() && !y.is_nan()) || (!x.is_nan() && y.is_nan())); - let res = std::intrinsics::maxnumf64(x, y); + let res = std::intrinsics::maximum_number_nsz_f64(x, y); if x.is_nan() { assert!(res == y); } else { @@ -38,6 +38,6 @@ fn test_both_nan() { let x: f64 = kani::any(); let y: f64 = kani::any(); kani::assume(x.is_nan() && y.is_nan()); - let res = std::intrinsics::maxnumf64(x, y); + let res = std::intrinsics::maximum_number_nsz_f64(x, y); assert!(res.is_nan()); } diff --git a/tests/kani/Intrinsics/MinNum/minnumf32.rs b/tests/kani/Intrinsics/MinNum/minnumf32.rs index 289587d83ec0..2d5bd76cb1d1 100644 --- a/tests/kani/Intrinsics/MinNum/minnumf32.rs +++ b/tests/kani/Intrinsics/MinNum/minnumf32.rs @@ -12,7 +12,7 @@ fn test_general() { let x: f32 = kani::any(); let y: f32 = kani::any(); kani::assume(!x.is_nan() && !y.is_nan()); - let res = std::intrinsics::minnumf32(x, y); + let res = std::intrinsics::minimum_number_nsz_f32(x, y); if x < y { assert!(res == x); } else { @@ -25,7 +25,7 @@ fn test_one_nan() { let x: f32 = kani::any(); let y: f32 = kani::any(); kani::assume((x.is_nan() && !y.is_nan()) || (!x.is_nan() && y.is_nan())); - let res = std::intrinsics::minnumf32(x, y); + let res = std::intrinsics::minimum_number_nsz_f32(x, y); if x.is_nan() { assert!(res == y); } else { @@ -38,6 +38,6 @@ fn test_both_nan() { let x: f32 = kani::any(); let y: f32 = kani::any(); kani::assume(x.is_nan() && y.is_nan()); - let res = std::intrinsics::minnumf32(x, y); + let res = std::intrinsics::minimum_number_nsz_f32(x, y); assert!(res.is_nan()); } diff --git a/tests/kani/Intrinsics/MinNum/minnumf64.rs b/tests/kani/Intrinsics/MinNum/minnumf64.rs index 111574433f5e..ed745da5a5b9 100644 --- a/tests/kani/Intrinsics/MinNum/minnumf64.rs +++ b/tests/kani/Intrinsics/MinNum/minnumf64.rs @@ -12,7 +12,7 @@ fn test_general() { let x: f64 = kani::any(); let y: f64 = kani::any(); kani::assume(!x.is_nan() && !y.is_nan()); - let res = std::intrinsics::minnumf64(x, y); + let res = std::intrinsics::minimum_number_nsz_f64(x, y); if x < y { assert!(res == x); } else { @@ -25,7 +25,7 @@ fn test_one_nan() { let x: f64 = kani::any(); let y: f64 = kani::any(); kani::assume((x.is_nan() && !y.is_nan()) || (!x.is_nan() && y.is_nan())); - let res = std::intrinsics::minnumf64(x, y); + let res = std::intrinsics::minimum_number_nsz_f64(x, y); if x.is_nan() { assert!(res == y); } else { @@ -38,6 +38,6 @@ fn test_both_nan() { let x: f64 = kani::any(); let y: f64 = kani::any(); kani::assume(x.is_nan() && y.is_nan()); - let res = std::intrinsics::minnumf64(x, y); + let res = std::intrinsics::minimum_number_nsz_f64(x, y); assert!(res.is_nan()); } diff --git a/tools/compile-timer/src/compile-timer.rs b/tools/compile-timer/src/compile-timer.rs index 4c7799d40ff4..c1aaa69d7cef 100644 --- a/tools/compile-timer/src/compile-timer.rs +++ b/tools/compile-timer/src/compile-timer.rs @@ -1,8 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -#![feature(exit_status_error)] - use crate::common::{AggrResult, Stats, aggregate_aggregates, krate_trimmed_path}; use clap::Parser; use serde::Serialize; From 08a94482d337fcd73779b882a1453d39565c2441 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 13 Aug 2026 18:26:50 -0400 Subject: [PATCH 2/3] Apply the same codegen-backend changes to the LLBC backend The Lean backend has its own `CodegenBackend` implementation, and it needs the identical treatment: `CompiledModules` in place of `CodegenResults`, `codegen_crate` taking `&CrateInfo`, `link` taking the modules and the crate info separately, the extra `link_binary` argument, and the new required `target_cpu`. Since rustc now builds the `CrateInfo` itself, the backend no longer maps `tcx.sess.target.arch` into it, which leaves the `rustc_target::spec::Arch` import unused. Missed in the previous commit because the backend is behind the optional `llbc` feature, so the default build never compiles it -- `llbc-regression` caught it. Verified with `cargo build-dev -- --features cprover --features llbc` and the `llbc` suite, 10 passed. --- .../codegen_aeneas_llbc/compiler_interface.rs | 54 +++++++++---------- 1 file changed, 27 insertions(+), 27 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index e81b4f77219e..834998cec343 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -25,7 +25,7 @@ use rustc_codegen_ssa::back::archive::{ }; use rustc_codegen_ssa::back::link::link_binary; use rustc_codegen_ssa::traits::CodegenBackend; -use rustc_codegen_ssa::{CodegenResults, CrateInfo}; +use rustc_codegen_ssa::{CompiledModules, CrateInfo}; use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; use rustc_errors::ErrorGuaranteed; use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; @@ -40,7 +40,6 @@ use rustc_public::{CrateDef, DefId}; use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; -use rustc_target::spec::Arch; use std::any::Any; use std::fs::File; use std::path::Path; @@ -199,7 +198,15 @@ impl CodegenBackend for LlbcCodegenBackend { "kani-llbc" } - fn codegen_crate(&self, tcx: TyCtxt) -> Box { + fn target_cpu(&self, sess: &Session) -> String { + match sess.opts.cg.target_cpu { + Some(ref name) => name, + None => sess.target.cpu.as_ref(), + } + .to_owned() + } + + fn codegen_crate<'tcx>(&self, tcx: TyCtxt<'tcx>, _crate_info: &CrateInfo) -> Box { let ret_val = rustc_internal::run(tcx, || { // Queries shouldn't change today once codegen starts. let queries = QUERY_DB.with(|db| db.borrow().clone()); @@ -279,7 +286,7 @@ impl CodegenBackend for LlbcCodegenBackend { // To avoid overriding the metadata for its verification, we skip this step when // reachability is None, even because there is nothing to record. } - codegen_results(tcx) + codegen_results() }); ret_val.unwrap() } @@ -289,8 +296,9 @@ impl CodegenBackend for LlbcCodegenBackend { ongoing_codegen: Box, _sess: &Session, _filenames: &OutputFilenames, - ) -> (CodegenResults, FxIndexMap) { - match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() + ) -> (CompiledModules, FxIndexMap) { + match ongoing_codegen + .downcast::<(CompiledModules, FxIndexMap)>() { Ok(val) => *val, Err(val) => panic!("unexpected error: {:?}", (*val).type_id()), @@ -314,21 +322,23 @@ impl CodegenBackend for LlbcCodegenBackend { fn link( &self, sess: &Session, - codegen_results: CodegenResults, + compiled_modules: CompiledModules, + crate_info: CrateInfo, rustc_metadata: EncodedMetadata, outputs: &OutputFilenames, ) { - let requested_crate_types = &codegen_results.crate_info.crate_types.clone(); - let local_crate_name = codegen_results.crate_info.local_crate_name; + let requested_crate_types = crate_info.crate_types.clone(); + let local_crate_name = crate_info.local_crate_name; link_binary( sess, &ArArchiveBuilderBuilder, - codegen_results, + compiled_modules, + crate_info, rustc_metadata, outputs, self.name(), ); - for crate_type in requested_crate_types { + for crate_type in &requested_crate_types { let out_fname = out_filename(sess, *crate_type, outputs, local_crate_name); let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); @@ -362,23 +372,13 @@ fn contract_metadata_for_harness( } /// Return a struct that contains information about the codegen results as expected by `rustc`. -fn codegen_results(tcx: TyCtxt) -> Box { +/// +/// Kani produces no object files, so the module lists are empty. `rustc` now builds the `CrateInfo` +/// itself and passes it to `codegen_crate` and `link`, so there is nothing crate-specific to report +/// here. +fn codegen_results() -> Box { let work_products = FxIndexMap::::default(); - Box::new(( - CodegenResults { - modules: vec![], - allocator_module: None, - crate_info: CrateInfo::new( - tcx, - match tcx.sess.target.arch { - Arch::X86_64 => "x86_64".to_string(), - Arch::AArch64 => "aarch64".to_string(), - _ => format!("{:?}", tcx.sess.target.arch).to_lowercase(), - }, - ), - }, - work_products, - )) + Box::new((CompiledModules { modules: vec![], allocator_module: None }, work_products)) } /// Execute the provided function and measure the clock time it took for its execution. From 0ff0954fd7231858f5857d0ce0fe42da3344f2f5 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 13 Aug 2026 19:02:33 -0400 Subject: [PATCH 3/3] Address review: restore misplaced docs and update the intrinsics table Three documentation defects from the previous commits, all valid. `nonnull_pointee` was inserted between `readable_name`'s doc comment and `readable_name` itself, so that comment -- which explains stripping the local crate prefix after rust-lang/rust#149401 -- ended up documenting the new helper, and `readable_name` was left undocumented. The helper now sits after `readable_name`, restoring the original pairing. `is_alignment`'s summary still claimed it checks `core::ptr::Alignment` only, while it accepts the `mem` and `ptr` modules under both `core` and `std`. The user-facing intrinsic support table in `docs/src/rust-feature-support/intrinsics.md` still advertised the removed `fabsf32`/`fabsf64`, `maxnumf*` and `minnumf*` names. It now lists `fabs` and the `maximum_number_nsz_*`/`minimum_number_nsz_*` names this PR matches on. --- docs/src/rust-feature-support/intrinsics.md | 11 +++++------ .../codegen_cprover_gotoc/codegen/foreign_function.rs | 3 ++- kani-compiler/src/kani_middle/mod.rs | 8 ++++---- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 74b0290736a1..ea662ff7c3d7 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -152,8 +152,7 @@ exp2f32 | Partial | Results are overapproximated | exp2f64 | Partial | Results are overapproximated | expf32 | Partial | Results are overapproximated | expf64 | Partial | Results are overapproximated | -fabsf32 | Yes | | -fabsf64 | Yes | | +fabs | Yes | | fadd_fast | Yes | | fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) | float_to_int_unchecked | Yes | | @@ -172,12 +171,12 @@ log2f32 | Partial | Results are overapproximated | log2f64 | Partial | Results are overapproximated | logf32 | Partial | Results are overapproximated | logf64 | Partial | Results are overapproximated | -maxnumf32 | Yes | | -maxnumf64 | Yes | | +maximum_number_nsz_f32 | Yes | | +maximum_number_nsz_f64 | Yes | | align_of | Yes | | align_of_val | Yes | | -minnumf32 | Yes | | -minnumf64 | Yes | | +minimum_number_nsz_f32 | Yes | | +minimum_number_nsz_f64 | Yes | | move_val_init | No | | mul_with_overflow | Yes | | needs_drop | Yes | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 86390fc5867f..f72a91c398d9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -227,7 +227,8 @@ impl GotocCtx<'_, '_> { } } -/// Returns `true` if `ty` is `core::ptr::Alignment`. +/// Returns `true` if `ty` is the standard library's `Alignment`, under either the `core` or `std` +/// path and under either the `mem` module (as of nightly-2026-03-21) or the `ptr` module (before). /// /// That type is `repr(transparent)` over a `repr(usize)` enum and is therefore /// ABI-identical to `usize`, but its goto type is not `size_t`. We treat it as diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index a7bc08fedb35..72ee77a92051 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -30,6 +30,10 @@ use self::attributes::KaniAttributes; /// 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()) +} + /// If `ty` is `NonNull`, return `T`. /// /// `NonNull` is `repr(transparent)` over `*const T`, so it holds exactly the same address. The @@ -47,10 +51,6 @@ pub fn nonnull_pointee(ty: Ty) -> Option { }) } -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,