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
+rotate.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/util/bitvector_expr.h

@@ -1008,4 +1008,48 @@ inline count_trailing_zeros_exprt &to_count_trailing_zeros_expr(exprt &expr)
   return ret;
 }
 
+/// \brief Reverse the order of bits in a bit-vector.
+class bitreverse_exprt : public unary_exprt
+{
+public:
+  explicit bitreverse_exprt(exprt op)
+    : unary_exprt(ID_bitreverse, std::move(op))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<bitreverse_exprt>(const exprt &base)
+{
+  return base.id() == ID_bitreverse;
+}
+
+inline void validate_expr(const bitreverse_exprt &value)
+{
+  validate_operands(value, 1, "Bit-wise reverse must have one operand");
+}
+
+/// \brief Cast an exprt to a \ref bitreverse_exprt
+///
+/// \a expr must be known to be \ref bitreverse_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref bitreverse_exprt
+inline const bitreverse_exprt &to_bitreverse_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_bitreverse);
+  const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_bitreverse_expr(const exprt &)
+inline bitreverse_exprt &to_bitreverse_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_bitreverse);
+  bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H

src/util/irep_ids.def

@@ -864,6 +864,7 @@ IREP_ID_TWO(vector_lt, vector-<)
 IREP_ID_ONE(shuffle_vector)
 IREP_ID_ONE(count_trailing_zeros)
 IREP_ID_ONE(empty_union)
+IREP_ID_ONE(bitreverse)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree

src/util/simplify_expr.cpp

@@ -2542,6 +2542,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
   {
     r = simplify_overflow_unary(to_unary_overflow_expr(expr));
   }
+  else if(expr.id() == ID_bitreverse)
+  {
+    r = simplify_bitreverse(to_bitreverse_expr(expr));
+  }
 
   if(!no_change_join_operands)
     r = changed(r);

src/util/simplify_expr_class.h

@@ -33,6 +33,7 @@ class binary_exprt;
 class binary_overflow_exprt;
 class binary_relation_exprt;
 class bitnot_exprt;
+class bitreverse_exprt;
 class bswap_exprt;
 class byte_extract_exprt;
 class byte_update_exprt;
@@ -210,6 +211,9 @@ class simplify_exprt
   /// Try to simplify count-trailing-zeros to a constant expression.
   NODISCARD resultt<> simplify_ctz(const count_trailing_zeros_exprt &);
 
+  /// Try to simplify bit-reversing to a constant expression.
+  NODISCARD resultt<> simplify_bitreverse(const bitreverse_exprt &);
+
   // auxiliary
   bool simplify_if_implies(
     exprt &expr, const exprt &cond, bool truth, bool &new_truth);

src/util/simplify_expr_int.cpp

@@ -1822,3 +1822,27 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
 #endif
   return unchanged(expr);
 }
+
+simplify_exprt::resultt<>
+simplify_exprt::simplify_bitreverse(const bitreverse_exprt &expr)
+{
+  auto const_bits_opt = expr2bits(
+    expr.op(),
+    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
+    ns);
+
+  if(!const_bits_opt.has_value())
+    return unchanged(expr);
+
+  std::reverse(const_bits_opt->begin(), const_bits_opt->end());
+
+  auto result = bits2expr(
+    *const_bits_opt,
+    expr.type(),
+    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
+    ns);
+  if(!result.has_value())
+    return unchanged(expr);
+
+  return std::move(*result);
+}