Upgrade Rust toolchain to nightly-2026-04-01

[feliperodri]

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, honouring -C target-cpu). The backend factory closure in kani_compiler.rs 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 crate root.

Allocation shim signatures. The shims changed shape twice over, and both changes 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 on the old path only. Both paths are now accepted.
• The pointer arguments of __rust_dealloc and __rust_realloc are now NonNull<u8> rather than *mut u8. NonNull<T> 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. Foreign signatures now represent it as a pointer, via a nonnull_pointee helper in kani_middle shared with the uninitialized-memory instrumentation.

The same NonNull change reached the uninitialized-memory checks two ways, which is why -Z uninit-checks was crashing with Should only build checks for raw pointers, std::ptr::NonNull<u8> encountered: the pointee type had to be resolved through the wrapper, and the argument handed to the shadow-memory model had to be the inner pointer, obtained by projecting NonNull's single field.

Float intrinsics. fabsf16/fabsf32/fabsf64/fabsf128 were replaced by a single generic fabs<T: FloatPrimitive>; the width is now recovered from the signature so codegen keeps using the width-specific CBMC builtins, and the four unmatchable arms are removed. maxnumf32/maxnumf64 and minnumf32/minnumf64 were renamed to 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:

• kani_macros: proc_macro_diagnostic is only needed by the #[cfg(kani_sysroot)] module, so it is declared with cfg_attr; proc_macro_span is not used at all (the span APIs in loop_contracts come from syn/proc-macro2) and is removed.
• library/kani: 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: f16/f128 appear only inside macro bodies that expand in downstream crates, which declare the gates themselves.
• kani-compiler: more_qualified_paths, and compile-timer: exit_status_error, are both unused.

Upstream commit range: 38c0de8dcb14d42290042521be9958d37f3fa390...48cc71ee88cd0f11217eced958b9930970da998b

Resolves #4737.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

Upgrades Kani to Rust nightly 2026-04-01 and adapts compiler integrations to upstream API changes.

Changes:

• Updates codegen backend and rustc API usage.
• Supports revised allocation shims and uninitialized-memory instrumentation.
• Migrates renamed float intrinsics and removes obsolete feature gates.

Reviewed changes

Copilot reviewed 26 out of 26 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
rust-toolchain.toml	Updates the nightly toolchain.
tools/compile-timer/src/compile-timer.rs	Removes an unused feature gate.
library/kani/src/lib.rs	Gates layout_for_ptr by feature.
library/kani_macros/src/lib.rs	Narrows proc-macro feature usage.
library/kani_core/src/lib.rs	Removes unused float feature gates.
kani-compiler/src/main.rs	Removes an obsolete feature gate.
kani-compiler/src/kani_compiler.rs	Updates backend factory signature.
kani-compiler/src/intrinsics.rs	Handles renamed generic float intrinsics.
kani-compiler/src/kani_middle/mod.rs	Adds NonNull pointee resolution.
kani-compiler/src/kani_middle/intrinsics.rs	Updates Spanned import.
kani-compiler/src/kani_middle/points_to/points_to_analysis.rs	Updates Spanned import.
kani-compiler/src/kani_middle/transform/internal_mir.rs	Updates dummy_spanned usage.
kani-compiler/src/kani_middle/transform/check_uninit/mod.rs	Supports NonNull operands.
kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs	Projects shim pointers for instrumentation.
kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs	Updates respan import.
kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs	Migrates the goto backend interface.
kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs	Adapts allocation-shim FFI types.
kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs	Migrates the LLBC backend interface.
tests/kani/Intrinsics/Math/fabsf16.rs	Tests generic fabs for f16.
tests/kani/Intrinsics/Math/fabsf32.rs	Tests generic fabs for f32.
tests/kani/Intrinsics/Math/fabsf64.rs	Tests generic fabs for f64.
tests/kani/Intrinsics/Math/fabsf128.rs	Tests generic fabs for f128.
tests/kani/Intrinsics/MaxNum/maxnumf32.rs	Uses renamed f32 maximum intrinsic.
tests/kani/Intrinsics/MaxNum/maxnumf64.rs	Uses renamed f64 maximum intrinsic.
tests/kani/Intrinsics/MinNum/minnumf32.rs	Uses renamed f32 minimum intrinsic.
tests/kani/Intrinsics/MinNum/minnumf64.rs	Uses renamed f64 minimum intrinsic.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.