---

yaml
---
r: 83309
b: refs/heads/variant-submodule
c: c750f5e
h: refs/heads/develop
i:
  83307: 4ebdcd6

Author: TGWDB

[refs]

@@ -131,7 +131,7 @@ refs/heads/unwind-counters4: 57aedaa3fe3995b30ba69c96c9f04df79f8e8ff8
 refs/heads/value-set-make-member: 0f8404cb460f55d43bc253e12f1bde7fd7ed4d37
 refs/heads/value-set-member-fix: 2c87bd4c0d9e1954e2de6af0118fa1ef296ae548
 "refs/heads/value_set_fi_hacks": 3d243543adb4ff450596e7994e2fa1d590ec1e1b
-refs/heads/variant-submodule: 5d4b7803c1bf2002fc0f367920e89ac6b04b2a84
+refs/heads/variant-submodule: c750f5e9eec033096f42e04518a9f6591a9cc105
 refs/heads/windows-console-streambuf: b984ac7bd772da956bb5656f0072d85b3fdbbf34
 refs/tags/cbmc-5.10: 097cf712f57d59cff9c53a9fb7b9b81be1245f93
 refs/tags/cbmc-5.11: 90d0de91b0918c9e5d5ed250cae62241ae38392a

branches/variant-submodule/src/Makefile

@@ -91,7 +91,7 @@ memory-analyzer.dir: util.dir goto-programs.dir langapi.dir linking.dir \
 	                   ansi-c.dir
 
 symtab2gb.dir: util.dir goto-programs.dir langapi.dir linking.dir \
-               json.dir json-symtab-language.dir ansi-c.dir
+               json.dir json-symtab-language.dir
 
 # building for a particular directory
 

branches/variant-submodule/src/ansi-c/expr2c.cpp

@@ -2290,6 +2290,72 @@ std::string expr2ct::convert_initializer_list(const exprt &src)
   return dest;
 }
 
+std::string expr2ct::convert_rox(const exprt &src, unsigned precedence)
+{
+  // AAAA rox n ==   (AAAA lhs_op n % width(AAAA))
+  //               | (AAAA rhs_op (width(AAAA) - n % width(AAAA)))
+  // Where lhs_op and rhs_op depend on whether it is rol or ror
+  // auto rotate_expr = to_binary_expr(src);
+  auto rotate_expr = expr_checked_cast<shift_exprt>(src);
+  // Get AAAA and if it's signed wrap it in a cast to remove
+  // the sign since this messes with C shifts
+  exprt &op0 = rotate_expr.op();
+  size_t type_width;
+  if(can_cast_type<signedbv_typet>(op0.type()))
+  {
+    // Set the type width
+    type_width = to_signedbv_type(op0.type()).get_width();
+    // Shifts in C are arithmetic and care about sign, by forcing
+    // a cast to unsigned we force the shifts to perform rol/r
+    op0 = typecast_exprt(op0, unsignedbv_typet(type_width));
+  }
+  else if(can_cast_type<unsignedbv_typet>(op0.type()))
+  {
+    // Set the type width
+    type_width = to_unsignedbv_type(op0.type()).get_width();
+  }
+  else
+  {
+    // Type that can't be represented as bitvector
+    // get some kind of width in a potentially unsafe way
+    type_width = op0.type().get_size_t("width");
+  }
+  // Construct the "width(AAAA)" constant
+  const exprt width_expr =
+    from_integer(type_width, rotate_expr.distance().type());
+  // Apply modulo to n since shifting will overflow
+  // That is: 0001 << 4 == 0, but 0001 rol 4 == 0001
+  const exprt distance_modulo_width =
+    mod_exprt(rotate_expr.distance(), width_expr);
+  // Now put the pieces together
+  // width(AAAA) - (n % width(AAAA))
+  const auto complement_width_expr =
+    minus_exprt(width_expr, distance_modulo_width);
+  // lhs and rhs components defined according to rol/ror
+  exprt lhs_expr;
+  exprt rhs_expr;
+  if(src.id() == ID_rol)
+  {
+    // AAAA << (n % width(AAAA))
+    lhs_expr = shl_exprt(op0, distance_modulo_width);
+    // AAAA >> complement_width_expr
+    rhs_expr = ashr_exprt(op0, complement_width_expr);
+  }
+  else if(src.id() == ID_ror)
+  {
+    // AAAA >> (n % width(AAAA))
+    lhs_expr = ashr_exprt(op0, distance_modulo_width);
+    // AAAA << complement_width_expr
+    rhs_expr = shl_exprt(op0, complement_width_expr);
+  }
+  else
+  {
+    // Someone called this function when they shouldn't have.
+    UNREACHABLE;
+  }
+  return convert_with_precedence(bitor_exprt(lhs_expr, rhs_expr), precedence);
+}
+
 std::string expr2ct::convert_designated_initializer(const exprt &src)
 {
   if(src.operands().size()!=1)
@@ -3794,6 +3860,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_type)
     return convert(src.type());
 
+  else if(src.id() == ID_rol || src.id() == ID_ror)
+    return convert_rox(src, precedence);
+
   auto function_string_opt = convert_function(src);
   if(function_string_opt.has_value())
     return *function_string_opt;

branches/variant-submodule/src/ansi-c/expr2c_class.h

@@ -126,6 +126,15 @@ class expr2ct
     const std::string &symbol2,
     unsigned precedence);
 
+  /// Conversion function from rol/ror expressions to C code strings
+  /// Note that this constructs a complex expression to do bit
+  /// twiddling since rol/ror operations are not native to ANSI-C.
+  /// The complex expression is then recursively converted.
+  /// \param src: is an exprt that must be either an rol or ror
+  /// \param precedence: precedence for bracketing
+  /// \returns string for performing rol/ror as bit twiddling with C
+  std::string convert_rox(const exprt &src, unsigned precedence);
+
   std::string convert_overflow(
     const exprt &src, unsigned &precedence);