Partial support for bitreverse (model-checking#779)

* Support for `bitreverse` (WIP)

* Add test for all types

src/kani-compiler/cbmc/src/goto_program/expr.rs

@@ -203,6 +203,8 @@ pub enum SelfOperand {
 pub enum UnaryOperand {
     /// `~self`
     Bitnot,
+    /// `__builtin_bitreverse<n>(self)`
+    BitReverse,
     /// `__builtin_bswap<n>(self)`
     Bswap,
     /// `__CPROVER_DYNAMIC_OBJECT(self)`
@@ -1086,7 +1088,7 @@ impl Expr {
 impl Expr {
     fn typecheck_unop_arg(op: UnaryOperand, arg: &Expr) -> bool {
         match op {
-            Bitnot | Bswap | Popcount => arg.typ.is_integer(),
+            Bitnot | BitReverse | Bswap | Popcount => arg.typ.is_integer(),
             CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.is_integer(),
             IsDynamicObject | ObjectSize | PointerObject => arg.typ().is_pointer(),
             PointerOffset => arg.typ == Type::void_pointer(),
@@ -1097,7 +1099,7 @@ impl Expr {
 
     fn unop_return_type(op: UnaryOperand, arg: &Expr) -> Type {
         match op {
-            Bitnot | Bswap | UnaryMinus => arg.typ.clone(),
+            Bitnot | BitReverse | Bswap | UnaryMinus => arg.typ.clone(),
             CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.clone(),
             ObjectSize | PointerObject => Type::size_t(),
             PointerOffset => Type::ssize_t(),
@@ -1122,6 +1124,11 @@ impl Expr {
         self.unop(Bswap)
     }
 
+    /// `__builtin_bitreverse<n>(self)`
+    pub fn bitreverse(self) -> Expr {
+        self.unop(BitReverse)
+    }
+
     /// `__CPROVER_DYNAMIC_OBJECT(self)`
     pub fn dynamic_object(self) -> Self {
         self.unop(IsDynamicObject)

src/kani-compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs

@@ -476,6 +476,7 @@ pub trait Transformer: Sized {
         let transformed_e = self.transform_expr(e);
         match op {
             UnaryOperand::Bitnot => transformed_e.bitnot(),
+            UnaryOperand::BitReverse => transformed_e.bitreverse(),
             UnaryOperand::Bswap => transformed_e.bswap(),
             UnaryOperand::IsDynamicObject => transformed_e.dynamic_object(),
             UnaryOperand::Not => transformed_e.not(),

src/kani-compiler/cbmc/src/irep/irep_id.rs

@@ -593,6 +593,7 @@ pub enum IrepId {
     WorkingDirectory,
     Section,
     Bswap,
+    BitReverse,
     JavaBytecodeIndex,
     JavaInstanceof,
     JavaSuperMethodCall,
@@ -1431,6 +1432,7 @@ impl ToString for IrepId {
             IrepId::WorkingDirectory => "working_directory",
             IrepId::Section => "section",
             IrepId::Bswap => "bswap",
+            IrepId::BitReverse => "bitreverse",
             IrepId::JavaBytecodeIndex => "java_bytecode_index",
             IrepId::JavaInstanceof => "java_instanceof",
             IrepId::JavaSuperMethodCall => "java_super_method_call",

src/kani-compiler/cbmc/src/irep/to_irep.rs

@@ -98,6 +98,7 @@ impl ToIrepId for UnaryOperand {
     fn to_irep_id(&self) -> IrepId {
         match self {
             UnaryOperand::Bitnot => IrepId::Bitnot,
+            UnaryOperand::BitReverse => IrepId::BitReverse,
             UnaryOperand::Bswap => IrepId::Bswap,
             UnaryOperand::CountLeadingZeros { .. } => IrepId::CountLeadingZeros,
             UnaryOperand::CountTrailingZeros { .. } => IrepId::CountTrailingZeros,
@@ -277,6 +278,9 @@ impl ToIrep for ExprValue {
                 sub: vec![e.to_irep(mm)],
                 named_sub: vector_map![(IrepId::BitsPerByte, Irep::just_int_id(8))],
             },
+            ExprValue::UnOp { op: UnaryOperand::BitReverse, e } => {
+                Irep { id: IrepId::BitReverse, sub: vec![e.to_irep(mm)], named_sub: vector_map![] }
+            }
             ExprValue::UnOp { op: UnaryOperand::CountLeadingZeros { allow_zero }, e } => Irep {
                 id: IrepId::CountLeadingZeros,
                 sub: vec![e.to_irep(mm)],

src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs

@@ -355,6 +355,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "atomic_xsub_acqrel" => codegen_atomic_binop!(sub),
             "atomic_xsub_rel" => codegen_atomic_binop!(sub),
             "atomic_xsub_relaxed" => codegen_atomic_binop!(sub),
+            "bitreverse" => self.codegen_expr_to_place(p, fargs.remove(0).bitreverse()),
             // black_box is an identity function that hints to the compiler
             // to be maximally pessimistic to limit optimizations
             "black_box" => self.codegen_expr_to_place(p, fargs.remove(0)),

tests/kani/Intrinsics/fixme_bitreverse.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 we get the expected results for the `bitreverse` intrinsic
+// https://doc.rust-lang.org/std/intrinsics/fn.bitreverse.html
+
+// Note: Support for `__builtin_bitreverse` in CBMC is being added in
+// https://github.com/diffblue/cbmc/pull/6581
+// Tracking issue: https://github.com/model-checking/kani/issues/778
+
+const BITS_PER_BYTE: usize = 8;
+
+macro_rules! test_bitreverse_intrinsic {
+    ($ty:ty, $check_name:ident, $get_bit_name:ident) => {
+        fn $get_bit_name(x: $ty, n: usize) -> bool {
+            return x & (1 << n) != 0;
+        }
+
+        fn $check_name(a: $ty, b: $ty) -> bool {
+            let len: usize = (std::mem::size_of::<$ty>() * BITS_PER_BYTE) - 1;
+            for n in 0..len {
+                if $get_bit_name(a, n) != $get_bit_name(b, len - n) {
+                    return false;
+                }
+            }
+            return true;
+        }
+
+        let x: $ty = kani::any();
+        let res = $check_name(x, x.reverse_bits());
+        assert!(res);
+    };
+}
+
+#[allow(overflowing_literals)]
+fn main() {
+    test_bitreverse_intrinsic!(u8, check_reverse_u8, get_bit_at_u8);
+    test_bitreverse_intrinsic!(u16, check_reverse_u16, get_bit_at_u16);
+    test_bitreverse_intrinsic!(u32, check_reverse_u32, get_bit_at_u32);
+    test_bitreverse_intrinsic!(u64, check_reverse_u64, get_bit_at_u64);
+    test_bitreverse_intrinsic!(usize, check_reverse_usize, get_bit_at_usize);
+    test_bitreverse_intrinsic!(i8, check_reverse_i8, get_bit_at_i8);
+    test_bitreverse_intrinsic!(i16, check_reverse_i16, get_bit_at_i16);
+    test_bitreverse_intrinsic!(i32, check_reverse_i32, get_bit_at_i32);
+    test_bitreverse_intrinsic!(i64, check_reverse_i64, get_bit_at_i64);
+    test_bitreverse_intrinsic!(isize, check_reverse_isize, get_bit_at_isize);
+}