Merge pull request #5739 from diffblue/rolror

rol and ror expressions

Author: kroening

regression/cbmc/clang_builtins/rotate.c

@@ -0,0 +1,97 @@
+#include <assert.h>
+#include <limits.h>
+#include <stdint.h>
+
+#define rol(type, x, d)                                                        \
+  ((type)(((x) << (d)) | ((x) >> ((8 * sizeof(type)) - (d)))))
+
+#define ror(type, x, d)                                                        \
+  ((type)(((x) >> (d)) | ((x) << ((8 * sizeof(type)) - (d)))))
+
+#ifdef __clang__
+void check_left8(void)
+{
+  uint8_t op;
+  assert(__builtin_rotateleft8(op, 1) == rol(uint8_t, op, 1));
+  assert(__builtin_rotateleft8(op, 2) == rol(uint8_t, op, 2));
+  assert(__builtin_rotateleft8(op, 3) == rol(uint8_t, op, 3));
+  assert(__builtin_rotateleft8(op, 4) == rol(uint8_t, op, 4));
+}
+
+void check_left16(void)
+{
+  uint16_t op;
+  assert(__builtin_rotateleft16(op, 1) == rol(uint16_t, op, 1));
+  assert(__builtin_rotateleft16(op, 2) == rol(uint16_t, op, 2));
+  assert(__builtin_rotateleft16(op, 3) == rol(uint16_t, op, 3));
+  assert(__builtin_rotateleft16(op, 4) == rol(uint16_t, op, 4));
+}
+
+void check_left32(void)
+{
+  uint32_t op;
+  assert(__builtin_rotateleft32(op, 1) == rol(uint32_t, op, 1));
+  assert(__builtin_rotateleft32(op, 2) == rol(uint32_t, op, 2));
+  assert(__builtin_rotateleft32(op, 3) == rol(uint32_t, op, 3));
+  assert(__builtin_rotateleft32(op, 4) == rol(uint32_t, op, 4));
+}
+
+void check_left64(void)
+{
+  uint64_t op;
+  assert(__builtin_rotateleft64(op, 1) == rol(uint64_t, op, 1));
+  assert(__builtin_rotateleft64(op, 2) == rol(uint64_t, op, 2));
+  assert(__builtin_rotateleft64(op, 3) == rol(uint64_t, op, 3));
+  assert(__builtin_rotateleft64(op, 4) == rol(uint64_t, op, 4));
+}
+
+void check_right8(void)
+{
+  uint8_t op;
+  assert(__builtin_rotateright8(op, 1) == ror(uint8_t, op, 1));
+  assert(__builtin_rotateright8(op, 2) == ror(uint8_t, op, 2));
+  assert(__builtin_rotateright8(op, 3) == ror(uint8_t, op, 3));
+  assert(__builtin_rotateright8(op, 4) == ror(uint8_t, op, 4));
+}
+
+void check_right16(void)
+{
+  uint16_t op;
+  assert(__builtin_rotateright16(op, 1) == ror(uint16_t, op, 1));
+  assert(__builtin_rotateright16(op, 2) == ror(uint16_t, op, 2));
+  assert(__builtin_rotateright16(op, 3) == ror(uint16_t, op, 3));
+  assert(__builtin_rotateright16(op, 4) == ror(uint16_t, op, 4));
+}
+
+void check_right32(void)
+{
+  uint32_t op;
+  assert(__builtin_rotateright32(op, 1) == ror(uint32_t, op, 1));
+  assert(__builtin_rotateright32(op, 2) == ror(uint32_t, op, 2));
+  assert(__builtin_rotateright32(op, 3) == ror(uint32_t, op, 3));
+  assert(__builtin_rotateright32(op, 4) == ror(uint32_t, op, 4));
+}
+
+void check_right64(void)
+{
+  uint64_t op;
+  assert(__builtin_rotateright64(op, 1) == ror(uint64_t, op, 1));
+  assert(__builtin_rotateright64(op, 2) == ror(uint64_t, op, 2));
+  assert(__builtin_rotateright64(op, 3) == ror(uint64_t, op, 3));
+  assert(__builtin_rotateright64(op, 4) == ror(uint64_t, op, 4));
+}
+#endif
+
+int main(void)
+{
+#ifdef __clang__
+  check_left8();
+  check_left16();
+  check_left32();
+  check_left64();
+  check_right8();
+  check_right16();
+  check_right32();
+  check_right64();
+#endif
+}

regression/cbmc/clang_builtins/rotate.desc

@@ -0,0 +1,6 @@
+CORE gcc-only
+rotate.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

src/ansi-c/c_typecheck_expr.cpp

@@ -2314,6 +2314,38 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(bswap_expr);
   }
+  else if(
+    identifier == "__builtin_rotateleft8" ||
+    identifier == "__builtin_rotateleft16" ||
+    identifier == "__builtin_rotateleft32" ||
+    identifier == "__builtin_rotateleft64" ||
+    identifier == "__builtin_rotateright8" ||
+    identifier == "__builtin_rotateright16" ||
+    identifier == "__builtin_rotateright32" ||
+    identifier == "__builtin_rotateright64")
+  {
+    // clang only
+    if(expr.arguments().size() != 2)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects two operands" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    irep_idt id = (identifier == "__builtin_rotateleft8" ||
+                   identifier == "__builtin_rotateleft16" ||
+                   identifier == "__builtin_rotateleft32" ||
+                   identifier == "__builtin_rotateleft64")
+                    ? ID_rol
+                    : ID_ror;
+
+    shift_exprt rotate_expr(expr.arguments()[0], id, expr.arguments()[1]);
+    rotate_expr.add_source_location() = source_location;
+
+    return std::move(rotate_expr);
+  }
   else if(identifier=="__builtin_nontemporal_load")
   {
     if(expr.arguments().size()!=1)

src/ansi-c/clang_builtin_headers.h

@@ -8,3 +8,15 @@ void __builtin_nontemporal_store();
 void __builtin_nontemporal_load();
 
 int __builtin_flt_rounds(void);
+
+// clang-format off
+unsigned char __builtin_rotateleft8(unsigned char, unsigned char);
+unsigned short __builtin_rotateleft16(unsigned short, unsigned short);
+unsigned int __builtin_rotateleft32(unsigned int, unsigned int);
+unsigned long long __builtin_rotateleft64(unsigned long long, unsigned long long);
+
+unsigned char __builtin_rotateright8(unsigned char, unsigned char);
+unsigned short __builtin_rotateright16(unsigned short, unsigned short);
+unsigned int __builtin_rotateright32(unsigned int, unsigned int);
+unsigned long long __builtin_rotateright64(unsigned long long, unsigned long long);
+// clang-format on

src/solvers/smt2/smt2_conv.cpp

@@ -1362,6 +1362,46 @@ void smt2_convt::convert_expr(const exprt &expr)
         "unsupported type for " + shift_expr.id_string() + ": " +
         type.id_string());
   }
+  else if(expr.id() == ID_rol || expr.id() == ID_ror)
+  {
+    const shift_exprt &shift_expr = to_shift_expr(expr);
+    const typet &type = shift_expr.type();
+
+    if(
+      type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+      type.id() == ID_bv)
+    {
+      // SMT-LIB offers rotate_left and rotate_right, but these require a
+      // constant distance.
+      if(shift_expr.id() == ID_rol)
+        out << "((_ rotate_left";
+      else if(shift_expr.id() == ID_ror)
+        out << "((_ rotate_right";
+      else
+        UNREACHABLE;
+
+      out << ' ';
+
+      auto distance_int_op = numeric_cast<mp_integer>(shift_expr.distance());
+
+      if(distance_int_op.has_value())
+      {
+        out << distance_int_op.value();
+      }
+      else
+        UNEXPECTEDCASE(
+          "distance type for " + shift_expr.id_string() + "must be constant");
+
+      out << ") ";
+      convert_expr(shift_expr.op());
+
+      out << ")"; // rotate_*
+    }
+    else
+      UNEXPECTEDCASE(
+        "unsupported type for " + shift_expr.id_string() + ": " +
+        type.id_string());
+  }
   else if(expr.id()==ID_with)
   {
     convert_with(to_with_expr(expr));

src/util/std_expr.h

@@ -2503,8 +2503,7 @@ inline bitand_exprt &to_bitand_expr(exprt &expr)
   return static_cast<bitand_exprt &>(expr);
 }
 
-
-/// \brief A base class for shift operators
+/// \brief A base class for shift and rotate operators
 class shift_exprt:public binary_exprt
 {
 public:
@@ -2539,7 +2538,8 @@ class shift_exprt:public binary_exprt
 template <>
 inline bool can_cast_expr<shift_exprt>(const exprt &base)
 {
-  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr;
+  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr ||
+         base.id() == ID_ror || base.id() == ID_rol;
 }
 
 inline void validate_expr(const shift_exprt &value)