From 12768f247b35059e0535afe388f0c7dfabd6f907 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Mon, 4 Mar 2024 16:39:48 -0500 Subject: [PATCH] Upgrade Rust toolchain to `nightly-2024-03-01` (#3052) Upgrades the Rust toolchain to `nightly-2024-03-01`. The Rust compiler PRs that triggered changes in this upgrades are: * https://github.com/rust-lang/rust/pull/121516 * https://github.com/rust-lang/rust/pull/121598 * https://github.com/rust-lang/rust/pull/121489 * https://github.com/rust-lang/rust/pull/121783 --- .../codegen/intrinsic.rs | 10 ++++---- kani-compiler/src/session.rs | 23 +++++++++++-------- kani-driver/src/cbmc_property_renderer.rs | 2 +- library/kani/src/lib.rs | 2 +- library/kani/src/models/mod.rs | 5 +--- rust-toolchain.toml | 2 +- tests/cargo-kani/assess-artifacts/expected | 2 +- .../assess-workspace-artifacts/expected | 2 +- .../intrinsics/simd-arith-overflows/main.rs | 9 ++------ .../simd-cmp-result-type-is-diff-size/main.rs | 11 ++------- .../intrinsics/simd-div-div-zero/main.rs | 7 ++---- .../intrinsics/simd-div-rem-overflow/main.rs | 11 +++------ .../simd-extract-wrong-type/main.rs | 7 ++---- .../intrinsics/simd-insert-wrong-type/main.rs | 7 ++---- .../intrinsics/simd-rem-div-zero/main.rs | 7 ++---- .../simd-result-type-is-float/main.rs | 11 ++------- .../simd-shl-shift-negative/main.rs | 7 ++---- .../simd-shl-shift-too-large/main.rs | 7 ++---- .../simd-shr-shift-negative/main.rs | 7 ++---- .../simd-shr-shift-too-large/main.rs | 7 ++---- .../simd-shuffle-indexes-out/main.rs | 7 ++---- .../main.rs | 7 ++---- .../main.rs | 7 ++---- tests/kani/Intrinsics/SIMD/Compare/float.rs | 14 ++--------- .../SIMD/Compare/result_type_is_same_size.rs | 11 ++------- tests/kani/Intrinsics/SIMD/Compare/signed.rs | 16 ++----------- .../kani/Intrinsics/SIMD/Compare/unsigned.rs | 16 ++----------- .../kani/Intrinsics/SIMD/Construction/main.rs | 8 ++----- tests/kani/Intrinsics/SIMD/Operators/arith.rs | 14 ++++------- .../kani/Intrinsics/SIMD/Operators/bitmask.rs | 9 ++------ .../Intrinsics/SIMD/Operators/bitshift.rs | 8 ++----- .../kani/Intrinsics/SIMD/Operators/bitwise.rs | 8 ++----- .../Intrinsics/SIMD/Operators/division.rs | 8 ++----- .../SIMD/Operators/division_float.rs | 7 ++---- .../SIMD/Operators/remainder_float_fixme.rs | 7 ++---- tests/kani/Intrinsics/SIMD/Shuffle/main.rs | 7 ++---- tests/kani/SIMD/simd_float_ops_fixme.rs | 8 ++----- tools/bookrunner/librustdoc/doctest.rs | 11 +++++---- 38 files changed, 91 insertions(+), 228 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 7996d434c351..20e3f34f48bf 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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" => { diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 5b5416a5f142..bc0930eb9e4b 100644 --- a/kani-compiler/src/session.rs +++ b/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) + 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); })); diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 62ef748a1ad5..c233959abd6a 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/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); diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index e3456f69fbb3..087e23c7d47e 100644 --- a/library/kani/src/lib.rs +++ b/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)] diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 194f220595c0..2081ddf639df 100644 --- a/library/kani/src/models/mod.rs +++ b/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(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] diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 408b2e859604..747a9f2f5295 100644 --- a/rust-toolchain.toml +++ b/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"] diff --git a/tests/cargo-kani/assess-artifacts/expected b/tests/cargo-kani/assess-artifacts/expected index c1d3acbfd531..b8a25c834ab6 100644 --- a/tests/cargo-kani/assess-artifacts/expected +++ b/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 diff --git a/tests/cargo-kani/assess-workspace-artifacts/expected b/tests/cargo-kani/assess-workspace-artifacts/expected index 4e9a26f89c27..fba2cd94f212 100644 --- a/tests/cargo-kani/assess-workspace-artifacts/expected +++ b/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 diff --git a/tests/expected/intrinsics/simd-arith-overflows/main.rs b/tests/expected/intrinsics/simd-arith-overflows/main.rs index 74cfe8ae878f..fc710645fd66 100644 --- a/tests/expected/intrinsics/simd-arith-overflows/main.rs +++ b/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(x: T, y: T) -> T; - fn simd_sub(x: T, y: T) -> T; - fn simd_mul(x: T, y: T) -> T; -} - #[kani::proof] fn main() { let a = kani::any(); diff --git a/tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs b/tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs index f826ae92f3b7..f84cf1d8b9aa 100644 --- a/tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs +++ b/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 : -// > 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(x: T, y: T) -> U; -} - #[kani::proof] fn main() { let x = u64x2(0, 0); diff --git a/tests/expected/intrinsics/simd-div-div-zero/main.rs b/tests/expected/intrinsics/simd-div-div-zero/main.rs index 4f613e362947..148ae62a252c 100644 --- a/tests/expected/intrinsics/simd-div-div-zero/main.rs +++ b/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(x: T, y: T) -> T; -} - #[kani::proof] fn test_simd_div() { let dividend = kani::any(); diff --git a/tests/expected/intrinsics/simd-div-rem-overflow/main.rs b/tests/expected/intrinsics/simd-div-rem-overflow/main.rs index e7f2e9fbc48f..5f49e7db6154 100644 --- a/tests/expected/intrinsics/simd-div-rem-overflow/main.rs +++ b/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(x: T, y: T) -> T; - fn simd_rem(x: T, y: T) -> T; -} - unsafe fn do_simd_div(dividends: i32x2, divisors: i32x2) -> i32x2 { simd_div(dividends, divisors) } diff --git a/tests/expected/intrinsics/simd-extract-wrong-type/main.rs b/tests/expected/intrinsics/simd-extract-wrong-type/main.rs index 5d32f1ed9de8..b8fb5a3ffc6f 100644 --- a/tests/expected/intrinsics/simd-extract-wrong-type/main.rs +++ b/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(x: T, idx: u32) -> U; -} - #[kani::proof] fn main() { let y = i64x2(0, 1); diff --git a/tests/expected/intrinsics/simd-insert-wrong-type/main.rs b/tests/expected/intrinsics/simd-insert-wrong-type/main.rs index ec2edfc110dd..6c4946a051b6 100644 --- a/tests/expected/intrinsics/simd-insert-wrong-type/main.rs +++ b/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(x: T, idx: u32, b: U) -> T; -} - #[kani::proof] fn main() { let y = i64x2(0, 1); diff --git a/tests/expected/intrinsics/simd-rem-div-zero/main.rs b/tests/expected/intrinsics/simd-rem-div-zero/main.rs index 715de058154b..4393808ac039 100644 --- a/tests/expected/intrinsics/simd-rem-div-zero/main.rs +++ b/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(x: T, y: T) -> T; -} - #[kani::proof] fn test_simd_rem() { let dividend = kani::any(); diff --git a/tests/expected/intrinsics/simd-result-type-is-float/main.rs b/tests/expected/intrinsics/simd-result-type-is-float/main.rs index 18a2152b93c5..01286de9cdd8 100644 --- a/tests/expected/intrinsics/simd-result-type-is-float/main.rs +++ b/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 : -// > 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(x: T, y: T) -> U; -} - #[kani::proof] fn main() { let x = u64x2(0, 0); diff --git a/tests/expected/intrinsics/simd-shl-shift-negative/main.rs b/tests/expected/intrinsics/simd-shl-shift-negative/main.rs index 0c7116b30567..2b7b2a418e19 100644 --- a/tests/expected/intrinsics/simd-shl-shift-negative/main.rs +++ b/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(x: T, y: T) -> T; -} - #[kani::proof] fn test_simd_shl() { let value = kani::any(); diff --git a/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs b/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs index fff9aadf1900..dada7a5a8b84 100644 --- a/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs +++ b/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(x: T, y: T) -> T; -} - #[kani::proof] fn test_simd_shl() { let value = kani::any(); diff --git a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs b/tests/expected/intrinsics/simd-shr-shift-negative/main.rs index 580f0337db25..dc38955099a2 100644 --- a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs +++ b/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(x: T, y: T) -> T; -} - #[kani::proof] fn test_simd_shr() { let value = kani::any(); diff --git a/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs b/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs index 3d9cd5e0c919..70ae0ad0da45 100644 --- a/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs +++ b/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(x: T, y: T) -> T; -} - #[kani::proof] fn test_simd_shr() { let value = kani::any(); diff --git a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs index d8a4c22de85f..0f7c42d2d46c 100644 --- a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs +++ b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs @@ -3,17 +3,14 @@ //! Checks that `simd_shuffle` triggers an out-of-bounds failure when any of the //! indexes supplied is greater than the combined size of the input vectors. -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::simd_shuffle; #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x2(i64, i64); -extern "platform-intrinsic" { - fn simd_shuffle(x: T, y: T, idx: U) -> V; -} - #[kani::proof] fn main() { let y = i64x2(0, 1); diff --git a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs index 25796f6c22e7..6345f5516101 100644 --- a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs +++ b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs @@ -3,7 +3,8 @@ //! Checks that Kani triggers an error when the result type doesn't have the //! length expected from a `simd_shuffle` call. -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::simd_shuffle; #[repr(simd)] #[allow(non_camel_case_types)] @@ -15,10 +16,6 @@ pub struct i64x2(i64, i64); #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x4(i64, i64, i64, i64); -extern "platform-intrinsic" { - fn simd_shuffle(x: T, y: T, idx: I) -> U; -} - #[kani::proof] fn main() { let y = i64x2(0, 1); diff --git a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs index 6bdadae159f8..81f176700152 100644 --- a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs +++ b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs @@ -3,7 +3,8 @@ //! Checks that Kani triggers an error when the result type doesn't have the //! subtype expected from a `simd_shuffle` call. -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::simd_shuffle; #[repr(simd)] #[allow(non_camel_case_types)] @@ -15,10 +16,6 @@ pub struct i64x2(i64, i64); #[derive(Clone, Copy, PartialEq)] pub struct f64x2(f64, f64); -extern "platform-intrinsic" { - fn simd_shuffle(x: T, y: T, idx: I) -> U; -} - #[kani::proof] fn main() { let y = i64x2(0, 1); diff --git a/tests/kani/Intrinsics/SIMD/Compare/float.rs b/tests/kani/Intrinsics/SIMD/Compare/float.rs index 6d2113beb3a0..cc5765ef226b 100644 --- a/tests/kani/Intrinsics/SIMD/Compare/float.rs +++ b/tests/kani/Intrinsics/SIMD/Compare/float.rs @@ -2,7 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Checks that intrinsics for SIMD vectors of signed integers are supported -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::*; #[repr(simd)] #[allow(non_camel_case_types)] @@ -19,17 +20,6 @@ pub struct i64x2(i64, i64); #[derive(Clone, Copy, PartialEq)] pub struct i32x2(i32, i32); -// The predicate type U in the functions below must -// be a SIMD type, otherwise we get a compilation error -extern "platform-intrinsic" { - fn simd_eq(x: T, y: T) -> U; - fn simd_ne(x: T, y: T) -> U; - fn simd_lt(x: T, y: T) -> U; - fn simd_le(x: T, y: T) -> U; - fn simd_gt(x: T, y: T) -> U; - fn simd_ge(x: T, y: T) -> U; -} - macro_rules! assert_cmp { ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => { let $res_cmp: i32x2 = $simd_cmp($x, $y); diff --git a/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs b/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs index cc38ad81864d..d3582057fd00 100644 --- a/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs +++ b/tests/kani/Intrinsics/SIMD/Compare/result_type_is_same_size.rs @@ -3,7 +3,8 @@ //! Checks that storing the result of a vector operation in a vector of //! size equal to the operands' sizes works. -#![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 u32x2(u32, u32); -// From : -// > 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(x: T, y: T) -> U; -} - #[kani::proof] fn main() { let x = u64x2(0, 0); diff --git a/tests/kani/Intrinsics/SIMD/Compare/signed.rs b/tests/kani/Intrinsics/SIMD/Compare/signed.rs index be93395fd2d9..cfd781fa64c7 100644 --- a/tests/kani/Intrinsics/SIMD/Compare/signed.rs +++ b/tests/kani/Intrinsics/SIMD/Compare/signed.rs @@ -2,26 +2,14 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Checks that intrinsics for SIMD vectors of signed integers are supported -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::*; #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x2(i64, i64); -// From : -// > 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(x: T, y: T) -> U; - fn simd_ne(x: T, y: T) -> U; - fn simd_lt(x: T, y: T) -> U; - fn simd_le(x: T, y: T) -> U; - fn simd_gt(x: T, y: T) -> U; - fn simd_ge(x: T, y: T) -> U; -} - macro_rules! assert_cmp { ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => { let $res_cmp: i64x2 = $simd_cmp($x, $y); diff --git a/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs b/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs index d30640f123d2..ee39f750c8a2 100644 --- a/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs +++ b/tests/kani/Intrinsics/SIMD/Compare/unsigned.rs @@ -2,26 +2,14 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Checks that intrinsics for SIMD vectors of unsigned integers are supported -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::*; #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] pub struct u64x2(u64, u64); -// From : -// > 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(x: T, y: T) -> U; - fn simd_ne(x: T, y: T) -> U; - fn simd_lt(x: T, y: T) -> U; - fn simd_le(x: T, y: T) -> U; - fn simd_gt(x: T, y: T) -> U; - fn simd_ge(x: T, y: T) -> U; -} - macro_rules! assert_cmp { ($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => { let $res_cmp: u64x2 = $simd_cmp($x, $y); diff --git a/tests/kani/Intrinsics/SIMD/Construction/main.rs b/tests/kani/Intrinsics/SIMD/Construction/main.rs index 6e9116e4dc15..5de3ae20d868 100644 --- a/tests/kani/Intrinsics/SIMD/Construction/main.rs +++ b/tests/kani/Intrinsics/SIMD/Construction/main.rs @@ -3,18 +3,14 @@ //! Checks that the `simd_extract` and `simd_insert` intrinsics are supported //! and return the expected results. -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::{simd_extract, simd_insert}; #[repr(simd)] #[allow(non_camel_case_types)] #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x2(i64, i64); -extern "platform-intrinsic" { - fn simd_extract(x: T, idx: u32) -> U; - fn simd_insert(x: T, idx: u32, b: U) -> T; -} - #[kani::proof] fn main() { let y = i64x2(0, 1); diff --git a/tests/kani/Intrinsics/SIMD/Operators/arith.rs b/tests/kani/Intrinsics/SIMD/Operators/arith.rs index 6af147b826e0..d9f442a659ba 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/arith.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/arith.rs @@ -1,22 +1,16 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This test doesn't work because support for SIMD intrinsics isn't available -//! at the moment in Kani. Support to be added in -//! -#![feature(repr_simd, platform_intrinsics)] +//! Checks that the SIMD intrinsics `simd_add`, `simd_sub` and +//! `simd_mul` are supported and return the expected results. +#![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)] pub struct i8x2(i8, i8); -extern "platform-intrinsic" { - fn simd_add(x: T, y: T) -> T; - fn simd_sub(x: T, y: T) -> T; - fn simd_mul(x: T, y: T) -> T; -} - macro_rules! verify_no_overflow { ($cf: ident, $uf: ident) => {{ let a: i8 = kani::any(); diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs b/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs index 4d3293264b6e..6992408436b9 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs @@ -6,16 +6,11 @@ //! This is done by initializing vectors with the contents of 2-member tuples //! with symbolic values. The result of using each of the intrinsics is compared //! against the result of using the associated bitwise operator on the tuples. -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] #![feature(generic_const_exprs)] #![feature(portable_simd)] -#![feature(core_intrinsics)] - use std::fmt::Debug; - -extern "platform-intrinsic" { - fn simd_bitmask(x: T) -> U; -} +use std::intrinsics::simd::simd_bitmask; #[repr(simd)] #[derive(Clone, Debug)] diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs index 1041f918123f..fa2cd3c52cd6 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs @@ -3,7 +3,8 @@ //! Checks that the `simd_shl` and `simd_shr` intrinsics are supported and they //! return the expected results. -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::{simd_shl, simd_shr}; #[repr(simd)] #[allow(non_camel_case_types)] @@ -15,11 +16,6 @@ pub struct i32x2(i32, i32); #[derive(Clone, Copy, PartialEq, Eq)] pub struct u32x2(u32, u32); -extern "platform-intrinsic" { - fn simd_shl(x: T, y: T) -> T; - fn simd_shr(x: T, y: T) -> T; -} - #[kani::proof] fn test_simd_shl() { let value = kani::any(); diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs b/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs index aa53bb6ac9ea..b18410088f18 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/bitwise.rs @@ -8,7 +8,8 @@ //! This is done by initializing vectors with the contents of 2-member tuples //! with symbolic values. The result of using each of the intrinsics is compared //! against the result of using the associated bitwise operator on the tuples. -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::{simd_and, simd_or, simd_xor}; #[repr(simd)] #[allow(non_camel_case_types)] @@ -50,11 +51,6 @@ pub struct u32x2(u32, u32); #[derive(Clone, Copy, PartialEq, Eq)] pub struct u64x2(u64, u64); -extern "platform-intrinsic" { - fn simd_and(x: T, y: T) -> T; - fn simd_or(x: T, y: T) -> T; - fn simd_xor(x: T, y: T) -> T; -} macro_rules! compare_simd_op_with_normal_op { ($simd_op: ident, $normal_op: tt, $simd_type: ident) => { let tup_x: (_,_) = kani::any(); diff --git a/tests/kani/Intrinsics/SIMD/Operators/division.rs b/tests/kani/Intrinsics/SIMD/Operators/division.rs index 593ac3fdfe7b..e1e8dab39cca 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/division.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/division.rs @@ -3,18 +3,14 @@ //! Checks that the `simd_div` and `simd_rem` intrinsics are supported and they //! return the expected results. -#![feature(repr_simd, platform_intrinsics)] +#![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(x: T, y: T) -> T; - fn simd_rem(x: T, y: T) -> T; -} - #[kani::proof] fn test_simd_div() { let dividend = kani::any(); diff --git a/tests/kani/Intrinsics/SIMD/Operators/division_float.rs b/tests/kani/Intrinsics/SIMD/Operators/division_float.rs index 97ea2e6e7ca7..711b67b87116 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/division_float.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/division_float.rs @@ -2,7 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Checks that the `simd_div` intrinsic returns the expected results for floating point numbers. -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::simd_div; #[repr(simd)] #[allow(non_camel_case_types)] @@ -19,10 +20,6 @@ impl f32x2 { } } -extern "platform-intrinsic" { - fn simd_div(x: T, y: T) -> T; -} - #[kani::proof] fn test_simd_div() { let dividends = f32x2::new_with(|| { diff --git a/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs b/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs index c97e96896bcf..e64498e20242 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs @@ -2,7 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Checks that the `simd_rem` intrinsic returns the expected results for floating point numbers. -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::simd_rem; #[repr(simd)] #[allow(non_camel_case_types)] @@ -19,10 +20,6 @@ impl f32x2 { } } -extern "platform-intrinsic" { - fn simd_rem(x: T, y: T) -> T; -} - #[kani::proof] fn test_simd_rem() { let dividends = f32x2::new_with(|| { diff --git a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs index 6d822a18bdc1..9b6870e40004 100644 --- a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs +++ b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs @@ -3,7 +3,8 @@ //! Checks that `simd_shuffle` and `simd_shuffleN` (where `N` is a length) are //! supported and return the expected results. -#![feature(repr_simd, platform_intrinsics)] +#![feature(repr_simd, core_intrinsics)] +use std::intrinsics::simd::simd_shuffle; #[repr(simd)] #[allow(non_camel_case_types)] @@ -15,10 +16,6 @@ pub struct i64x2(i64, i64); #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x4(i64, i64, i64, i64); -extern "platform-intrinsic" { - fn simd_shuffle(x: T, y: T, idx: U) -> V; -} - #[kani::proof] fn main() { { diff --git a/tests/kani/SIMD/simd_float_ops_fixme.rs b/tests/kani/SIMD/simd_float_ops_fixme.rs index d258a2119eca..6b53d95d554a 100644 --- a/tests/kani/SIMD/simd_float_ops_fixme.rs +++ b/tests/kani/SIMD/simd_float_ops_fixme.rs @@ -4,14 +4,10 @@ //! Ensure we can handle SIMD defined in the standard library //! FIXME: #![allow(non_camel_case_types)] -#![feature(repr_simd, platform_intrinsics, portable_simd)] +#![feature(repr_simd, core_intrinsics, portable_simd)] +use std::intrinsics::simd::simd_add; use std::simd::f32x4; -extern "platform-intrinsic" { - fn simd_add(x: T, y: T) -> T; - fn simd_eq(x: T, y: T) -> U; -} - #[repr(simd)] #[derive(Clone, PartialEq, kani::Arbitrary)] pub struct f32x2(f32, f32); diff --git a/tools/bookrunner/librustdoc/doctest.rs b/tools/bookrunner/librustdoc/doctest.rs index cf0fdc106e38..8d4c8c5eda5c 100644 --- a/tools/bookrunner/librustdoc/doctest.rs +++ b/tools/bookrunner/librustdoc/doctest.rs @@ -65,6 +65,7 @@ pub fn make_test( // crate already is included. let result = rustc_driver::catch_fatal_errors(|| { rustc_span::create_session_if_not_set_then(edition, |_| { + use rustc_errors::emitter::stderr_destination; use rustc_errors::emitter::{Emitter, HumanEmitter}; use rustc_errors::DiagCtxt; use rustc_parse::maybe_new_parser_from_source_str; @@ -81,14 +82,14 @@ pub fn make_test( let fallback_bundle = rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false); - supports_color = HumanEmitter::stderr(ColorConfig::Auto, fallback_bundle.clone()) - .diagnostic_width(Some(80)) - .supports_color(); + supports_color = + HumanEmitter::new(stderr_destination(ColorConfig::Auto), fallback_bundle.clone()) + .diagnostic_width(Some(80)) + .supports_color(); let emitter = HumanEmitter::new(Box::new(io::sink()), fallback_bundle); - // FIXME(misdreavus): pass `-Z treat-err-as-bug` to the doctest parser - let handler = DiagCtxt::with_emitter(Box::new(emitter)); + let handler = DiagCtxt::new(Box::new(emitter)); let sess = ParseSess::with_dcx(handler, sm); let mut found_main = false;