From 724d163c4ae2af483991115e625dff3b11ad3b1b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 15 Aug 2023 17:28:29 -0700 Subject: [PATCH] Address comments --- kani-compiler/src/kani_middle/intrinsics.rs | 6 ++--- kani-compiler/src/kani_middle/provide.rs | 4 ++-- library/kani/src/models/mod.rs | 26 +++++++++++++++++++-- 3 files changed, 29 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index 8033acf01263..3ebf0224aba7 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -10,13 +10,13 @@ use rustc_middle::ty::{Const, GenericArgsRef}; use rustc_span::symbol::{sym, Symbol}; use tracing::{debug, trace}; -pub struct AbstractIntrinsics<'tcx> { +pub struct ModelIntrinsics<'tcx> { tcx: TyCtxt<'tcx>, /// Local declarations of the function being transformed. local_decls: IndexVec>, } -impl<'tcx> AbstractIntrinsics<'tcx> { +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. @@ -24,7 +24,7 @@ impl<'tcx> AbstractIntrinsics<'tcx> { /// 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>) { - AbstractIntrinsics { tcx, local_decls: body.local_decls.clone() }.transform(body) + ModelIntrinsics { tcx, local_decls: body.local_decls.clone() }.transform(body) } pub fn transform(&self, body: &mut Body<'tcx>) { diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index 20002a575558..7e26ec7c7513 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -4,7 +4,7 @@ //! to run during code generation. For example, this can be used to hook up //! custom MIR transformations. -use crate::kani_middle::intrinsics::AbstractIntrinsics; +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}; @@ -66,7 +66,7 @@ fn run_kani_mir_passes<'tcx>( 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. - AbstractIntrinsics::run_pass(tcx, &mut transformed_body); + ModelIntrinsics::run_pass(tcx, &mut transformed_body); tcx.arena.alloc(transformed_body) } diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index a24300b1217f..0bbb7d99565a 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -33,7 +33,15 @@ mod intrinsics { 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; } } @@ -53,6 +61,9 @@ mod intrinsics { 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 } @@ -70,7 +81,7 @@ mod intrinsics { *mask = if input[lane] == T::TRUE { shift_mask | 0x1 } else { - assert_eq!(input[lane], T::FALSE, "Masks values should either be 0 or 1"); + assert_eq!(input[lane], T::FALSE, "Masks values should either be 0 or -1"); shift_mask }; } @@ -122,14 +133,17 @@ mod test { 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")] + #[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!( @@ -138,6 +152,8 @@ 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")] fn test_invalid_generics() { @@ -145,6 +161,8 @@ mod test { 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 endianess correctly. #[test] fn test_bitmask_i32() { check_portable_bitmask::<_, i32, 8>(mask32x8::from([ @@ -158,12 +176,15 @@ mod test { #[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, @@ -177,6 +198,7 @@ mod test { ); } + /// Compare the value returned by our model and the simd_bitmask intrinsic. fn check_bitmask(mask: T) where T: Clone,