Add conversion for rol and ror operators to c output

This adds conversion for the rol and ror operators from CBMC
internals into C code. This is done by bit-twiddling the values
to achieve the outcome.

Fixes #6241

Author: TGWDB

src/ansi-c/expr2c.cpp

@@ -3794,6 +3794,59 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_type)
     return convert(src.type());
 
+  else if(src.id() == ID_rol)
+  {
+    // TODO:
+    // 1. check RHS is >= 0 && < LHS.type.width
+    //    Can be done with bitmasks...
+    // 2. handle signed types: convert to unsigned, rotate, convert back
+    // AAAA rol n == (AAAA << n) | (AAAA >> (width(AAAA) - n))
+    auto bin_expr = to_binary_expr(src);
+    const exprt &op0 = bin_expr.op0();
+    const exprt &op1 = bin_expr.op1();
+    irep_idt width_val = op0.type().get("width");
+    // if(can_cast_type<signedbv_typet>(op0.type()))
+    // {
+    //   // Do something
+    // }
+    auto width = constant_exprt(width_val, op1.type());
+    auto complement_expr = minus_exprt(width, op1);
+    auto rhs_expr = ashr_exprt(op0, complement_expr);
+    // if(can_cast_type<signedbv_typet>(op0.type()))
+    // {
+    //   // (Un)Do something
+    // }
+    auto lhs_exprt = shl_exprt(op0, op1);
+    auto the_expr = bitor_exprt(lhs_exprt, rhs_expr);
+    return convert_with_precedence(the_expr, precedence);
+  }
+  else if(src.id() == ID_ror)
+  {
+    // TODO:
+    // 1. check RHS is >= 0 && < LHS.type.width
+    //    Can be done with bitmasks...
+    // 2. handle signed types: convert to unsigned, rotate, convert back
+    // AAAA ror n == (AAAA >> n) | (AAAA << (width(AAAA) - n))
+    auto bin_expr = to_binary_expr(src);
+    const exprt &op0 = bin_expr.op0();
+    const exprt &op1 = bin_expr.op1();
+    irep_idt width_val = op0.type().get("width");
+    // if(can_cast_type<signedbv_typet>(op0.type()))
+    // {
+    //   // Do something
+    // }
+    auto width = constant_exprt(width_val, op1.type());
+    auto complement_expr = minus_exprt(width, op1);
+    auto rhs_expr = shl_exprt(op0, complement_expr);
+    // if(can_cast_type<signedbv_typet>(op0.type()))
+    // {
+    //   // (Un)Do something
+    // }
+    auto lhs_exprt = ashr_exprt(op0, op1);
+    auto the_expr = bitor_exprt(lhs_exprt, rhs_expr);
+    return convert_with_precedence(the_expr, precedence);
+  }
+
   auto function_string_opt = convert_function(src);
   if(function_string_opt.has_value())
     return *function_string_opt;