bitreverse_exprt: Expression to reverse the order of bits

tautschnig · tautschnig · commit 6076dbcea828 · 2022-01-28T15:47:45.000Z
Clang has a __builtin_bitreverse (and at some point GCC might as well: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=50481).
diff --git a/regression/cbmc/clang_builtins/bitreverse-typeconflict.c b/regression/cbmc/clang_builtins/bitreverse-typeconflict.c
@@ -0,0 +1,6 @@
+unsigned char __builtin_bitreverse8(char, char);
+
+int main()
+{
+  return __builtin_bitreverse8(1, 2);
+}
diff --git a/regression/cbmc/clang_builtins/bitreverse-typeconflict.desc b/regression/cbmc/clang_builtins/bitreverse-typeconflict.desc
@@ -0,0 +1,7 @@
+CORE
+bitreverse-typeconflict.c
+file bitreverse-typeconflict.c line 5 function main: error: __builtin_bitreverse8 expects one operand
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/clang_builtins/bitreverse.c b/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();
+}
diff --git a/regression/cbmc/clang_builtins/bitreverse.desc b/regression/cbmc/clang_builtins/bitreverse.desc
@@ -0,0 +1,8 @@
+CORE thorough-paths
+bitreverse.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -3204,6 +3204,28 @@ exprt c_typecheck_baset::do_special_functions(
   {
     return typecheck_builtin_overflow(expr, ID_mult);
   }
+  else if(
+    identifier == "__builtin_bitreverse8" ||
+    identifier == "__builtin_bitreverse16" ||
+    identifier == "__builtin_bitreverse32" ||
+    identifier == "__builtin_bitreverse64")
+  {
+    // clang only
+    if(expr.arguments().size() != 1)
+    {
+      std::ostringstream error_message;
+      error_message << expr.source_location().as_string()
+                    << ": error: " << identifier << " expects one operand";
+      throw invalid_source_file_exceptiont{error_message.str()};
+    }
+
+    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();
   // NOLINTNEXTLINE(readability/fn_size)
diff --git a/src/ansi-c/clang_builtin_headers.h b/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);
diff --git a/src/ansi-c/expr2c.cpp b/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;
diff --git a/src/ansi-c/expr2c_class.h b/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
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
@@ -86,6 +86,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_add_sub.cpp \
       flattening/boolbv_array.cpp \
       flattening/boolbv_array_of.cpp \
+      flattening/boolbv_bitreverse.cpp \
       flattening/boolbv_bitwise.cpp \
       flattening/boolbv_bswap.cpp \
       flattening/boolbv_bv_rel.cpp \
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
@@ -227,6 +227,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_bv(
       simplify_expr(to_count_trailing_zeros_expr(expr).lower(), ns));
   }
+  else if(expr.id() == ID_bitreverse)
+    return convert_bitreverse(to_bitreverse_expr(expr));
 
   return conversion_failed(expr);
 }
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arrays.h"
 
 class array_comprehension_exprt;
+class bitreverse_exprt;
 class bswap_exprt;
 class byte_extract_exprt;
 class byte_update_exprt;
@@ -192,6 +193,7 @@ class boolbvt:public arrayst
   virtual bvt convert_power(const binary_exprt &expr);
   virtual bvt convert_function_application(
     const function_application_exprt &expr);
+  virtual bvt convert_bitreverse(const bitreverse_exprt &expr);
 
   virtual exprt make_bv_expr(const typet &type, const bvt &bv);
   virtual exprt make_free_bv_expr(const typet &type);
diff --git a/src/solvers/flattening/boolbv_bitreverse.cpp b/src/solvers/flattening/boolbv_bitreverse.cpp
@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module:
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "boolbv.h"
+
+#include <util/bitvector_expr.h>
+
+bvt boolbvt::convert_bitreverse(const bitreverse_exprt &expr)
+{
+  const std::size_t width = boolbv_width(expr.type());
+  if(width == 0)
+    return conversion_failed(expr);
+
+  bvt bv = convert_bv(expr.op(), width);
+
+  std::reverse(bv.begin(), bv.end());
+
+  return bv;
+}
diff --git a/src/solvers/smt2/smt2_conv.cpp b/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,
diff --git a/src/util/bitvector_expr.cpp b/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()};
+}
diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h
@@ -1008,4 +1008,52 @@ 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))
+  {
+  }
+
+  /// Lower a bitreverse_exprt to arithmetic and logic expressions.
+  /// \return Semantically equivalent expression
+  exprt lower() const;
+};
+
+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
diff --git a/src/util/irep_ids.def b/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
diff --git a/src/util/simplify_expr.cpp b/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);
diff --git a/src/util/simplify_expr_class.h b/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);
diff --git a/src/util/simplify_expr_int.cpp b/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);
+}

Original file line number	Diff line number	Diff line change
`@@ -227,6 +227,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)`
`227`	`227`	`return convert_bv(`
`228`	`228`	`simplify_expr(to_count_trailing_zeros_expr(expr).lower(), ns));`
`229`	`229`	`}`
	`230`	`+ else if(expr.id() == ID_bitreverse)`
	`231`	`+ return convert_bitreverse(to_bitreverse_expr(expr));`
`230`	`232`
`231`	`233`	`return conversion_failed(expr);`
`232`	`234`	`}`