From 660b1f856c140c3f8d1260947a38c91b3b37a0b4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 3 Dec 2023 21:59:39 +0000 Subject: [PATCH 01/16] Update the rust toolchain to nightly-2023-12-03 Changes required due to: - rust-lang/rust@99ac405b96 Move MetadataLoader{,Dyn} to rustc_metadata. - rust-lang/rust@c997c6d822 Add more information to stable Instance --- .../src/codegen_cprover_gotoc/compiler_interface.rs | 2 +- kani-compiler/src/kani_middle/analysis.rs | 1 - kani-compiler/src/kani_middle/reachability.rs | 5 ++--- kani-driver/src/concrete_playback/test_generator.rs | 2 +- rust-toolchain.toml | 2 +- 5 files changed, 5 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index df472518c9a3..720e9d8ab423 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -40,7 +40,7 @@ use rustc_middle::mir::mono::MonoItem; use rustc_middle::ty::TyCtxt; use rustc_middle::util::Providers; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; -use rustc_session::cstore::MetadataLoaderDyn; +use rustc_metadata::creader::MetadataLoaderDyn; use rustc_session::output::out_filename; use rustc_session::Session; use rustc_smir::rustc_internal; diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index 011907c14ea4..b23fb99f83ff 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -151,7 +151,6 @@ impl From<&Terminator> for Key { TerminatorKind::Assert { .. } => Key("Assert"), TerminatorKind::Call { .. } => Key("Call"), TerminatorKind::Drop { .. } => Key("Drop"), - TerminatorKind::CoroutineDrop => Key("CoroutineDrop"), TerminatorKind::Goto { .. } => Key("Goto"), TerminatorKind::InlineAsm { .. } => Key("InlineAsm"), TerminatorKind::Resume { .. } => Key("Resume"), diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index d56b7b5db65d..216feb66fb87 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -266,7 +266,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { /// Collect an instance depending on how it is used (invoked directly or via fn_ptr). fn collect_instance(&mut self, instance: Instance, is_direct_call: bool) { let should_collect = match instance.kind { - InstanceKind::Virtual | InstanceKind::Intrinsic => { + InstanceKind::Virtual { .. } | InstanceKind::Intrinsic => { // Instance definition has no body. assert!(is_direct_call, "Expected direct call {instance:?}"); false @@ -453,8 +453,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => { // We generate code for this without invoking any lang item. } - TerminatorKind::CoroutineDrop { .. } - | TerminatorKind::Goto { .. } + TerminatorKind::Goto { .. } | TerminatorKind::SwitchInt { .. } | TerminatorKind::Resume | TerminatorKind::Return diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 492369fb32eb..53c3a92dd94c 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -163,7 +163,7 @@ impl KaniSession { let mut curr_line_num = 0; // Use a buffered reader/writer to generate the unit test line by line - for line in source_reader.lines().flatten() { + for line in source_reader.lines().map_while(Result::ok) { curr_line_num += 1; writeln!(temp_file, "{line}")?; if curr_line_num == proof_harness_end_line { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index e016b6b50492..1399eae195ec 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-12-01" +channel = "nightly-2023-12-03" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From fa0e7584439294dfbc0c61eff1f1c45a112df2ee Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 3 Dec 2023 22:31:49 +0000 Subject: [PATCH 02/16] fmt --- kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 720e9d8ab423..7b94dad06db4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -33,6 +33,7 @@ use rustc_data_structures::temp_dir::MaybeTempDir; use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; use rustc_hir::def_id::LOCAL_CRATE; use rustc_hir::definitions::DefPathHash; +use rustc_metadata::creader::MetadataLoaderDyn; use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; @@ -40,7 +41,6 @@ use rustc_middle::mir::mono::MonoItem; use rustc_middle::ty::TyCtxt; use rustc_middle::util::Providers; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; -use rustc_metadata::creader::MetadataLoaderDyn; use rustc_session::output::out_filename; use rustc_session::Session; use rustc_smir::rustc_internal; From 86c81b0095da39adb700dbce85d07e7d449de2c1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Dec 2023 22:51:12 +0000 Subject: [PATCH 03/16] portable-simd no longer provides a ToBitMask trait --- tests/kani/SIMD/portable_simd.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/kani/SIMD/portable_simd.rs b/tests/kani/SIMD/portable_simd.rs index c8995de410e0..a368c7060e4e 100644 --- a/tests/kani/SIMD/portable_simd.rs +++ b/tests/kani/SIMD/portable_simd.rs @@ -4,7 +4,7 @@ //! Ensure we have basic support of portable SIMD. #![feature(portable_simd)] -use std::simd::{mask32x4, u64x16, ToBitMask}; +use std::simd::{mask32x4, u64x16}; #[kani::proof] fn check_sum_any() { From ba6b95e20b3e3add97d9c40a1462f5524a7ae6f5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Dec 2023 22:57:03 +0000 Subject: [PATCH 04/16] Also drop unit test of our stub that uses ToBitMask --- library/kani/src/models/mod.rs | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 8b3f771756dc..e44323f355cb 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -184,20 +184,6 @@ mod test { check_bitmask::<_, [u8; 9], i128, 70>(CustomMask([-1i128; 70])); } - /// Compare the value returned by our model and the portable simd representation. - fn check_portable_bitmask(mask: T) - where - T: ToBitMask + Clone, - T::BitMask: Debug + PartialEq, - E: kani_intrinsic::MaskElement, - [u8; kani_intrinsic::mask_len(LANES)]: Sized, - { - assert_eq!( - unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) }, - mask.to_bitmask() - ); - } - /// Compare the value returned by our model and the simd_bitmask intrinsic. fn check_bitmask(mask: T) where From cdf13e8f1bae5f5ccb6733e2305457324f5f8149 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Dec 2023 22:59:55 +0000 Subject: [PATCH 05/16] Revert "Also drop unit test of our stub that uses ToBitMask" This reverts commit ba6b95e20b3e3add97d9c40a1462f5524a7ae6f5. --- library/kani/src/models/mod.rs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index e44323f355cb..8b3f771756dc 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -184,6 +184,20 @@ mod test { check_bitmask::<_, [u8; 9], i128, 70>(CustomMask([-1i128; 70])); } + /// Compare the value returned by our model and the portable simd representation. + fn check_portable_bitmask(mask: T) + where + T: ToBitMask + Clone, + T::BitMask: Debug + PartialEq, + E: kani_intrinsic::MaskElement, + [u8; kani_intrinsic::mask_len(LANES)]: Sized, + { + assert_eq!( + unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) }, + mask.to_bitmask() + ); + } + /// Compare the value returned by our model and the simd_bitmask intrinsic. fn check_bitmask(mask: T) where From 6207f88af359b3b0a5d91850d6d00f20256f7d1e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Dec 2023 23:01:05 +0000 Subject: [PATCH 06/16] Fix with u64 --- library/kani/src/models/mod.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 8b3f771756dc..a790d5e9645e 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -187,13 +187,11 @@ mod test { /// Compare the value returned by our model and the portable simd representation. fn check_portable_bitmask(mask: T) where - T: ToBitMask + Clone, - T::BitMask: Debug + PartialEq, E: kani_intrinsic::MaskElement, [u8; kani_intrinsic::mask_len(LANES)]: Sized, { assert_eq!( - unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) }, + unsafe { kani_intrinsic::simd_bitmask::<_, u64, E, LANES>(mask.clone()) }, mask.to_bitmask() ); } From fcae824acaecb00ec69540655deb9d2ac016f2b3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Dec 2023 23:43:14 +0000 Subject: [PATCH 07/16] Compiles, test still fails --- library/kani/src/models/mod.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index a790d5e9645e..a21cb1c5ab37 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -185,8 +185,10 @@ mod test { } /// Compare the value returned by our model and the portable simd representation. - fn check_portable_bitmask(mask: T) + fn check_portable_bitmask(mask: Mask) where + T: std::simd::MaskElement, + LaneCount: SupportedLaneCount, E: kani_intrinsic::MaskElement, [u8; kani_intrinsic::mask_len(LANES)]: Sized, { From d6adfd0ea04b1ba0b7d12218ade706a849787de6 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 5 Dec 2023 08:08:11 +0000 Subject: [PATCH 08/16] Update stubs to match upstream SIMD bitmask changes --- library/kani/src/models/mod.rs | 28 +++++++++++++--------------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index a21cb1c5ab37..199c8c69209e 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -69,11 +69,11 @@ mod intrinsics { } #[cfg(target_endian = "little")] - unsafe fn simd_bitmask_impl(input: &[T; LANES]) -> [u8; mask_len(LANES)] + unsafe fn simd_bitmask_impl(input: &[T; LANES]) -> [u8; MASK_LEN] where T: MaskElement, { - let mut mask_array = [0; mask_len(LANES)]; + let mut mask_array = [0; MASK_LEN]; for lane in (0..input.len()).rev() { let byte = lane / 8; let mask = &mut mask_array[byte]; @@ -99,14 +99,13 @@ mod intrinsics { #[rustc_diagnostic_item = "KaniModelSimdBitmask"] pub(super) unsafe fn simd_bitmask(input: T) -> U where - [u8; mask_len(LANES)]: Sized, + [u8; size_of::()]: Sized, E: MaskElement, { // These checks are compiler sanity checks to ensure we are not doing anything invalid. - assert_eq!( - size_of::(), - size_of::<[u8; mask_len(LANES)]>(), - "Expected size of return type and mask lanes to match", + assert!( + size_of::() >= mask_len(LANES), + "Expected size of return type to be greater or equal to the mask lanes", ); assert_eq!( size_of::(), @@ -115,8 +114,8 @@ mod intrinsics { ); let data = &*(&input as *const T as *const [E; LANES]); - let mask = simd_bitmask_impl(data); - (&mask as *const [u8; mask_len(LANES)] as *const U).read() + let mask = simd_bitmask_impl::() }>(data); + (&mask as *const [u8; size_of::()] as *const U).read() } /// Structure used for sanity check our parameters. @@ -127,7 +126,7 @@ mod intrinsics { #[cfg(test)] mod test { use super::intrinsics as kani_intrinsic; - use std::{fmt::Debug, simd::*}; + use std::{fmt::Debug, simd::*, mem::size_of}; extern "platform-intrinsic" { fn simd_bitmask(x: T) -> U; @@ -155,10 +154,10 @@ mod test { /// Tests that the model correctly fails if the size parameter of the mask doesn't match the /// expected number of bytes in the representation. #[test] - #[should_panic(expected = "Expected size of return type and mask lanes to match")] + #[should_panic(expected = "Expected size of return type to be greater or equal to the mask lanes")] fn test_invalid_generics() { - let mask = mask32x16::splat(false); - assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, u16, i32, 2>(mask) }, u16::MAX); + let mask = mask32x32::splat(false); + assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, u8, i32, 32>(mask) }, u8::MAX); } /// Test that the `simd_bitmask` model is equivalent to the intrinsic for a few random values. @@ -190,7 +189,6 @@ mod test { T: std::simd::MaskElement, LaneCount: SupportedLaneCount, E: kani_intrinsic::MaskElement, - [u8; kani_intrinsic::mask_len(LANES)]: Sized, { assert_eq!( unsafe { kani_intrinsic::simd_bitmask::<_, u64, E, LANES>(mask.clone()) }, @@ -204,7 +202,7 @@ mod test { T: Clone, U: PartialEq + Debug, E: kani_intrinsic::MaskElement, - [u8; kani_intrinsic::mask_len(LANES)]: Sized, + [u8; size_of::()]: Sized, { assert_eq!( unsafe { kani_intrinsic::simd_bitmask::<_, U, E, LANES>(mask.clone()) }, From 606d96dda843a7cce7b2d3226eea9cf9e334541e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Dec 2023 08:09:30 +0000 Subject: [PATCH 09/16] fmt --- library/kani/src/models/mod.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 199c8c69209e..e63e819ead9d 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -69,7 +69,9 @@ mod intrinsics { } #[cfg(target_endian = "little")] - unsafe fn simd_bitmask_impl(input: &[T; LANES]) -> [u8; MASK_LEN] + unsafe fn simd_bitmask_impl( + input: &[T; LANES], + ) -> [u8; MASK_LEN] where T: MaskElement, { @@ -126,7 +128,7 @@ mod intrinsics { #[cfg(test)] mod test { use super::intrinsics as kani_intrinsic; - use std::{fmt::Debug, simd::*, mem::size_of}; + use std::{fmt::Debug, mem::size_of, simd::*}; extern "platform-intrinsic" { fn simd_bitmask(x: T) -> U; @@ -154,7 +156,9 @@ mod test { /// Tests that the model correctly fails if the size parameter of the mask doesn't match the /// expected number of bytes in the representation. #[test] - #[should_panic(expected = "Expected size of return type to be greater or equal to the mask lanes")] + #[should_panic( + expected = "Expected size of return type to be greater or equal to the mask lanes" + )] fn test_invalid_generics() { let mask = mask32x32::splat(false); assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, u8, i32, 32>(mask) }, u8::MAX); From 9f2d97b3325aa5009f28dc323f83e4acec65af1b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Dec 2023 08:43:08 +0000 Subject: [PATCH 10/16] validate_instance: make sure we actually have a body --- kani-compiler/src/kani_middle/stubbing/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 03298456c522..41ee18c80efc 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -51,7 +51,7 @@ pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool { checker.visit_body(&item.body()); checker.is_valid() } else { - true + instance.body().is_some() } } From d00c43703e0a1f7dea886c3000d1bdbd9f74f808 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 6 Dec 2023 11:25:07 -0800 Subject: [PATCH 11/16] Revert "validate_instance: make sure we actually have a body" This reverts commit 9f2d97b3325aa5009f28dc323f83e4acec65af1b. --- kani-compiler/src/kani_middle/stubbing/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 41ee18c80efc..03298456c522 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -51,7 +51,7 @@ pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool { checker.visit_body(&item.body()); checker.is_valid() } else { - instance.body().is_some() + true } } From 505700aa8c4605187cc07919830991cbe6075762 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 6 Dec 2023 11:30:18 -0800 Subject: [PATCH 12/16] Work around issue with is_foreign_item --- kani-compiler/src/kani_middle/reachability.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 216feb66fb87..9e35e273bb66 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -485,7 +485,10 @@ fn to_fingerprint(tcx: TyCtxt, item: &InternalMonoItem) -> Fingerprint { /// Return whether we should include the item into codegen. fn should_codegen_locally(instance: &Instance) -> bool { - !instance.is_foreign_item() + // TODO: This should only check is_foreign_item() or even `has_body()`. + // We need https://github.com/rust-lang/rust/pull/118681 to land first. + //!instance.is_foreign_item() + instance.body().is_some() } fn collect_alloc_items(alloc_id: AllocId) -> Vec { From ff40897f12214837e4bad05f6e7160347791e8fb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 6 Dec 2023 12:53:34 -0800 Subject: [PATCH 13/16] Revert model change and add new test The change was only needed in the test case, since the way portable simd invokes the intrinsic is still the same My current hypothesis is that the current failure could be an issue with simd_shuffle --- library/kani/src/models/mod.rs | 60 ++++++++++++++++++++------------ tests/kani/SIMD/portable_simd.rs | 10 +++++- 2 files changed, 46 insertions(+), 24 deletions(-) diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index e63e819ead9d..26a1c4563c54 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -69,13 +69,11 @@ mod intrinsics { } #[cfg(target_endian = "little")] - unsafe fn simd_bitmask_impl( - input: &[T; LANES], - ) -> [u8; MASK_LEN] + unsafe fn simd_bitmask_impl(input: &[T; LANES]) -> [u8; mask_len(LANES)] where T: MaskElement, { - let mut mask_array = [0; MASK_LEN]; + let mut mask_array = [0; mask_len(LANES)]; for lane in (0..input.len()).rev() { let byte = lane / 8; let mask = &mut mask_array[byte]; @@ -101,13 +99,14 @@ mod intrinsics { #[rustc_diagnostic_item = "KaniModelSimdBitmask"] pub(super) unsafe fn simd_bitmask(input: T) -> U where - [u8; size_of::()]: Sized, + [u8; mask_len(LANES)]: Sized, E: MaskElement, { // These checks are compiler sanity checks to ensure we are not doing anything invalid. - assert!( - size_of::() >= mask_len(LANES), - "Expected size of return type to be greater or equal to the mask lanes", + assert_eq!( + size_of::(), + size_of::<[u8; mask_len(LANES)]>(), + "Expected size of return type and mask lanes to match", ); assert_eq!( size_of::(), @@ -116,8 +115,8 @@ mod intrinsics { ); let data = &*(&input as *const T as *const [E; LANES]); - let mask = simd_bitmask_impl::() }>(data); - (&mask as *const [u8; size_of::()] as *const U).read() + let mask = simd_bitmask_impl(data); + (&mask as *const [u8; mask_len(LANES)] as *const U).read() } /// Structure used for sanity check our parameters. @@ -128,7 +127,7 @@ mod intrinsics { #[cfg(test)] mod test { use super::intrinsics as kani_intrinsic; - use std::{fmt::Debug, mem::size_of, simd::*}; + use std::{fmt::Debug, simd::*}; extern "platform-intrinsic" { fn simd_bitmask(x: T) -> U; @@ -138,8 +137,8 @@ mod test { /// masks with lanes represented using i16. #[test] fn test_bitmask_i16() { - check_portable_bitmask::<_, i16, 16>(mask16x16::splat(false)); - check_portable_bitmask::<_, i16, 16>(mask16x16::splat(true)); + check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(false)); + check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(true)); } /// Tests that the model correctly fails if an invalid value is given. @@ -156,23 +155,21 @@ mod test { /// Tests that the model correctly fails if the size parameter of the mask doesn't match the /// expected number of bytes in the representation. #[test] - #[should_panic( - expected = "Expected size of return type to be greater or equal to the mask lanes" - )] + #[should_panic(expected = "Expected size of return type and mask lanes to match")] fn test_invalid_generics() { - let mask = mask32x32::splat(false); - assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, u8, i32, 32>(mask) }, u8::MAX); + let mask = mask32x16::splat(false); + assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, u16, i32, 2>(mask) }, u16::MAX); } /// Test that the `simd_bitmask` model is equivalent to the intrinsic for a few random values. /// These values shouldn't be symmetric and ensure that we also handle endianness correctly. #[test] fn test_bitmask_i32() { - check_portable_bitmask::<_, i32, 8>(mask32x8::from([ + check_portable_bitmask::<_, i32, 8, u8>(mask32x8::from([ true, true, false, true, false, false, false, true, ])); - check_portable_bitmask::<_, i32, 4>(mask32x4::from([true, false, false, true])); + check_portable_bitmask::<_, i32, 4, u8>(mask32x4::from([true, false, false, true])); } #[repr(simd)] @@ -188,14 +185,16 @@ mod test { } /// Compare the value returned by our model and the portable simd representation. - fn check_portable_bitmask(mask: Mask) + fn check_portable_bitmask(mask: Mask) where T: std::simd::MaskElement, LaneCount: SupportedLaneCount, E: kani_intrinsic::MaskElement, + [u8; kani_intrinsic::mask_len(LANES)]: Sized, + u64: From, { assert_eq!( - unsafe { kani_intrinsic::simd_bitmask::<_, u64, E, LANES>(mask.clone()) }, + unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask.clone())) }, mask.to_bitmask() ); } @@ -206,11 +205,26 @@ mod test { T: Clone, U: PartialEq + Debug, E: kani_intrinsic::MaskElement, - [u8; size_of::()]: Sized, + [u8; kani_intrinsic::mask_len(LANES)]: Sized, { assert_eq!( unsafe { kani_intrinsic::simd_bitmask::<_, U, E, LANES>(mask.clone()) }, unsafe { simd_bitmask::(mask) } ); } + + /// Similar to portable simd_harness. + #[test] + fn check_mask_harness() { + // From array doesn't work either. Manually build [false, true, false, true] + let mut mask = mask32x4::splat(false); + mask.set(1, true); + mask.set(3, true); + let bitmask = mask.to_bitmask(); + assert_eq!(bitmask, 0b1010); + + let kani_mask = unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) }; + assert_eq!(kani_mask, bitmask); + } + } diff --git a/tests/kani/SIMD/portable_simd.rs b/tests/kani/SIMD/portable_simd.rs index a368c7060e4e..0a0b6d435d46 100644 --- a/tests/kani/SIMD/portable_simd.rs +++ b/tests/kani/SIMD/portable_simd.rs @@ -4,7 +4,7 @@ //! Ensure we have basic support of portable SIMD. #![feature(portable_simd)] -use std::simd::{mask32x4, u64x16}; +use std::simd::{mask32x4, u32x4, u64x16}; #[kani::proof] fn check_sum_any() { @@ -23,3 +23,11 @@ fn check_mask() { let bitmask = mask.to_bitmask(); assert_eq!(bitmask, 0b1010); } + +#[kani::proof] +fn check_resize() { + let x = u32x4::from_array([0, 1, 2, 3]); + assert_eq!(x.resize::<8>(9).to_array(), [0, 1, 2, 3, 9, 9, 9, 9]); + assert_eq!(x.resize::<2>(9).to_array(), [0, 1]); + +} From 6f1569dd82a99fe59700fbf9b258128958be5d36 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 7 Dec 2023 22:02:33 +0000 Subject: [PATCH 14/16] Fix selection in `simd_shuffle` to use input len --- kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 5d60f15f69a5..11e4721dfb31 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1729,7 +1729,7 @@ impl<'tcx> GotocCtx<'tcx> { // [u32; n]: translated wrapped in a struct let indexes = fargs.remove(0); - let (_, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx); + let (in_type_len, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx); let (ret_type_len, ret_type_subtype) = rust_ret_type.simd_size_and_type(self.tcx); if ret_type_len != n { let err_msg = format!( @@ -1749,7 +1749,7 @@ impl<'tcx> GotocCtx<'tcx> { // An unsigned type here causes an invariant violation in CBMC. // Issue: https://github.com/diffblue/cbmc/issues/6298 let st_rep = Type::ssize_t(); - let n_rep = Expr::int_constant(n, st_rep.clone()); + let n_rep = Expr::int_constant(in_type_len, st_rep.clone()); // P = indexes.expanded_map(v -> if v < N then vec1[v] else vec2[v-N]) let elems = (0..n) From fa92da29f014ffe1e26fe759c2c67d0257bc5b25 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 7 Dec 2023 22:22:50 +0000 Subject: [PATCH 15/16] Add more tests (`simd_shuffle`/`simd_swizzle`) --- library/kani/src/models/mod.rs | 4 +-- tests/kani/Intrinsics/SIMD/Shuffle/main.rs | 10 +++++++ tests/kani/SIMD/portable_simd.rs | 1 - tests/kani/SIMD/swizzle.rs | 31 ++++++++++++++++++++++ 4 files changed, 43 insertions(+), 3 deletions(-) create mode 100644 tests/kani/SIMD/swizzle.rs diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 26a1c4563c54..194f220595c0 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -223,8 +223,8 @@ mod test { let bitmask = mask.to_bitmask(); assert_eq!(bitmask, 0b1010); - let kani_mask = unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) }; + let kani_mask = + unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) }; assert_eq!(kani_mask, bitmask); } - } diff --git a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs index b3b0d41f0dff..6d822a18bdc1 100644 --- a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs +++ b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs @@ -45,3 +45,13 @@ fn main() { assert!(c == i64x4(2, 4, 6, 8)); } } + +#[kani::proof] +fn check_shuffle() { + { + let y = i64x2(0, 1); + let z = i64x2(1, 2); + const I: [u32; 4] = [1, 2, 0, 3]; + let _x: i64x4 = unsafe { simd_shuffle(y, z, I) }; + } +} diff --git a/tests/kani/SIMD/portable_simd.rs b/tests/kani/SIMD/portable_simd.rs index 0a0b6d435d46..64cfb4b1fcf3 100644 --- a/tests/kani/SIMD/portable_simd.rs +++ b/tests/kani/SIMD/portable_simd.rs @@ -29,5 +29,4 @@ fn check_resize() { let x = u32x4::from_array([0, 1, 2, 3]); assert_eq!(x.resize::<8>(9).to_array(), [0, 1, 2, 3, 9, 9, 9, 9]); assert_eq!(x.resize::<2>(9).to_array(), [0, 1]); - } diff --git a/tests/kani/SIMD/swizzle.rs b/tests/kani/SIMD/swizzle.rs new file mode 100644 index 000000000000..26781743dbfa --- /dev/null +++ b/tests/kani/SIMD/swizzle.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Ensure we can safely swizzle between SIMD types of different sizes. +#![feature(portable_simd)] + +use std::simd::{simd_swizzle, u32x4, u32x8}; + +#[kani::proof] +fn harness_from_u32x4_to_u32x4() { + let a = u32x4::from_array([0, 1, 2, 3]); + let b = u32x4::from_array([4, 5, 6, 7]); + let r: u32x4 = simd_swizzle!(a, b, [0, 1, 6, 7]); + assert_eq!(r.to_array(), [0, 1, 6, 7]); +} + +#[kani::proof] +fn harness_from_u32x4_to_u32x8() { + let a = u32x4::from_array([0, 1, 2, 3]); + let b = u32x4::from_array([4, 5, 6, 7]); + let r: u32x8 = simd_swizzle!(a, b, [0, 1, 2, 3, 4, 5, 6, 7]); + assert_eq!(r.to_array(), [0, 1, 2, 3, 4, 5, 6, 7]); +} + +#[kani::proof] +fn harness_from_u32x8_to_u32x4() { + let a = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]); + let b = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]); + let r: u32x4 = simd_swizzle!(a, b, [0, 1, 2, 3]); + assert_eq!(r.to_array(), [0, 1, 2, 3]); +} From 9be3d1fa4766048bb8d80c66813d37e98e718c0d Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 7 Dec 2023 17:49:40 -0800 Subject: [PATCH 16/16] Regression now passes - Use internal to go around is_foreign_item() issue - Update tests after an issue: https://github.com/rust-lang/rust/pull/116915 - Update the toolchain --- kani-compiler/src/kani_middle/reachability.rs | 11 ++-- kani-compiler/src/kani_middle/stubbing/mod.rs | 1 + rust-toolchain.toml | 2 +- tests/expected/any_vec/exact_length.expected | 8 +-- tests/expected/any_vec/out_bounds.expected | 63 ++----------------- 5 files changed, 16 insertions(+), 69 deletions(-) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 9e35e273bb66..a8e7d9fe3f83 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -153,7 +153,11 @@ impl<'tcx> MonoItemsCollector<'tcx> { /// instruction looking for the items that should be included in the compilation. fn reachable_items(&mut self) { while let Some(to_visit) = self.queue.pop() { - if !self.collected.contains(&to_visit) { + // TODO: This should only check is_foreign_item() or even `has_body()`. + // We need https://github.com/rust-lang/rust/pull/118681 to land first. + if !self.collected.contains(&to_visit) + && !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id()) + { self.collected.insert(to_visit.clone()); let next_items = match &to_visit { MonoItem::Fn(instance) => self.visit_fn(*instance), @@ -485,10 +489,7 @@ fn to_fingerprint(tcx: TyCtxt, item: &InternalMonoItem) -> Fingerprint { /// Return whether we should include the item into codegen. fn should_codegen_locally(instance: &Instance) -> bool { - // TODO: This should only check is_foreign_item() or even `has_body()`. - // We need https://github.com/rust-lang/rust/pull/118681 to land first. - //!instance.is_foreign_item() - instance.body().is_some() + !instance.is_foreign_item() } fn collect_alloc_items(alloc_id: AllocId) -> Vec { diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 03298456c522..6af0b442c8d4 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -46,6 +46,7 @@ pub fn harness_stub_map( pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool { let internal_instance = rustc_internal::internal(instance); if get_stub(tcx, internal_instance.def_id()).is_some() { + debug!(?instance, "validate_instance"); let item = CrateItem::try_from(instance).unwrap(); let mut checker = StubConstChecker::new(tcx, internal_instance, item); checker.visit_body(&item.body()); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 1399eae195ec..2bdb5cdf793a 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-12-03" +channel = "nightly-2023-12-07" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/any_vec/exact_length.expected b/tests/expected/any_vec/exact_length.expected index 641db7843ff1..082f3fb61570 100644 --- a/tests/expected/any_vec/exact_length.expected +++ b/tests/expected/any_vec/exact_length.expected @@ -1,12 +1,12 @@ Checking harness check_access_length_17... -Failed Checks: dereference failure: pointer outside object bounds\ -in check_access_length_17 +Failed Checks: assumption failed\ +in >::get_unchecked Checking harness check_access_length_zero... -Failed Checks: dereference failure: pointer outside object bounds\ -in check_access_length_zero +Failed Checks: assumption failed\ +in >::get_unchecked Verification failed for - check_access_length_17 Verification failed for - check_access_length_zero diff --git a/tests/expected/any_vec/out_bounds.expected b/tests/expected/any_vec/out_bounds.expected index 167fefe6d6f4..24121aee4ee8 100644 --- a/tests/expected/any_vec/out_bounds.expected +++ b/tests/expected/any_vec/out_bounds.expected @@ -1,61 +1,6 @@ -check_always_out_bounds::check_0.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer NULL"\ -function check_always_out_bounds::check_0 - -check_always_out_bounds::check_0.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_0 - -check_always_out_bounds::check_0.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: invalid integer address"\ -function check_always_out_bounds::check_0 - -check_always_out_bounds::check_1.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_1 - -check_always_out_bounds::check_2.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_2 - -check_always_out_bounds::check_3.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_3 - -check_always_out_bounds::check_4.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_4 - -check_always_out_bounds::check_5.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_5 - -check_always_out_bounds::check_6.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_6 - -check_always_out_bounds::check_7.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_7 - -check_always_out_bounds::check_8.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_8 - -check_always_out_bounds::check_9.cover\ -Status: UNREACHABLE\ -Description: "cover condition: *val == 0"\ -function check_always_out_bounds::check_9 +Checking harness check_always_out_bounds... +Failed Checks: assumption failed +in >::get_unchecked +Verification failed for - check_always_out_bounds