Upgrade Rust toolchain to nightly-2024-03-01

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

@@ -415,6 +415,11 @@ impl<'tcx> GotocCtx<'tcx> {
                 loc,
                 "https://github.com/model-checking/kani/issues/374",
             ),
+            "catch_unwind" => self.codegen_unimplemented_stmt(
+                intrinsic,
+                loc,
+                "https://github.com/model-checking/kani/issues/267",
+            ),
             "ceilf32" => codegen_simple_intrinsic!(Ceilf),
             "ceilf64" => codegen_simple_intrinsic!(Ceil),
             "compare_bytes" => self.codegen_compare_bytes(fargs, place, loc),
@@ -584,11 +589,6 @@ impl<'tcx> GotocCtx<'tcx> {
             "transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, place),
             "truncf32" => codegen_simple_intrinsic!(Truncf),
             "truncf64" => codegen_simple_intrinsic!(Trunc),
-            "try" => self.codegen_unimplemented_stmt(
-                intrinsic,
-                loc,
-                "https://github.com/model-checking/kani/issues/267",
-            ),
             "type_id" => codegen_intrinsic_const!(),
             "type_name" => codegen_intrinsic_const!(),
             "unaligned_volatile_load" => {

kani-compiler/src/session.rs

@@ -4,12 +4,17 @@
 //! Module used to configure a compiler session.
 
 use crate::args::Arguments;
+use rustc_data_structures::sync::Lrc;
+use rustc_errors::emitter::Emitter;
 use rustc_errors::{
-    emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter,
-    ColorConfig, Diagnostic, TerminalUrl,
+    emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter, ColorConfig,
+    DiagInner,
 };
 use rustc_session::config::ErrorOutputType;
 use rustc_session::EarlyDiagCtxt;
+use rustc_span::source_map::FilePathMapping;
+use rustc_span::source_map::SourceMap;
+use std::io;
 use std::io::IsTerminal;
 use std::panic;
 use std::sync::LazyLock;
@@ -49,17 +54,15 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send
             let msg = format!("Kani unexpectedly panicked at {info}.",);
             let fallback_bundle =
                 fallback_fluent_bundle(rustc_driver::DEFAULT_LOCALE_RESOURCES.to_vec(), false);
-            let mut emitter = JsonEmitter::basic(
-                false,
-                HumanReadableErrorType::Default(ColorConfig::Never),
-                None,
+            let mut emitter = JsonEmitter::new(
+                Box::new(io::BufWriter::new(io::stderr())),
+                #[allow(clippy::arc_with_non_send_sync)]
+                Lrc::new(SourceMap::new(FilePathMapping::empty())),
                 fallback_bundle,
-                None,
                 false,
-                false,
-                TerminalUrl::No,
+                HumanReadableErrorType::Default(ColorConfig::Never),
             );
-            let diagnostic = Diagnostic::new(rustc_errors::Level::Bug, msg);
+            let diagnostic = DiagInner::new(rustc_errors::Level::Bug, msg);
             emitter.emit_diagnostic(diagnostic);
             (*JSON_PANIC_HOOK)(info);
         }));

kani-driver/src/cbmc_property_renderer.rs

@@ -837,7 +837,7 @@ fn annotate_properties_with_reach_results(
             let prop_match_id =
                 check_marker_pat.captures(description.as_str()).unwrap().get(0).unwrap().as_str();
             // Get the status associated to the ID we captured
-            let reach_status_opt = reach_map.get(&prop_match_id.to_string());
+            let reach_status_opt = reach_map.get(prop_match_id);
             // Update the reachability status of the property
             if let Some(reach_status) = reach_status_opt {
                 prop.reach = Some(*reach_status);

library/kani/src/lib.rs

@@ -13,7 +13,7 @@
 // Used to model simd.
 #![feature(repr_simd)]
 // Features used for tests only.
-#![cfg_attr(test, feature(platform_intrinsics, portable_simd))]
+#![cfg_attr(test, feature(core_intrinsics, portable_simd))]
 // Required for rustc_diagnostic_item
 #![allow(internal_features)]
 

library/kani/src/models/mod.rs

@@ -127,12 +127,9 @@ mod intrinsics {
 #[cfg(test)]
 mod test {
     use super::intrinsics as kani_intrinsic;
+    use std::intrinsics::simd::*;
     use std::{fmt::Debug, simd::*};
 
-    extern "platform-intrinsic" {
-        fn simd_bitmask<T, U>(x: T) -> U;
-    }
-
     /// Test that the `simd_bitmask` model is equivalent to the intrinsic for all true and all false
     /// masks with lanes represented using i16.
     #[test]

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-02-25"
+channel = "nightly-2024-03-01"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/cargo-kani/assess-artifacts/expected

@@ -3,7 +3,7 @@ Analyzed 1 packages
  Unsupported feature |   Crates | Instances
                      | impacted |    of use
 ---------------------+----------+-----------
- try                 |        1 |         2
+ catch_unwind        |        1 |         2
 ============================================
 =========================================
  Reason for failure    | Number of tests

tests/cargo-kani/assess-workspace-artifacts/expected

@@ -3,7 +3,7 @@ Analyzed 2 packages
  Unsupported feature |   Crates | Instances
                      | impacted |    of use
 ---------------------+----------+-----------
- try                 |        2 |         3
+ catch_unwind        |        2 |         3
 ============================================
 =========================================
  Reason for failure    | Number of tests

tests/expected/intrinsics/simd-arith-overflows/main.rs

@@ -2,19 +2,14 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! This test ensures we detect overflows in SIMD arithmetic operations
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::{simd_add, simd_mul, simd_sub};
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
 pub struct i8x2(i8, i8);
 
-extern "platform-intrinsic" {
-    fn simd_add<T>(x: T, y: T) -> T;
-    fn simd_sub<T>(x: T, y: T) -> T;
-    fn simd_mul<T>(x: T, y: T) -> T;
-}
-
 #[kani::proof]
 fn main() {
     let a = kani::any();

tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs

@@ -3,7 +3,8 @@
 
 //! Checks that storing the result of a vector operation in a vector of
 //! size different to the operands' sizes causes an error.
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::simd_eq;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
@@ -20,14 +21,6 @@ pub struct u64x2(u64, u64);
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct u32x4(u32, u32, u32, u32);
 
-// From <https://github.com/rust-lang/rfcs/blob/master/text/1199-simd-infrastructure.md#comparisons>:
-// > The type checker ensures that `T` and `U` have the same length, and that
-// > `U` is appropriately "boolean"-y.
-// This means that `U` is allowed to be `i64` or `u64`, but not `f64`.
-extern "platform-intrinsic" {
-    fn simd_eq<T, U>(x: T, y: T) -> U;
-}
-
 #[kani::proof]
 fn main() {
     let x = u64x2(0, 0);

tests/expected/intrinsics/simd-div-div-zero/main.rs

@@ -2,17 +2,14 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `simd_div` triggers a failure when the divisor is zero.
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::simd_div;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct i32x2(i32, i32);
 
-extern "platform-intrinsic" {
-    fn simd_div<T>(x: T, y: T) -> T;
-}
-
 #[kani::proof]
 fn test_simd_div() {
     let dividend = kani::any();

tests/expected/intrinsics/simd-div-rem-overflow/main.rs

@@ -1,20 +1,15 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Checks that the `simd_div` and `simd_rem` intrinsics check for integer overflows.
-
-#![feature(repr_simd, platform_intrinsics)]
+//! Checks that the `simd_div` and `simd_rem` intrinsics check for integer overflows.
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::{simd_div, simd_rem};
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct i32x2(i32, i32);
 
-extern "platform-intrinsic" {
-    fn simd_div<T>(x: T, y: T) -> T;
-    fn simd_rem<T>(x: T, y: T) -> T;
-}
-
 unsafe fn do_simd_div(dividends: i32x2, divisors: i32x2) -> i32x2 {
     simd_div(dividends, divisors)
 }

tests/expected/intrinsics/simd-extract-wrong-type/main.rs

@@ -4,17 +4,14 @@
 //! This test checks that we emit an error when the return type for
 //! `simd_extract` has a type different to the first argument's (i.e., the
 //! vector) base type.
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::simd_extract;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct i64x2(i64, i64);
 
-extern "platform-intrinsic" {
-    fn simd_extract<T, U>(x: T, idx: u32) -> U;
-}
-
 #[kani::proof]
 fn main() {
     let y = i64x2(0, 1);

tests/expected/intrinsics/simd-insert-wrong-type/main.rs

@@ -4,17 +4,14 @@
 //! This test checks that we emit an error when the third argument for
 //! `simd_insert` (the value to be inserted) has a type different to the first
 //! argument's (i.e., the vector) base type.
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::simd_insert;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct i64x2(i64, i64);
 
-extern "platform-intrinsic" {
-    fn simd_insert<T, U>(x: T, idx: u32, b: U) -> T;
-}
-
 #[kani::proof]
 fn main() {
     let y = i64x2(0, 1);

tests/expected/intrinsics/simd-rem-div-zero/main.rs

@@ -2,17 +2,14 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `simd_rem` triggers a failure when the divisor is zero
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::simd_rem;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct i32x2(i32, i32);
 
-extern "platform-intrinsic" {
-    fn simd_rem<T>(x: T, y: T) -> T;
-}
-
 #[kani::proof]
 fn test_simd_rem() {
     let dividend = kani::any();

tests/expected/intrinsics/simd-result-type-is-float/main.rs

@@ -3,7 +3,8 @@
 
 //! Checks that storing the result of a vector comparison in a vector of floats
 //! causes an error.
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::simd_eq;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
@@ -25,14 +26,6 @@ pub struct u32x4(u32, u32, u32, u32);
 #[derive(Clone, Copy, PartialEq)]
 pub struct f32x2(f32, f32);
 
-// From <https://github.com/rust-lang/rfcs/blob/master/text/1199-simd-infrastructure.md#comparisons>:
-// > The type checker ensures that `T` and `U` have the same length, and that
-// > `U` is appropriately "boolean"-y.
-// This means that `U` is allowed to be `i64` or `u64`, but not `f64`.
-extern "platform-intrinsic" {
-    fn simd_eq<T, U>(x: T, y: T) -> U;
-}
-
 #[kani::proof]
 fn main() {
     let x = u64x2(0, 0);

tests/expected/intrinsics/simd-shl-shift-negative/main.rs

@@ -2,17 +2,14 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `simd_shl` returns a failure if the shift distance is negative.
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::simd_shl;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct i32x2(i32, i32);
 
-extern "platform-intrinsic" {
-    fn simd_shl<T>(x: T, y: T) -> T;
-}
-
 #[kani::proof]
 fn test_simd_shl() {
     let value = kani::any();

tests/expected/intrinsics/simd-shl-shift-too-large/main.rs

@@ -2,17 +2,14 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `simd_shl` returns a failure if the shift distance is too large.
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::simd_shl;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct i32x2(i32, i32);
 
-extern "platform-intrinsic" {
-    fn simd_shl<T>(x: T, y: T) -> T;
-}
-
 #[kani::proof]
 fn test_simd_shl() {
     let value = kani::any();

tests/expected/intrinsics/simd-shr-shift-negative/main.rs

@@ -2,17 +2,14 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `simd_shr` returns a failure if the shift distance is negative.
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::simd_shr;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct i32x2(i32, i32);
 
-extern "platform-intrinsic" {
-    fn simd_shr<T>(x: T, y: T) -> T;
-}
-
 #[kani::proof]
 fn test_simd_shr() {
     let value = kani::any();

tests/expected/intrinsics/simd-shr-shift-too-large/main.rs

@@ -2,17 +2,14 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `simd_shr` returns a failure if the shift distance is too large.
-#![feature(repr_simd, platform_intrinsics)]
+#![feature(repr_simd, core_intrinsics)]
+use std::intrinsics::simd::simd_shr;
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct i32x2(i32, i32);
 
-extern "platform-intrinsic" {
-    fn simd_shr<T>(x: T, y: T) -> T;
-}
-
 #[kani::proof]
 fn test_simd_shr() {
     let value = kani::any();