Thorough testing for rotate intrinsics (#880)

* Add thorough tests for rotate intrinsics

* Remove concrete tests for rotate intrinsics

* Move code after test description

* format

* Update comment

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

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);
 }

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
+
+// 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 ) => {
+        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.
+}

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 `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
+        $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.
+}