Add a test for ctpop (model-checking#1048)

* Add a test for `ctpop`

* Fix format

tests/kani/Intrinsics/Count/ctpop.rs

@@ -0,0 +1,73 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `ctpop` is supported and returns the expected results
+// (the number of bits equal to one in a value)
+#![feature(core_intrinsics)]
+use std::intrinsics::ctpop;
+
+// Define a function for counting like `ctpop` and assert that their results are
+// the same for any value
+macro_rules! test_ctpop {
+    ( $fn_name:ident, $ty:ty ) => {
+        fn $fn_name(x: $ty) -> $ty {
+            let mut count = 0;
+            let num_bits = <$ty>::BITS;
+            for i in 0..num_bits {
+                // Get value at index `i`
+                let bitmask = 1 << i;
+                let bit = x & bitmask;
+                if bit != 0 {
+                    count += 1;
+                }
+                // The assertion below mitigates a low performance issue in this
+                // test due to the loop having a conditional jump at the end,
+                // see https://github.com/model-checking/kani/issues/1046 for
+                // more details.
+                assert!(count >= 0);
+            }
+            count
+        }
+        let var: $ty = kani::any();
+        // Check that the result is correct
+        assert!($fn_name(var) == ctpop(var));
+
+        // Check that the stable version returns the same value
+        assert!(ctpop(var) as u32 == var.count_ones());
+    };
+}
+
+#[kani::proof]
+fn test_ctpop_u8() {
+    test_ctpop!(my_ctpop_u8, u8);
+}
+
+#[kani::proof]
+fn test_ctpop_u16() {
+    test_ctpop!(my_ctpop_u16, u16);
+}
+
+#[kani::proof]
+fn test_ctpop_u32() {
+    test_ctpop!(my_ctpop_u32, u32);
+}
+
+#[kani::proof]
+fn test_ctpop_u64() {
+    test_ctpop!(my_ctpop_u64, u64);
+}
+
+// We do not run the test for u128 because it takes too long
+fn test_ctpop_u128() {
+    test_ctpop!(my_ctpop_u128, u128);
+}
+
+#[kani::proof]
+fn test_ctpop_usize() {
+    test_ctpop!(my_ctpop_usize, usize);
+}
+
+// `ctpop` also works with signed integer types, but this causes overflows
+// unless we restrict their values considerably (due to the conversions in
+// `count_ones`), making the signed versions not very interesting to test here.
+// https://github.com/model-checking/kani/issues/934