Complete tests for count intrinsics (model-checking#883)

* Complete tests for count intrinsics

* Use `kani::any()` instead of concrete value in `test_ctlz_nonzero`

tests/kani/Intrinsics/Count/ctlz.rs

@@ -0,0 +1,67 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `ctlz` and `ctlz_nonzero` are supported and return the expected
+// results
+
+#![feature(core_intrinsics)]
+use std::intrinsics::{ctlz, ctlz_nonzero};
+
+// Define a function for counting like `ctlz` and assert that their results are
+// the same for any value
+macro_rules! test_ctlz {
+    ( $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 << (num_bits - i - 1);
+                let bit = x & bitmask;
+                if bit == 0 {
+                    count += 1;
+                } else {
+                    break;
+                }
+            }
+            count
+        }
+        let var: $ty = kani::any();
+        // Check that the result is correct
+        assert!($fn_name(var) == ctlz(var));
+        // Check that the stable version returns the same value
+        assert!(ctlz(var) as u32 == var.leading_zeros());
+    };
+}
+
+// Assert that the results of `ctlz` and `ctlz_nonzero` are the same if we
+// exclude zero
+macro_rules! test_ctlz_nonzero {
+    ($ty:ty) => {
+        let var_nonzero: $ty = kani::any();
+        kani::assume(var_nonzero != 0);
+        unsafe {
+            assert!(ctlz(var_nonzero) == ctlz_nonzero(var_nonzero));
+        }
+    };
+}
+
+fn main() {
+    test_ctlz!(my_ctlz_u8, u8);
+    test_ctlz!(my_ctlz_u16, u16);
+    test_ctlz!(my_ctlz_u32, u32);
+    test_ctlz!(my_ctlz_u64, u64);
+    test_ctlz!(my_ctlz_u128, u128);
+    test_ctlz!(my_ctlz_usize, usize);
+    test_ctlz_nonzero!(u8);
+    test_ctlz_nonzero!(u16);
+    test_ctlz_nonzero!(u32);
+    test_ctlz_nonzero!(u64);
+    test_ctlz_nonzero!(u128);
+    test_ctlz_nonzero!(usize);
+    // These intrinsics are 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, making the signed versions not very interesting to test
+    // here.
+}

tests/kani/Intrinsics/Count/ctlz_nonzero_panic.rs

@@ -0,0 +1,25 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `ctlz_nonzero` fails if zero is passed as an argument
+
+#![feature(core_intrinsics)]
+use std::intrinsics::ctlz_nonzero;
+
+// Call `ctlz_nonzero` with an unconstrained symbolic argument
+macro_rules! test_ctlz_nonzero {
+    ($ty:ty) => {
+        let var_nonzero: $ty = kani::any();
+        let _ = unsafe { ctlz_nonzero(var_nonzero) };
+    };
+}
+
+fn main() {
+    test_ctlz_nonzero!(u8);
+    test_ctlz_nonzero!(u16);
+    test_ctlz_nonzero!(u32);
+    test_ctlz_nonzero!(u64);
+    test_ctlz_nonzero!(u128);
+    test_ctlz_nonzero!(usize);
+}

tests/kani/Intrinsics/Count/cttz.rs

@@ -0,0 +1,70 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `cttz` and `cttz_nonzero` are supported and return the expected
+// results
+
+#![feature(core_intrinsics)]
+use std::intrinsics::{cttz, cttz_nonzero};
+
+// Define a function for counting like `cttz` and assert that their results are
+// the same for any value
+macro_rules! test_cttz {
+    ( $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;
+                } else {
+                    break;
+                }
+            }
+            count
+        }
+        let var: $ty = kani::any();
+        // FIXME: Remove the assumption below when CBMC returns the correct value for 0
+        // https://github.com/model-checking/kani/issues/881
+        kani::assume(var != 0);
+        // Check that the result is correct
+        assert!($fn_name(var) == cttz(var));
+        // Check that the stable version returns the same value
+        assert!(cttz(var) as u32 == var.trailing_zeros());
+    };
+}
+
+// Assert that the results of `cttz` and `cttz_nonzero` are the same if we
+// exclude zero
+macro_rules! test_cttz_nonzero {
+    ($ty:ty) => {
+        let var_nonzero: $ty = kani::any();
+        kani::assume(var_nonzero != 0);
+        unsafe {
+            assert!(cttz(var_nonzero) == cttz_nonzero(var_nonzero));
+        }
+    };
+}
+
+fn main() {
+    test_cttz!(my_cttz_u8, u8);
+    test_cttz!(my_cttz_u16, u16);
+    test_cttz!(my_cttz_u32, u32);
+    test_cttz!(my_cttz_u64, u64);
+    test_cttz!(my_cttz_u128, u128);
+    test_cttz!(my_cttz_usize, usize);
+    test_cttz_nonzero!(u8);
+    test_cttz_nonzero!(u16);
+    test_cttz_nonzero!(u32);
+    test_cttz_nonzero!(u64);
+    test_cttz_nonzero!(u128);
+    test_cttz_nonzero!(usize);
+    // These intrinsics are 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, making the signed versions not very interesting to test
+    // here.
+}

tests/kani/Intrinsics/Count/cttz_nonzero_panic.rs

@@ -0,0 +1,25 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `cttz_nonzero` fails if zero is passed as an argument
+
+#![feature(core_intrinsics)]
+use std::intrinsics::cttz_nonzero;
+
+// Call `cttz_nonzero` with an unconstrained symbolic argument
+macro_rules! test_cttz_nonzero {
+    ($ty:ty) => {
+        let var_nonzero: $ty = kani::any();
+        let _ = unsafe { cttz_nonzero(var_nonzero) };
+    };
+}
+
+fn main() {
+    test_cttz_nonzero!(u8);
+    test_cttz_nonzero!(u16);
+    test_cttz_nonzero!(u32);
+    test_cttz_nonzero!(u64);
+    test_cttz_nonzero!(u128);
+    test_cttz_nonzero!(usize);
+}