From c3dde0ade8c8674e5ec461cea41213cf963cb632 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 2 Mar 2022 19:36:48 +0000 Subject: [PATCH 1/5] Add thorough tests for rotate intrinsics --- tests/kani/Intrinsics/Rotate/rotate_left.rs | 47 +++++++++++++++++ tests/kani/Intrinsics/Rotate/rotate_right.rs | 54 ++++++++++++++++++++ 2 files changed, 101 insertions(+) create mode 100644 tests/kani/Intrinsics/Rotate/rotate_left.rs create mode 100644 tests/kani/Intrinsics/Rotate/rotate_right.rs diff --git a/tests/kani/Intrinsics/Rotate/rotate_left.rs b/tests/kani/Intrinsics/Rotate/rotate_left.rs new file mode 100644 index 000000000000..633e33e92d4b --- /dev/null +++ b/tests/kani/Intrinsics/Rotate/rotate_left.rs @@ -0,0 +1,47 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(core_intrinsics)] +use std::intrinsics::{rotate_left, rotate_right}; + +// Check that `rotate_left` is supported and returns the expected result. + +macro_rules! test_rotate_left { + ( $fn_name:ident, $ty:ty ) => { + fn $fn_name(x: $ty, rot_x: $ty, n: u32) { + let i: u32 = kani::any(); + kani::assume(i < <$ty>::BITS); + // Get value at index `i` + let bitmask = 1 << i; + let bit = (x & bitmask) != 0; + // Get value at rotated index `rot_i` + let rot_i = (i + (n as u32)) % <$ty>::BITS; + let rot_bitmask = 1 << rot_i; + let rot_bit = (rot_x & rot_bitmask) != 0; + // Assert that both bit values are the same + assert!(bit == rot_bit); + } + let x: $ty = kani::any(); + let n: u32 = kani::any(); + // Limit `n` to `u8::MAX` to avoid overflows + kani::assume(n <= u8::MAX as u32); + let y: $ty = rotate_left(x, n as $ty); + // Check that the rotation is correct + $fn_name(x, y, n); + // Check that the stable version returns the same value + assert!(y == x.rotate_left(n)); + }; +} + +fn main() { + test_rotate_left!(check_rol_u8, u8); + test_rotate_left!(check_rol_u16, u16); + test_rotate_left!(check_rol_u32, u32); + test_rotate_left!(check_rol_u64, u64); + test_rotate_left!(check_rol_u128, u128); + test_rotate_left!(check_rol_usize, usize); + // `rotate_left` is also defined for signed integer types by casting the + // number into the corresponding unsigned type and then casting the result + // into the original signed type. This causes overflows unless we restrict + // their values considerably, making the signed versions not very + // interesting to test here. +} diff --git a/tests/kani/Intrinsics/Rotate/rotate_right.rs b/tests/kani/Intrinsics/Rotate/rotate_right.rs new file mode 100644 index 000000000000..1a85fa7e6e68 --- /dev/null +++ b/tests/kani/Intrinsics/Rotate/rotate_right.rs @@ -0,0 +1,54 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that `rotate_right` is supported and returns the expected result. +#![feature(core_intrinsics)] +use std::intrinsics::rotate_right; + +macro_rules! test_rotate_right { + ( $fn_name:ident, $ty:ty ) => { + fn $fn_name(x: $ty, rot_x: $ty, n: u32) { + let BITS_i32 = <$ty>::BITS as i32; + let i: i32 = kani::any(); + kani::assume(i < BITS_i32); + kani::assume(i >= 0); + // Get value at index `i` + let bitmask = 1 << i; + let bit = (x & bitmask) != 0; + // Get value at rotated index `rot_i` + let mut rot_i = (i - (n as i32)) % BITS_i32; + // If the rotated index is negative, we must add the bit-width to + // get the actual rotated index + if rot_i < 0 { + rot_i = rot_i + BITS_i32; + } + let rot_bitmask = 1 << rot_i; + let rot_bit = (rot_x & rot_bitmask) != 0; + // Assert that both bit values are the same + assert!(bit == rot_bit); + } + let x: $ty = kani::any(); + let n: u32 = kani::any(); + // Limit `n` to `i8::MAX` to avoid overflows + kani::assume(n <= u8::MAX as u32); + let y: $ty = rotate_right(x, n as $ty); + // Check that the rotation is correct + $fn_name(x, y, n); + // Check that the stable version returns the same value + assert!(y == x.rotate_right(n)); + }; +} + +fn main() { + test_rotate_right!(check_ror_u8, u8); + test_rotate_right!(check_ror_u16, u16); + test_rotate_right!(check_ror_u32, u32); + test_rotate_right!(check_ror_u64, u64); + test_rotate_right!(check_ror_u128, u128); + test_rotate_right!(check_ror_usize, usize); + // `rotate_right` is also defined for signed integer types by casting the + // number into the corresponding unsigned type and then casting the result + // into the original signed type. This causes overflows unless we restrict + // their values considerably, making the signed versions not very + // interesting to test here. +} From dd3ef0f029d17924fc68a3b462012bc793267b84 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 2 Mar 2022 19:41:49 +0000 Subject: [PATCH 2/5] Remove concrete tests for rotate intrinsics --- .../kani/BitManipulation/Stable/fixme_main.rs | 3 -- .../BitManipulation/Unstable/Rotate/main.rs | 38 ------------------- 2 files changed, 41 deletions(-) delete mode 100644 tests/kani/BitManipulation/Unstable/Rotate/main.rs diff --git a/tests/kani/BitManipulation/Stable/fixme_main.rs b/tests/kani/BitManipulation/Stable/fixme_main.rs index 98a6b9645c51..19b338a3dca0 100644 --- a/tests/kani/BitManipulation/Stable/fixme_main.rs +++ b/tests/kani/BitManipulation/Stable/fixme_main.rs @@ -6,13 +6,10 @@ fn main() { // Intrinsics implemented as integer primitives // https://doc.rust-lang.org/core/intrinsics/fn.cttz.html // https://doc.rust-lang.org/core/intrinsics/fn.ctlz.html - // https://doc.rust-lang.org/std/intrinsics/fn.rotate_left.html let x = 0b0011_1000_u8; let num_trailing = x.trailing_zeros(); let num_leading = x.leading_zeros(); - let rotated_num = x.rotate_left(3); assert!(num_trailing == 3); // fails because of https://github.com/model-checking/kani/issues/26 assert!(num_leading == 2); - assert!(rotated_num == 0b1100_0001_u8); } diff --git a/tests/kani/BitManipulation/Unstable/Rotate/main.rs b/tests/kani/BitManipulation/Unstable/Rotate/main.rs deleted file mode 100644 index bd35a2f9a38c..000000000000 --- a/tests/kani/BitManipulation/Unstable/Rotate/main.rs +++ /dev/null @@ -1,38 +0,0 @@ -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 OR MIT -#![feature(core_intrinsics)] -use std::intrinsics::{rotate_left, rotate_right}; - -fn main() { - let vl8 = 0b0011_1000_u8; - let vl16 = 0b0011_1000_0000_0000_u16; - let vl32 = 0b0011_1000_0000_0000_0000_0000_0000_0000_u32; - let vl64 = - 0b0011_1000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_u64; - - let vr8 = 0b0000_1110_u8; - let vr16 = 0b0000_0000_0000_1110_u16; - let vr32 = 0b0000_0000_0000_0000_0000_0000_0000_1110_u32; - let vr64 = - 0b0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_1110_u64; - - let rol8 = rotate_left(vl8, 3); - let rol16 = rotate_left(vl16, 3); - let rol32 = rotate_left(vl32, 3); - let rol64 = rotate_left(vl64, 3); - - let ror8 = rotate_right(vr8, 3); - let ror16 = rotate_right(vr16, 3); - let ror32 = rotate_right(vr32, 3); - let ror64 = rotate_right(vr64, 3); - - assert!(rol8 == 0b1100_0001_u8); - assert!(rol16 == 0b1100_0000_0000_0001_u16); - assert!(rol32 == 0b1100_0000_0000_0000_0000_0000_0000_0001_u32); - assert!(rol64 == 0b1100_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0001_u64); - - assert!(ror8 == 0b1100_0001_u8); - assert!(ror16 == 0b1100_0000_0000_0001_u16); - assert!(ror32 == 0b1100_0000_0000_0000_0000_0000_0000_0001_u32); - assert!(ror64 == 0b1100_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0001_u64); -} From 8c2734c4eda4fea7dceab629c18ed20a0e8d674d Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 2 Mar 2022 19:45:53 +0000 Subject: [PATCH 3/5] Move code after test description --- tests/kani/Intrinsics/Rotate/rotate_left.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/kani/Intrinsics/Rotate/rotate_left.rs b/tests/kani/Intrinsics/Rotate/rotate_left.rs index 633e33e92d4b..4772bd691753 100644 --- a/tests/kani/Intrinsics/Rotate/rotate_left.rs +++ b/tests/kani/Intrinsics/Rotate/rotate_left.rs @@ -1,9 +1,9 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -#![feature(core_intrinsics)] -use std::intrinsics::{rotate_left, rotate_right}; // Check that `rotate_left` is supported and returns the expected result. +#![feature(core_intrinsics)] +use std::intrinsics::rotate_left; macro_rules! test_rotate_left { ( $fn_name:ident, $ty:ty ) => { @@ -29,7 +29,7 @@ macro_rules! test_rotate_left { $fn_name(x, y, n); // Check that the stable version returns the same value assert!(y == x.rotate_left(n)); - }; + } } fn main() { From 83f834ed2f87eab31d6ac4a2fb09bdb20bc4a845 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 2 Mar 2022 20:07:36 +0000 Subject: [PATCH 4/5] format --- tests/kani/Intrinsics/Rotate/rotate_left.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/kani/Intrinsics/Rotate/rotate_left.rs b/tests/kani/Intrinsics/Rotate/rotate_left.rs index 4772bd691753..cd3e80411d93 100644 --- a/tests/kani/Intrinsics/Rotate/rotate_left.rs +++ b/tests/kani/Intrinsics/Rotate/rotate_left.rs @@ -29,7 +29,7 @@ macro_rules! test_rotate_left { $fn_name(x, y, n); // Check that the stable version returns the same value assert!(y == x.rotate_left(n)); - } + }; } fn main() { From 07dba9d3a9da9976b792ad231d62f15720335dc9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Wed, 2 Mar 2022 18:23:34 -0500 Subject: [PATCH 5/5] Update comment Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- tests/kani/Intrinsics/Rotate/rotate_right.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/kani/Intrinsics/Rotate/rotate_right.rs b/tests/kani/Intrinsics/Rotate/rotate_right.rs index 1a85fa7e6e68..e2baedf2baf8 100644 --- a/tests/kani/Intrinsics/Rotate/rotate_right.rs +++ b/tests/kani/Intrinsics/Rotate/rotate_right.rs @@ -29,7 +29,7 @@ macro_rules! test_rotate_right { } let x: $ty = kani::any(); let n: u32 = kani::any(); - // Limit `n` to `i8::MAX` to avoid overflows + // Limit `n` to `u8::MAX` to avoid overflows kani::assume(n <= u8::MAX as u32); let y: $ty = rotate_right(x, n as $ty); // Check that the rotation is correct