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,77 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_type)
     return convert(src.type());
 
+  else if(src.id() == ID_rol)
+  {
+    // AAAA rol n ==   (AAAA << n % width(AAAA))
+    //               | (AAAA >> (width(AAAA) - n % width(AAAA)))
+    auto bin_expr = to_binary_expr(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 = bin_expr.op0();
+    if(can_cast_type<signedbv_typet>(op0.type()))
+    {
+      // Shifts in C are arithmetic and care about sign, by forcing
+      // a cast to unsigned we force the shifts to perform rol/r
+      size_t ws = op0.type().get_size_t("width");
+      op0 = typecast_exprt(op0, unsignedbv_typet(ws));
+    }
+    // Get n because we need its type to construct the "width(AAAA)"
+    // value to use in operations below.
+    exprt &op1 = bin_expr.op1();
+    // Construct the "width(AAAA)" constant
+    irep_idt width_val = op0.type().get("width");
+    auto width = constant_exprt(width_val, op1.type());
+    // Apply modulo to n since shifting will overflow
+    // That is: 0001 << 4 == 0, but 0001 rol 4 == 0001
+    op1 = mod_exprt(op1, width);
+    // Now put the pieces together
+    // width(AAAA) - (n % width(AAAA))
+    auto complement_expr = minus_exprt(width, op1);
+    // AAAA >> complement_expr
+    auto rhs_expr = ashr_exprt(op0, complement_expr);
+    // AAAA << (n % width(AAAA))
+    auto lhs_exprt = shl_exprt(op0, op1);
+    // The whole thing
+    auto the_expr = bitor_exprt(lhs_exprt, rhs_expr);
+    return convert_with_precedence(the_expr, precedence);
+  }
+  else if(src.id() == ID_ror)
+  {
+    // AAAA rol n ==   (AAAA >> n % width(AAAA))
+    //               | (AAAA << (width(AAAA) - n % width(AAAA)))
+    auto bin_expr = to_binary_expr(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 = bin_expr.op0();
+    if(can_cast_type<signedbv_typet>(op0.type()))
+    {
+      // Shifts in C are arithmetic and care about sign, by forcing
+      // a cast to unsigned we force the shifts to perform rol/r
+      size_t ws = op0.type().get_size_t("width");
+      op0 = typecast_exprt(op0, unsignedbv_typet(ws));
+    }
+    // Get n because we need its type to construct the "width(AAAA)"
+    // value to use in operations below.
+    exprt &op1 = bin_expr.op1();
+    // Construct the "width(AAAA)" constant
+    irep_idt width_val = op0.type().get("width");
+    auto width = constant_exprt(width_val, op1.type());
+    // Apply modulo to n since shifting will overflow
+    // That is: 0001 >> 4 == 0, but 0001 ror 4 == 0001
+    op1 = mod_exprt(op1, width);
+    // Now put the pieces together
+    // width(AAAA) - (n % width(AAAA))
+    auto complement_expr = minus_exprt(width, op1);
+    // AAAA << complement_expr
+    auto rhs_expr = shl_exprt(op0, complement_expr);
+    // AAAA >> (n % width(AAAA))
+    auto lhs_exprt = ashr_exprt(op0, op1);
+    // The whole thing
+    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;