bitreverse_exprt: Expression to reverse the order of bits

Clang has a __builtin_bitreverse (and at some point GCC might as well:
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=50481).

Author: tautschnig

regression/cbmc/clang_builtins/bitreverse.c

@@ -0,0 +1,64 @@
+#include <assert.h>
+#include <stdint.h>
+
+#define test_bit_reverse(W)                                                    \
+  uint##W##_t test_bit_reverse##W(uint##W##_t v)                               \
+  {                                                                            \
+    uint##W##_t result = 0;                                                    \
+    int i;                                                                     \
+    for(i = 0; i < W; i++)                                                     \
+    {                                                                          \
+      if(v & (1ULL << i))                                                      \
+        result |= 1ULL << (W - i - 1);                                         \
+    }                                                                          \
+    return result;                                                             \
+  }                                                                            \
+  int dummy_for_semicolon##W
+
+test_bit_reverse(8);
+test_bit_reverse(16);
+test_bit_reverse(32);
+test_bit_reverse(64);
+
+#ifndef __clang__
+unsigned char __builtin_bitreverse8(unsigned char);
+unsigned short __builtin_bitreverse16(unsigned short);
+unsigned int __builtin_bitreverse32(unsigned int);
+unsigned long long __builtin_bitreverse64(unsigned long long);
+#endif
+
+void check_8(void)
+{
+  uint8_t op;
+  assert(__builtin_bitreverse8(op) == test_bit_reverse8(op));
+  assert(__builtin_bitreverse8(1) == 0x80);
+}
+
+void check_16(void)
+{
+  uint16_t op;
+  assert(__builtin_bitreverse16(op) == test_bit_reverse16(op));
+  assert(__builtin_bitreverse16(1) == 0x8000);
+}
+
+void check_32(void)
+{
+  uint32_t op;
+  assert(__builtin_bitreverse32(op) == test_bit_reverse32(op));
+  assert(__builtin_bitreverse32(1) == 0x80000000);
+}
+
+void check_64(void)
+{
+  uint64_t op;
+  assert(__builtin_bitreverse64(op) == test_bit_reverse64(op));
+  assert(__builtin_bitreverse64(1) == 0x8000000000000000ULL);
+}
+
+int main(void)
+{
+  check_8();
+  check_16();
+  check_32();
+  check_64();
+}

regression/cbmc/clang_builtins/bitreverse.desc

@@ -0,0 +1,8 @@
+CORE
+bitreverse.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -3238,6 +3238,27 @@ exprt c_typecheck_baset::do_special_functions(
                                       std::move(result),
                                       expr.source_location()};
   }
+  else if(
+    identifier == "__builtin_bitreverse8" ||
+    identifier == "__builtin_bitreverse16" ||
+    identifier == "__builtin_bitreverse32" ||
+    identifier == "__builtin_bitreverse64")
+  {
+    // clang only
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects one operand" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    bitreverse_exprt bitreverse{expr.arguments()[0]};
+    bitreverse.add_source_location() = source_location;
+
+    return std::move(bitreverse);
+  }
   else
     return nil_exprt();
 }

src/ansi-c/clang_builtin_headers.h

@@ -54,6 +54,11 @@ void __builtin_nontemporal_load();
 
 int __builtin_flt_rounds(void);
 
+unsigned char __builtin_bitreverse8(unsigned char);
+unsigned short __builtin_bitreverse16(unsigned short);
+unsigned int __builtin_bitreverse32(unsigned int);
+unsigned long long __builtin_bitreverse64(unsigned long long);
+
 unsigned char __builtin_rotateleft8(unsigned char, unsigned char);
 unsigned short __builtin_rotateleft16(unsigned short, unsigned short);
 unsigned int __builtin_rotateleft32(unsigned int, unsigned int);

src/ansi-c/expr2c.cpp

@@ -3496,6 +3496,22 @@ std::string expr2ct::convert_conditional_target_group(const exprt &src)
   return dest;
 }
 
+std::string expr2ct::convert_bitreverse(const bitreverse_exprt &src)
+{
+  if(auto type_ptr = type_try_dynamic_cast<unsignedbv_typet>(src.type()))
+  {
+    const std::size_t width = type_ptr->get_width();
+    if(width == 8 || width == 16 || width == 32 || width == 64)
+    {
+      return convert_function(
+        src, "__builtin_bitreverse" + std::to_string(width));
+    }
+  }
+
+  unsigned precedence;
+  return convert_norep(src, precedence);
+}
+
 std::string expr2ct::convert_with_precedence(
   const exprt &src,
   unsigned &precedence)
@@ -3904,6 +3920,9 @@ std::string expr2ct::convert_with_precedence(
     return convert_conditional_target_group(src);
   }
 
+  else if(src.id() == ID_bitreverse)
+    return convert_bitreverse(to_bitreverse_expr(src));
+
   auto function_string_opt = convert_function(src);
   if(function_string_opt.has_value())
     return *function_string_opt;

src/ansi-c/expr2c_class.h

@@ -277,6 +277,7 @@ class expr2ct
     bool include_padding_components);
 
   std::string convert_conditional_target_group(const exprt &src);
+  std::string convert_bitreverse(const bitreverse_exprt &src);
 };
 
 #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H

src/solvers/flattening/boolbv.cpp

@@ -155,11 +155,14 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_replication(to_replication_expr(expr));
   else if(expr.id()==ID_extractbits)
     return convert_extractbits(to_extractbits_expr(expr));
-  else if(expr.id()==ID_bitnot || expr.id()==ID_bitand ||
-          expr.id()==ID_bitor || expr.id()==ID_bitxor ||
-          expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
-          expr.id()==ID_bitnand)
+  else if(
+    expr.id() == ID_bitnot || expr.id() == ID_bitand || expr.id() == ID_bitor ||
+    expr.id() == ID_bitxor || expr.id() == ID_bitxnor ||
+    expr.id() == ID_bitnor || expr.id() == ID_bitnand ||
+    expr.id() == ID_bitreverse)
+  {
     return convert_bitwise(expr);
+  }
   else if(expr.id() == ID_unary_minus)
     return convert_unary_minus(to_unary_minus_expr(expr));
   else if(expr.id()==ID_unary_plus)

src/solvers/flattening/boolbv_bitwise.cpp

@@ -60,6 +60,15 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
 
     return bv;
   }
+  else if(expr.id() == ID_bitreverse)
+  {
+    const exprt &op = to_bitreverse_expr(expr).op();
+    bvt bv = convert_bv(op, width);
+
+    std::reverse(bv.begin(), bv.end());
+
+    return bv;
+  }
 
   UNIMPLEMENTED;
 }

src/solvers/smt2/smt2_conv.cpp

@@ -2134,6 +2134,10 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     out << "()";
   }
+  else if(expr.id() == ID_bitreverse)
+  {
+    convert_expr(simplify_expr(to_bitreverse_expr(expr).lower(), ns));
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,

src/util/bitvector_expr.cpp

@@ -142,3 +142,17 @@ exprt count_trailing_zeros_exprt::lower() const
 
   return typecast_exprt::conditional_cast(result, type());
 }
+
+exprt bitreverse_exprt::lower() const
+{
+  const std::size_t int_width = to_bitvector_type(type()).get_width();
+
+  exprt::operandst result_bits;
+  result_bits.reserve(int_width);
+
+  const exprt operand = op();
+  for(std::size_t i = 0; i < int_width; ++i)
+    result_bits.push_back(extractbit_exprt{operand, i});
+
+  return concatenation_exprt{result_bits, type()};
+}