Toolchain upgrade to nightly-2025-05-04 (#4059)

This PR upgrade Rust toolchain to nightly-2025-05-04.
Thanks to @remi-delmas-3000 the suggestion, we can enable
target-features.
For this PR, I enabled sse and neon. 

Resolves #3059 #3878 #4044

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

Author: thanhnguyen-aws

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -283,6 +283,7 @@ impl GotocCtx<'_> {
                     | AssertMessage::DivisionByZero { .. }
                     | AssertMessage::RemainderByZero { .. }
                     | AssertMessage::ResumedAfterReturn { .. }
+                    | AssertMessage::ResumedAfterDrop { .. }
                     | AssertMessage::ResumedAfterPanic { .. } => {
                         (msg.description().unwrap(), PropertyClass::Assertion)
                     }

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -29,7 +29,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::{CodegenResults, CrateInfo, TargetConfig};
 use rustc_data_structures::fx::{FxHashMap, FxIndexMap};
 use rustc_errors::DEFAULT_LOCALE_RESOURCE;
 use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE};
@@ -41,6 +41,7 @@ use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
 use rustc_smir::rustc_internal;
+use rustc_span::symbol::Symbol;
 use rustc_target::spec::PanicStrategy;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::{Instance, MonoItem};
@@ -249,6 +250,19 @@ impl CodegenBackend for GotocCodegenBackend {
         DEFAULT_LOCALE_RESOURCE
     }
 
+    fn target_config(&self, _sess: &Session) -> TargetConfig {
+        TargetConfig {
+            target_features: vec![],
+            unstable_target_features: vec![Symbol::intern("sse"), Symbol::intern("neon")],
+            // `true` is used as a default so backends need to acknowledge when they do not
+            // support the float types, rather than accidentally quietly skipping all tests.
+            has_reliable_f16: true,
+            has_reliable_f16_math: true,
+            has_reliable_f128: true,
+            has_reliable_f128_math: true,
+        }
+    }
+
     fn codegen_crate(
         &self,
         tcx: TyCtxt,

kani-compiler/src/kani_middle/transform/internal_mir.rs

@@ -549,6 +549,9 @@ impl RustcInternalMir for AssertMessage {
             AssertMessage::NullPointerDereference => {
                 rustc_middle::mir::AssertMessage::NullPointerDereference
             }
+            AssertMessage::ResumedAfterDrop(coroutine_kind) => {
+                rustc_middle::mir::AssertMessage::ResumedAfterDrop(coroutine_kind.internal_mir(tcx))
+            }
         }
     }
 }
@@ -579,6 +582,8 @@ impl RustcInternalMir for TerminatorKind {
                     target: rustc_middle::mir::BasicBlock::from_usize(*target),
                     unwind: unwind.internal_mir(tcx),
                     replace: false,
+                    drop: None,
+                    async_fut: None,
                 }
             }
             TerminatorKind::Call { func, args, destination, target, unwind } => {

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-04-24"
+channel = "nightly-2025-05-04"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/function-contract/history/block.expected

@@ -1,5 +1,5 @@
 assertion\
 	 - Status: SUCCESS\
-	 - Description: "|result| old({ let x = &ptr; let y = **x; y + 1 }) == *ptr"\
+	 - Description: "|result| old({let x = &ptr; let y = **x; y + 1}) == *ptr"\
 
 VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/history/side_effect.expected

@@ -1,2 +1,2 @@
-Failed Checks: |result| old({ *ptr+=1; *ptr }) == _val
+Failed Checks: |result| old({*ptr+=1; *ptr}) == _val
 VERIFICATION:- FAILED

tests/expected/function-contract/interior-mutability/api/unsafecell.expected

@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| unsafe{ *im.x.get() } < 101"\
+- Description: "|_| unsafe{*im.x.get()} < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected

@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| unsafe{ *im.x.as_ptr() } < 101"\
+- Description: "|_| unsafe{*im.x.as_ptr()} < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected

@@ -1,6 +1,6 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| unsafe{ *im.x.get() } < 101"\
+- Description: "|_| unsafe{*im.x.get()} < 101"\
 in function modify
 
 VERIFICATION:- SUCCESSFUL

tests/expected/ptr_to_ref_cast/alignment/expected

@@ -1,4 +1,4 @@
 check_misaligned_ptr_cast_fail.safety_check\
 Status: FAILURE\
-Description: "misaligned pointer to reference cast: address must be a multiple of its type's alignment"\
+Description: "misaligned pointer dereference: address must be a multiple of its type's alignment"\
 in function check_misaligned_ptr_cast_fail