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) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index df472518c9a3..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_session::cstore::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..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), @@ -266,7 +270,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 +457,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-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/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/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 8b3f771756dc..194f220595c0 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -137,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. @@ -165,11 +165,11 @@ mod test { /// 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)] @@ -185,15 +185,16 @@ 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: ToBitMask + Clone, - T::BitMask: Debug + PartialEq, + 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::<_, T::BitMask, E, LANES>(mask.clone()) }, + unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask.clone())) }, mask.to_bitmask() ); } @@ -211,4 +212,19 @@ mod test { 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/rust-toolchain.toml b/rust-toolchain.toml index e016b6b50492..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-01" +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 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 c8995de410e0..64cfb4b1fcf3 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, u32x4, u64x16}; #[kani::proof] fn check_sum_any() { @@ -23,3 +23,10 @@ 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]); +} 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]); +}