Add a test for bswap (model-checking#1023)

* Add a test for `bswap`

* Address comments

tests/kani/Intrinsics/bswap.rs

@@ -0,0 +1,74 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `bswap` returns the expected results.
+// https://doc.rust-lang.org/std/intrinsics/fn.bswap.html
+
+// `bswap` reverses the bytes in an integer type `T`, for example:
+//
+// ```
+// let n = 0x12345678u32;
+// let m = std::intrinsics::bswap(n);
+
+// assert_eq!(m, 0x78563412);
+// ```
+
+#![feature(core_intrinsics)]
+
+const BITS_PER_BYTE: usize = 8;
+
+macro_rules! test_bswap_intrinsic {
+    ($ty:ty, $check_name:ident, $get_byte_name:ident) => {
+        // Gets the i-th byte in `x`
+        fn $get_byte_name(x: $ty, i: usize) -> $ty {
+                let mask = 0xFF as $ty << i * BITS_PER_BYTE;
+                let masked_res = x & mask;
+                let bytes_res = masked_res >> i * BITS_PER_BYTE;
+                bytes_res
+        }
+
+        // Checks that the order of bytes in the original integer is reversed in
+        // the swapped integer
+        fn $check_name(a: $ty, b: $ty) {
+            let bytes = std::mem::size_of::<$ty>();
+            let i: usize = kani::any();
+            kani::assume(i < bytes);
+            let a_byte = $get_byte_name(a, i);
+            let b_byte = $get_byte_name(b, bytes - i - 1);
+            assert!(a_byte == b_byte);
+        }
+
+        let x: $ty = kani::any();
+        $check_name(x, std::intrinsics::bswap(x));
+    }
+}
+
+#[kani::proof]
+fn test_bswap_u8() {
+    test_bswap_intrinsic!(u8, check_bswap_u8, get_byte_at_u8);
+}
+
+#[kani::proof]
+fn test_bswap_u16() {
+    test_bswap_intrinsic!(u16, check_bswap_u16, get_byte_at_u16);
+}
+
+#[kani::proof]
+fn test_bswap_u32() {
+    test_bswap_intrinsic!(u32, check_bswap_u32, get_byte_at_u32);
+}
+
+#[kani::proof]
+fn test_bswap_u64() {
+    test_bswap_intrinsic!(u64, check_bswap_u64, get_byte_at_u64);
+}
+
+#[kani::proof]
+fn test_bswap_u128() {
+    test_bswap_intrinsic!(u128, check_bswap_u128, get_byte_at_u128);
+}
+
+// `bswap` also works with signed integer types, but this causes overflows
+// unless we restrict their values considerably (due to how bytes are
+// extracted), making the signed versions not very interesting to test here.
+// https://github.com/model-checking/kani/issues/934