diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index fbb9cc90cdaa..4506680158ca 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -406,9 +406,9 @@ impl<'tcx> GotocCtx<'tcx> { proj: ProjectionElem>, ) -> Result, UnimplementedData> { let before = before?; + trace!(?before, ?proj, "codegen_projection"); match proj { ProjectionElem::Deref => { - trace!(?before, ?proj, "codegen_projection"); let base_type = before.mir_typ(); let inner_goto_expr = if base_type.is_box() { self.deref_box(before.goto_expr) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index dcdf6a8bfaf9..9535e74152ad 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -193,7 +193,7 @@ impl CodegenBackend for GotocCodegenBackend { } fn provide_extern(&self, providers: &mut ExternProviders) { - provide::provide_extern(providers); + provide::provide_extern(providers, &self.queries.lock().unwrap()); } fn print_version(&self) { diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs new file mode 100644 index 000000000000..fd296b28d757 --- /dev/null +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -0,0 +1,108 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains a MIR pass that replaces some intrinsics by rust intrinsics models as +//! well as validation logic that can only be added during monomorphization. +use rustc_index::IndexVec; +use rustc_middle::mir::{interpret::ConstValue, Body, ConstantKind, Operand, TerminatorKind}; +use rustc_middle::mir::{Local, LocalDecl}; +use rustc_middle::ty::{self, Ty, TyCtxt}; +use rustc_middle::ty::{Const, GenericArgsRef}; +use rustc_span::symbol::{sym, Symbol}; +use tracing::{debug, trace}; + +pub struct ModelIntrinsics<'tcx> { + tcx: TyCtxt<'tcx>, + /// Local declarations of the function being transformed. + local_decls: IndexVec>, +} + +impl<'tcx> ModelIntrinsics<'tcx> { + /// Function that replace calls to some intrinsics that have a high level model in our library. + /// + /// For now, we only look at intrinsic calls, which are modelled by a terminator. + /// + /// However, this pass runs after lowering intrinsics, which may replace the terminator by + /// an intrinsic statement (non-diverging intrinsic). + pub fn run_pass(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) { + ModelIntrinsics { tcx, local_decls: body.local_decls.clone() }.transform(body) + } + + pub fn transform(&self, body: &mut Body<'tcx>) { + for block in body.basic_blocks.as_mut() { + let terminator = block.terminator_mut(); + if let TerminatorKind::Call { func, args, .. } = &mut terminator.kind { + let func_ty = func.ty(&self.local_decls, self.tcx); + if let Some((intrinsic_name, generics)) = resolve_rust_intrinsic(self.tcx, func_ty) + { + trace!(?func, ?intrinsic_name, "run_pass"); + if intrinsic_name == sym::simd_bitmask { + self.replace_simd_bitmask(func, args, generics) + } + } + } + } + } + + /// Change the function call to use the stubbed version. + /// We only replace calls if we can ensure the input has simd representation. + fn replace_simd_bitmask( + &self, + func: &mut Operand<'tcx>, + args: &[Operand<'tcx>], + gen_args: GenericArgsRef<'tcx>, + ) { + assert_eq!(args.len(), 1); + let tcx = self.tcx; + let arg_ty = args[0].ty(&self.local_decls, tcx); + if arg_ty.is_simd() { + // Get the stub definition. + let stub_id = tcx.get_diagnostic_item(Symbol::intern("KaniModelSimdBitmask")).unwrap(); + debug!(?func, ?stub_id, "replace_simd_bitmask"); + + // Get SIMD information from the type. + let (len, elem_ty) = simd_len_and_type(tcx, arg_ty); + debug!(?len, ?elem_ty, "replace_simd_bitmask Ok"); + + // Increment the list of generic arguments since our stub also takes element type and len. + let mut new_gen_args = Vec::from_iter(gen_args.iter()); + new_gen_args.push(elem_ty.into()); + new_gen_args.push(len.into()); + + let Operand::Constant(fn_def) = func else { unreachable!() }; + fn_def.literal = ConstantKind::from_value( + ConstValue::ZeroSized, + tcx.type_of(stub_id).instantiate(tcx, &new_gen_args), + ); + } else { + debug!(?arg_ty, "replace_simd_bitmask failed"); + } + } +} + +fn simd_len_and_type<'tcx>(tcx: TyCtxt<'tcx>, simd_ty: Ty<'tcx>) -> (Const<'tcx>, Ty<'tcx>) { + match simd_ty.kind() { + ty::Adt(def, args) => { + assert!(def.repr().simd(), "`simd_size_and_type` called on non-SIMD type"); + let variant = def.non_enum_variant(); + let f0_ty = variant.fields[0u32.into()].ty(tcx, args); + + match f0_ty.kind() { + ty::Array(elem_ty, len) => (*len, *elem_ty), + _ => (Const::from_target_usize(tcx, variant.fields.len() as u64), f0_ty), + } + } + _ => unreachable!("unexpected layout for simd type {simd_ty}"), + } +} + +fn resolve_rust_intrinsic<'tcx>( + tcx: TyCtxt<'tcx>, + func_ty: Ty<'tcx>, +) -> Option<(Symbol, GenericArgsRef<'tcx>)> { + if let ty::FnDef(def_id, args) = *func_ty.kind() { + if tcx.is_intrinsic(def_id) { + return Some((tcx.item_name(def_id), args)); + } + } + None +} diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 04fc2b67e26f..8fe4ab31d0ae 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -30,6 +30,7 @@ use self::attributes::KaniAttributes; pub mod analysis; pub mod attributes; pub mod coercion; +mod intrinsics; pub mod metadata; pub mod provide; pub mod reachability; diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index 54596cf27627..dbc2dba993b0 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -4,6 +4,7 @@ //! to run during code generation. For example, this can be used to hook up //! custom MIR transformations. +use crate::kani_middle::intrinsics::ModelIntrinsics; use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items}; use crate::kani_middle::stubbing; use crate::kani_queries::{QueryDb, ReachabilityType}; @@ -18,7 +19,7 @@ use rustc_middle::{ /// Sets up rustc's query mechanism to apply Kani's custom queries to code from /// the present crate. pub fn provide(providers: &mut Providers, queries: &QueryDb) { - if queries.reachability_analysis != ReachabilityType::None && !queries.build_std { + if should_override(queries) { // Don't override queries if we are only compiling our dependencies. providers.optimized_mir = run_mir_passes; if queries.stubbing_enabled { @@ -30,8 +31,15 @@ pub fn provide(providers: &mut Providers, queries: &QueryDb) { /// Sets up rustc's query mechanism to apply Kani's custom queries to code from /// external crates. -pub fn provide_extern(providers: &mut ExternProviders) { - providers.optimized_mir = run_mir_passes_extern; +pub fn provide_extern(providers: &mut ExternProviders, queries: &QueryDb) { + if should_override(queries) { + // Don't override queries if we are only compiling our dependencies. + providers.optimized_mir = run_mir_passes_extern; + } +} + +fn should_override(queries: &QueryDb) -> bool { + queries.reachability_analysis != ReachabilityType::None && !queries.build_std } /// Returns the optimized code for the external function associated with `def_id` by @@ -61,6 +69,8 @@ fn run_kani_mir_passes<'tcx>( tracing::debug!(?def_id, "Run Kani transformation passes"); let mut transformed_body = stubbing::transform(tcx, def_id, body); stubbing::transform_foreign_functions(tcx, &mut transformed_body); + // This should be applied after stubbing so user stubs take precedence. + ModelIntrinsics::run_pass(tcx, &mut transformed_body); tcx.arena.alloc(transformed_body) } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 5212b64a733f..d955e204a833 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -5,10 +5,16 @@ #![feature(register_tool)] #![register_tool(kanitool)] // Used for rustc_diagnostic_item. +// Note: We could use a kanitool attribute instead. #![feature(rustc_attrs)] // This is required for the optimized version of `any_array()` #![feature(generic_const_exprs)] #![allow(incomplete_features)] +// Used to model simd. +#![feature(repr_simd)] +// Features used for tests only. +#![cfg_attr(test, feature(platform_intrinsics, portable_simd))] +// Required for rustc_diagnostic_item #![allow(internal_features)] pub mod arbitrary; @@ -19,6 +25,8 @@ pub mod slice; pub mod tuple; pub mod vec; +mod models; + pub use arbitrary::Arbitrary; #[cfg(feature = "concrete_playback")] pub use concrete_playback::concrete_playback_run; diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs new file mode 100644 index 000000000000..38ab03fabc95 --- /dev/null +++ b/library/kani/src/models/mod.rs @@ -0,0 +1,214 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Contains definitions that Kani compiler may use to model functions that are not suitable for +//! verification or functions without a body, such as intrinsics. +//! +//! Note that these are models that Kani uses by default; thus, we keep them separate from stubs. + +// Definitions in this module are not meant to be visible to the end user, only the compiler. +#[allow(dead_code)] +mod intrinsics { + use std::fmt::Debug; + use std::mem::size_of; + + /// Similar definition to portable SIMD. + /// We cannot reuse theirs since TRUE and FALSE defs are private. + /// We leave this private today, since this is not necessarily a final solution, so we don't + /// want users relying on this. + /// Our definitions are also a bit more permissive to comply with the platform intrinsics. + pub(super) trait MaskElement: PartialEq + Debug { + const TRUE: Self; + const FALSE: Self; + } + + macro_rules! impl_element { + { $ty:ty } => { + impl MaskElement for $ty { + const TRUE: Self = -1; + const FALSE: Self = 0; + } + } + } + + macro_rules! impl_unsigned_element { + { $ty:ty } => { + impl MaskElement for $ty { + // Note that in the declaration of the intrinsic it is documented that the lane + // values should be -1 or 0: + // + // + // However, MIRI and the Rust compiler seems to accept unsigned values and they + // use their binary representation. Thus, that's what we use for now. + /// All bits are 1 which represents TRUE. + const TRUE: Self = <$ty>::MAX; + /// All bits are 0 which represents FALSE. + const FALSE: Self = 0; + } + } + } + + impl_element! { i8 } + impl_element! { i16 } + impl_element! { i32 } + impl_element! { i64 } + impl_element! { i128 } + impl_element! { isize } + + impl_unsigned_element! { u8 } + impl_unsigned_element! { u16 } + impl_unsigned_element! { u32 } + impl_unsigned_element! { u64 } + impl_unsigned_element! { u128 } + impl_unsigned_element! { usize } + + /// Calculate the minimum number of lanes to represent a mask + /// Logic similar to `bitmask_len` from `portable_simd`. + /// + pub(super) const fn mask_len(len: usize) -> usize { + (len + 7) / 8 + } + + #[cfg(target_endian = "little")] + unsafe fn simd_bitmask_impl(input: &[T; LANES]) -> [u8; mask_len(LANES)] + where + T: MaskElement, + { + 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]; + let shift_mask = *mask << 1; + *mask = if input[lane] == T::TRUE { + shift_mask | 0x1 + } else { + assert_eq!(input[lane], T::FALSE, "Masks values should either be 0 or -1"); + shift_mask + }; + } + mask_array + } + + /// Stub for simd_bitmask. + /// + /// It will reduce a simd vector (TxN), into an integer of size S (in bits), where S >= N. + /// Each bit of the output will represent a lane from the input. A lane value of all 0's will be + /// translated to 1b0, while all 1's will be translated to 1b1. + /// + /// In order to be able to do this pragmatically, we take additional parameters that are filled + /// by the compiler. + #[rustc_diagnostic_item = "KaniModelSimdBitmask"] + pub(super) unsafe fn simd_bitmask(input: T) -> U + where + [u8; mask_len(LANES)]: 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_eq!( + size_of::(), + size_of::>(), + "Expected size of input and lanes to match", + ); + + 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() + } + + /// Structure used for sanity check our parameters. + #[repr(simd)] + struct Simd([T; LANES]); +} + +#[cfg(test)] +mod test { + use super::intrinsics as kani_intrinsic; + 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] + fn test_bitmask_i16() { + check_portable_bitmask::<_, i16, 16>(mask16x16::splat(false)); + check_portable_bitmask::<_, i16, 16>(mask16x16::splat(true)); + } + + /// Tests that the model correctly fails if an invalid value is given. + #[test] + #[should_panic(expected = "Masks values should either be 0 or -1")] + fn test_invalid_bitmask() { + let invalid_mask = unsafe { mask32x16::from_int_unchecked(i32x16::splat(10)) }; + assert_eq!( + unsafe { kani_intrinsic::simd_bitmask::<_, u16, i32, 16>(invalid_mask) }, + u16::MAX + ); + } + + /// 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")] + fn test_invalid_generics() { + let mask = unsafe { 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([ + true, true, false, true, false, false, false, true, + ])); + + check_portable_bitmask::<_, i32, 4>(mask32x4::from([true, false, false, true])); + } + + #[repr(simd)] + #[derive(Clone, Debug)] + struct CustomMask([T; LANES]); + + /// Check that the bitmask model can handle odd size SIMD arrays. + /// Since the portable_simd restricts the number of lanes, we have to use our own custom SIMD. + #[test] + fn test_bitmask_odd_lanes() { + check_bitmask::<_, [u8; 3], i128, 23>(CustomMask([0i128; 23])); + 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 + T: Clone, + U: PartialEq + Debug, + E: kani_intrinsic::MaskElement, + [u8; kani_intrinsic::mask_len(LANES)]: Sized, + { + assert_eq!( + unsafe { kani_intrinsic::simd_bitmask::<_, U, E, LANES>(mask.clone()) }, + unsafe { simd_bitmask::(mask) } + ); + } +} diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 0567227672ad..f0d43656f55b 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -34,6 +34,7 @@ cargo test -p cprover_bindings cargo test -p kani-compiler cargo test -p kani-driver cargo test -p kani_metadata +cargo test -p kani --lib # skip doc tests. # Declare testing suite information (suite and mode) TESTS=( diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs b/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs new file mode 100644 index 000000000000..4d3293264b6e --- /dev/null +++ b/tests/kani/Intrinsics/SIMD/Operators/bitmask.rs @@ -0,0 +1,59 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that we support `simd_bitmask` intrinsic. +//! +//! 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(generic_const_exprs)] +#![feature(portable_simd)] +#![feature(core_intrinsics)] + +use std::fmt::Debug; + +extern "platform-intrinsic" { + fn simd_bitmask(x: T) -> U; +} + +#[repr(simd)] +#[derive(Clone, Debug)] +struct CustomMask([i32; LANES]); + +impl CustomMask { + fn as_array(&self) -> [i32; LANES] { + unsafe { *(&self.clone() as *const Self as *const [i32; LANES]) } + } +} + +impl kani::Arbitrary for CustomMask +where + [bool; LANES]: Sized + kani::Arbitrary, +{ + fn any() -> Self { + CustomMask(kani::any::<[bool; LANES]>().map(|v| if v { 0i32 } else { -1 })) + } +} + +#[kani::proof] +fn check_u8() { + let (true_lane, false_lane) = (-1, 0); + + // This should be the mask 0b1101 for little endian machines. + let input = CustomMask([true_lane, false_lane, true_lane, true_lane]); + let mask = unsafe { simd_bitmask::<_, u8>(input) }; + assert_eq!(mask, 0b1101); + + let input = CustomMask([true_lane; 25]); + let mask = unsafe { simd_bitmask::<_, u32>(input) }; + assert_eq!(mask, 0b1111111111111111111111111); +} + +#[kani::proof] +fn check_unsigned_bitmask() { + let mask = kani::any::>(); + let bitmask = unsafe { simd_bitmask::<_, u8>(mask.clone()) }; + assert_eq!(bitmask.count_ones() as usize, mask.as_array().iter().filter(|e| **e == -1).count()); + assert_eq!(bitmask.count_zeros() as usize, mask.as_array().iter().filter(|e| **e == 0).count()); +} diff --git a/tests/kani/SIMD/portable_simd.rs b/tests/kani/SIMD/portable_simd.rs index 9f7d0f536dcc..c8995de410e0 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::u64x16; +use std::simd::{mask32x4, u64x16, ToBitMask}; #[kani::proof] fn check_sum_any() { @@ -13,3 +13,13 @@ fn check_sum_any() { // Cannot compare them directly: https://github.com/model-checking/kani/issues/2632 assert_eq!((a + b).as_array(), b.as_array()); } + +#[kani::proof] +fn check_mask() { + // 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); +} diff --git a/tests/perf/hashset/expected b/tests/perf/hashset/expected new file mode 100644 index 000000000000..8ba783d580f9 --- /dev/null +++ b/tests/perf/hashset/expected @@ -0,0 +1 @@ +4 successfully verified harnesses, 0 failures, 4 total diff --git a/tests/perf/hashset/hash_set.rs b/tests/perf/hashset/hash_set.rs new file mode 100644 index 000000000000..fb29db5c7ed6 --- /dev/null +++ b/tests/perf/hashset/hash_set.rs @@ -0,0 +1,74 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --enable-stubbing --enable-unstable +//! Try to verify HashSet basic behavior. + +use std::collections::{hash_map::RandomState, HashSet}; +use std::mem::{size_of, size_of_val, transmute}; + +fn concrete_state() -> RandomState { + let keys: [u64; 2] = [0, 0]; + assert_eq!(size_of_val(&keys), size_of::()); + unsafe { transmute(keys) } +} + +#[kani::proof] +#[kani::stub(RandomState::new, concrete_state)] +#[kani::unwind(2)] +#[kani::solver(kissat)] +fn check_insert() { + let mut set: HashSet = HashSet::default(); + let first = kani::any(); + set.insert(first); + assert_eq!(set.len(), 1); + assert_eq!(set.iter().next(), Some(&first)); +} + +#[kani::proof] +#[kani::stub(RandomState::new, concrete_state)] +#[kani::unwind(2)] +#[kani::solver(kissat)] +fn check_contains() { + let first = kani::any(); + let mut set: HashSet = HashSet::from([first]); + assert!(set.contains(&first)); +} + +#[kani::proof] +#[kani::stub(RandomState::new, concrete_state)] +#[kani::unwind(2)] +fn check_contains_str() { + let mut set = HashSet::from(["s"]); + assert!(set.contains(&"s")); +} + +#[kani::proof] +#[kani::stub(RandomState::new, concrete_state)] +#[kani::unwind(2)] +#[kani::solver(kissat)] +fn check_insert_two_concrete() { + let mut set: HashSet = HashSet::default(); + let first = 10; + let second = 20; + set.insert(first); + set.insert(second); + assert_eq!(set.len(), 2); +} + +// too slow so don't run in the regression for now +#[cfg(slow)] +mod slow { + #[kani::proof] + #[kani::stub(RandomState::new, concrete_state)] + #[kani::unwind(3)] + fn check_insert_two_elements() { + let mut set: HashSet = HashSet::default(); + let first = kani::any(); + set.insert(first); + + let second = kani::any(); + set.insert(second); + + if first == second { assert_eq!(set.len(), 1) } else { assert_eq!(set.len(), 2) } + } +}